mass_ratio_cert_exists
plain-language theorem explainer
The declaration proves existence of a certificate whose fields are the strict inequalities 17 < φ^6 and φ^6 < 18. Researchers deriving particle masses from the φ-ladder would cite it to anchor the numerical interval that enters rung-based mass predictions. The proof is a one-line term construction that packages the two components of the companion bounds theorem into the certificate structure.
Claim. There exists a certificate structure whose fields satisfy the inequalities $17 < phi^6$ and $phi^6 < 18$, where $phi$ is the golden ratio obeying $phi^2 = phi + 1$.
background
The module supplies rigorous proofs for mass ratios expressed as powers of φ on the φ-ladder. MassRatioCert is the structure that packages two real inequalities bounding φ^6 between 17 and 18. The upstream theorem phi_6_bounds_mass_ratio derives these bounds from the identity φ^6 = (φ^3)^2 together with φ^3 = 2φ + 1 and the interval 1.5 < φ < 1.62.
proof idea
The proof is a one-line term-mode wrapper that constructs an element of MassRatioCert by pairing the left and right projections of phi_6_bounds_mass_ratio.
why it matters
This result supplies the existence witness for the mass-ratio certificate that anchors numerical predictions on the φ-ladder. It supports the mass formula yardstick * φ^(rung - 8 + gap(Z)) by confirming the φ^6 interval used for scaling. Within the Recognition framework it closes the step from the algebraic identity φ^6 = (2φ + 1)^2 to a concrete numerical bound required for particle-mass ordering.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.