toReal
plain-language theorem explainer
The definition embeds a rational rung from the φ-ladder into the reals to serve as an exponent in Real.rpow calls inside mass formulas. Modelers working on fractional placements for quark or neutrino spectra cite it to keep the conversion uniform across modules. It is implemented as a direct coercion from ℚ to ℝ.
Claim. Let $r$ be a rational rung on the φ-ladder. Then toReal$(r)$ is the image of $r$ under the canonical embedding of ℚ into ℝ.
background
Rung is the abbreviation ℚ, introduced to represent possibly fractional placements on the φ-ladder. The module supplies a minimal representation seam so that physics modules exploring quarter-ladder refinements can share a uniform convention without altering the integer-rung core mass model. It depends on the transport RealsFromLogic.toReal, which maps a recovered LogicReal to Mathlib's ℝ via CompareReals.compareEquiv.
proof idea
The definition is a one-line coercion that casts the rational rung directly to a real number.
why it matters
It supplies the real embedding required by downstream results such as PhiInt in the algebra layer and the family of toComplex transports in ComplexFromLogic. The declaration closes the reporting seam for fractional rungs inside the mass formula yardstick · φ^(rung − 8 + gap(Z)), linking to the self-similar fixed point at T6. It leaves open whether any specific fractional rung is required by observed spectra.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.