Quantum mechanics: the exponential of i times a real action is a unit phase
ProvedEveryday.phase_normThe image's first label is quantum mechanics itself: the source equation's dynamics enters through the exponential of i times the action — the phase of each configuration in the path integral. The item is the phase's unitarity: for a real number s — the action of a configuration, in the image's units where ℏ = 1 — the complex number exp(i s) has modulus exactly one. A phase contributes direction, never magnitude.
Formalization Note The action is dimensionless with ℏ = 1, the units of the image, so the phase is exp(iS) rather than exp(iS/ℏ). The proof: the modulus of the complex exponential is the real exponential of the real part of its argument, and the real part of i times a real coercion is zero, so the modulus is the exponential of zero, which is one.
import Mathlib import Definitions.Def_Everyday_spacetime import Definitions.Def_Everyday_sectors
namespace Everyday /-- Quantum mechanics: the exponential of i times a real number is a phase — the amplitude exp(iS) contributed by a single configuration of real action S has modulus exactly one. -/ theorem phase_norm (s : ℝ) : ‖Complex.exp (Complex.I * (s : ℂ))‖ = 1 := by sorry end Everyday
Read-back
What the Lean code literally says, in plain math · glm-5-latest-short
The statement says: for every real number s, the complex norm of the complex exponential of (the imaginary unit times the coercion of s to the complex numbers) equals one. Unfolding, the norm of the complex exponential is the real exponential of the real part of its argument, and the real part of the imaginary unit times a real coercion is zero. The conclusion is an equation between a nonnegative real number and one.