complex_norm_exp_ofReal
plain-language theorem explainer
The identity asserts that the complex modulus of the exponential of any real scalar equals the real exponential of that scalar. Analysts handling phase factors or magnitude calculations in cost models would cite it when converting between real and complex domains. The proof is a direct rewrite of the complex norm exponential rule followed by simplification of the real part.
Claim. For every real number $r$, the complex modulus satisfies $|e^r| = e^r$, where the exponential on the left is the complex exponential function.
background
This result appears in the ClassicalResults module of the Cost domain, which assembles standard identities from real and complex analysis for later use in Recognition Science calculations. The module presents these as textbook facts justified by references such as Rudin and Ahlfors rather than physical assumptions. Nearby declarations treat the exponential expansion of cosh and the additivity of interval integrals under integrability hypotheses.
proof idea
The proof is a one-line wrapper that rewrites via the library fact Complex.norm_exp and then simplifies the real part of the ofReal embedding.
why it matters
The identity supplies a basic norm equality required for magnitude computations involving complex exponentials in cost functions. It supports downstream hyperbolic and path-integral results inside the same module and closes a minor classical gap without new hypotheses. In the broader framework it aligns with the use of exponential forms in the J-cost and phi-ladder constructions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.