complex_norm_exp_I_mul
plain-language theorem explainer
The declaration proves that the modulus of the complex exponential at a purely imaginary argument equals one. Researchers working on phase factors in wave equations or gauge theories would cite the identity when verifying unitarity or normalization. The proof is a one-line term wrapper that invokes the matching Mathlib lemma on the exponential norm.
Claim. For any real number $θ$, the complex modulus satisfies $‖e^{iθ}‖ = 1$.
background
This theorem sits in the ClassicalResults module, which assembles standard facts from real and complex analysis to support cost calculations. The module presents these identities as textbook results justified by references such as Ahlfors' Complex Analysis and Conway's Functions of One Complex Variable, rather than new physical postulates. Upstream, CirclePhaseLift.and supplies explicit logarithmic derivative bounds on the circle that frequently accompany phase exponentials, while GaugeInvariance.consequences records the conservation laws that follow from phase invariance in gauge settings.
proof idea
The proof is a one-line term-mode wrapper. It applies the Mathlib lemma Complex.norm_exp_ofReal_mul_I directly to the real angle θ and lets simpa perform the required simplification of the expression θ * I.
why it matters
The identity supplies the basic normalization for complex phases that appear in cost functionals and gauge-invariant constructions. It supports downstream work on circle phase lifts and the consequences of gauge symmetry listed in the QFT submodule. Within the Recognition framework it aligns with the use of periodic structures such as the eight-tick octave, though no specific open question or scaffolding closure is attached to this declaration.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.