complex_norm_ofReal
plain-language theorem explainer
The lemma states that the modulus of a real number embedded in the complexes equals its real absolute value. Numerics code for log Taylor bounds cites it to transfer real inequalities into the complex domain for error estimates. The proof is a term-mode one-liner that rewrites via RCLike.ofReal and applies the library identity RCLike.norm_ofReal.
Claim. For every real number $x$, the complex modulus satisfies $||(x : ℂ)|| = |x|$.
background
The Numerics.Interval.Log module develops rigorous interval bounds for the natural logarithm on positive reals. It uses monotonicity of log together with Taylor remainder estimates for log(1+x) when |x|<1, targeting the case x = phi - 1 for golden-ratio intervals. The module imports Mathlib facts on Complex.logTaylor and norm bounds to obtain concrete error controls.
proof idea
Term-mode one-line wrapper. It introduces the reflexivity equality (x : ℂ) = RCLike.ofReal x, then rewrites the goal with RCLike.norm_ofReal.
why it matters
The lemma is invoked inside log_taylor_error_bound to convert a real |x|<1 hypothesis into the corresponding complex-norm hypothesis required by Complex.norm_log_sub_logTaylor_le. It therefore supports the phi-interval arithmetic that feeds numerical verification of constants such as alpha inverse inside the Recognition Science band (137.030, 137.039).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.