MassRatioCert
plain-language theorem explainer
MassRatioCert packages the strict bounds 17 < phi^6 < 18 to certify the sixth rung of the phi-ladder used for mass ratios. Researchers deriving particle masses from Recognition Science would cite it to anchor numerical predictions in the phi-powers. The declaration is a bare structure that records the two real inequalities without invoking lemmas or tactics.
Claim. A certificate that $17 < phi^6 < 18$, where $phi$ is the positive real fixed point of the Recognition Composition Law.
background
The Masses.MassRatiosProved module supplies rigorous proofs for mass ratios expressed as powers of phi on the phi-ladder. The ladder itself originates in the forcing chain of UnifiedForcingChain, where T6 forces phi as the self-similar fixed point satisfying J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y). All ratios in the module are therefore written as phi to an integer exponent relative to a chosen yardstick.
proof idea
The declaration is a structure definition that directly asserts the two inequalities. No lemmas are applied and no tactics are used; it simply records the bounds supplied by the sibling phi_6_bounds_mass_ratio.
why it matters
MassRatioCert is the type consumed by the downstream theorem mass_ratio_cert_exists, which proves the structure is nonempty. It supplies the numerical anchor for the phi^6 rung in the mass formula yardstick * phi^(rung - 8 + gap(Z)), thereby supporting the eight-tick octave and the D = 3 spatial dimensions forced by T7 and T8.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.