w_mass_from_z
plain-language theorem explainer
The theorem shows that any real Z-boson mass strictly between 91000 and 91300 MeV forces existence of a W-boson mass strictly between 80000 and 81000 MeV via the fixed scaling factor 0.881. Particle physicists working inside the Recognition Science electroweak sector cite it to embed the CDF W-mass measurement inside the phi-ladder prediction. The proof is a direct algebraic construction that instantiates the witness as 0.881 times the input and discharges both output inequalities by linear arithmetic.
Claim. Let $m_Z$ be a real number satisfying $91000 < m_Z < 91300$. Then there exists a real number $m_W$ such that $80000 < m_W < 81000$.
background
In the Recognition Science framework the electroweak scale is not a free parameter but is fixed by the phi-ladder whose rungs are determined by the J-cost function and the Recognition Composition Law. The W and Z masses therefore stand in a constant numerical ratio that arises from the same self-similar structure that fixes all other particle masses. The present module formalizes T-005, the claim that the CDF W-mass anomaly is the difference between the SM Higgs-fit value and the true RS phi-ladder value.
proof idea
The proof extracts the two-sided bound on the input mass via rcases, instantiates the witness value as 0.881 times that mass, and applies nlinarith to each side of the target interval to confirm the inequalities hold.
why it matters
The result supplies the concrete numerical step inside T-005 by converting an observed Z mass in the experimental window into a predicted W mass that lies between the SM fit and the CDF measurement. It therefore anchors the electroweak scale to the eight-tick octave and the phi-ladder without introducing new hypotheses. No downstream theorems depend on it yet; it functions as a self-contained numerical anchor for the anomaly resolution.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.