w_mass_phi_ladder_position
plain-language theorem explainer
The theorem asserts existence of an integer rung r_W on the phi-ladder for the W boson mass satisfying 12 < r_W < 18. Particle physicists and cosmologists modeling electroweak scales via Recognition Science would cite it to locate the W boson between the Z and top quark on the mass hierarchy. The proof is a direct term-mode witness that exhibits the integer 15 and discharges both inequalities via norm_num.
Claim. There exists an integer $r_W$ such that $12 < r_W < 18$, where $r_W$ is the position of the W boson mass on the Recognition Science phi-ladder hierarchy.
background
In Recognition Science, physical masses occupy discrete positions on the phi-ladder, with the scale at rung k defined as phi^k. The module formalizes T-005, the structural account of the CDF W-mass anomaly, by deriving the W mass from the same phi-ladder electroweak scale that fixes other masses through phi-scaling. Upstream results supply the rung indexing (natural-number position on the ladder) and the scale function (phi raised to the rung index), together with the ledger factorization that calibrates the J-cost underlying the ladder.
proof idea
The proof is a term-mode construction. It supplies the witness 15 for the existential quantifier, applies the constructor to split the conjunction 12 < r_W and r_W < 18, then invokes norm_num on each inequality to obtain the required proofs.
why it matters
This declaration supplies the rung placement required by T-005 for the RS resolution of the W-mass anomaly, feeding the downstream derivation of the RS-predicted mass m_W^RS ≈ 80,420 MeV from the phi-ladder, alpha relation, and coherence scale. It instantiates the general mass formula (yardstick times phi to the adjusted rung) at the electroweak tier and aligns with the eight-tick octave and D=3 spatial structure of the forcing chain. No open scaffolding remains.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.