complex_norm_ofReal
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not apply to genuinely complex inputs.
- Does not supply any approximation or error bound, only an equality.
- Does not invoke Recognition-specific axioms beyond the ambient Mathlib library.
Lean usage
have hx_complex : ‖(x : ℂ)‖ < 1 := by rw [complex_norm_ofReal]; exact hxformal statement (Lean)
101lemma complex_norm_ofReal (x : ℝ) : ‖(x : ℂ)‖ = |x| := by
proof body
Term-mode proof.
102 have : (x : ℂ) = (RCLike.ofReal x : ℂ) := rfl
103 rw [this, RCLike.norm_ofReal]
104
105/-- Error bound for log Taylor polynomial on reals, using Complex.norm_log_sub_logTaylor_le -/