complex_norm_ofReal
plain-language theorem explainer
This lemma asserts that the complex modulus of any real number equals its absolute value. Numerics code constructing interval bounds for the logarithm cites it to convert real absolute-value inequalities into complex-norm inequalities. The term proof is a one-line wrapper that identifies the real-to-complex coercion with RCLike.ofReal and applies the built-in norm identity.
Claim. For every real number $x$, the modulus of $x$ viewed as a complex number equals the absolute value of $x$: $||(x : ℂ)|| = |x|$.
background
The module supplies rigorous interval bounds for the natural logarithm on positive reals by combining monotonicity with Taylor-series error estimates for log(1+x) when |x|<1. The strategy converts real intervals into complex-norm bounds so that Mathlib's Complex.norm_log_sub_logTaylor_le can be applied directly. This helper lemma bridges the real and complex settings by equating the modulus after the canonical embedding of ℝ into ℂ.
proof idea
The proof is a one-line wrapper. It first records the definitional equality (x : ℂ) = RCLike.ofReal x by reflexivity, then rewrites the norm goal using RCLike.norm_ofReal.
why it matters
The lemma is invoked inside log_taylor_error_bound to transfer the hypothesis |x|<1 into the complex-norm form required by Complex.norm_log_sub_logTaylor_le. It therefore supports the numerical verification of log(φ) intervals that feed the phi-ladder mass formula and the eight-tick octave. Within the Recognition framework it closes a small but necessary gap between real absolute values and the complex analysis tools used for T5 J-uniqueness and phi-based constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.