weak_mixing_bounds
plain-language theorem explainer
The theorem proves that the Recognition Science prediction for the weak mixing parameter satisfies 0.22 < bestPrediction < 0.24. Particle physicists comparing derived gauge couplings to data would cite this when discussing sin²θ_w near 0.230. The proof unfolds the prediction definition, invokes the tight golden-ratio bounds, and applies linear arithmetic to close both inequalities.
Claim. $0.22 < (3 - φ)/6 < 0.24$, where φ is the golden ratio.
background
In the Recognition Science treatment of gauge couplings, the weak mixing angle squared is predicted from the golden ratio φ via the expression (3 - φ)/6. The module derives all three Standard Model couplings from ledger geometry: α from D=3 voxel seams, α_s from wallpaper-group count 17, and sin²θ_w from SU(2)×U(1) structure that runs to ≈0.231 at the Z scale. Upstream lemmas supply the numerical bounds 1.61 < φ < 1.62 that pin the prediction inside the target interval.
proof idea
The tactic proof unfolds bestPrediction to prediction3, obtains phi > 1.61 and phi < 1.62 from the constants module, then applies linarith to establish the lower bound (3 - φ)/6 > 0.22 and the upper bound (3 - φ)/6 < 0.24.
why it matters
This declaration supplies the numerical bound required by the C-014 gauge-coupling derivation chain. It closes the weak-mixing entry in the unification hint where α, α_s and α_w converge near 10¹⁶ GeV. The result rests on the phi-forcing lemmas and the ledger-factorization structures; it leaves open the precise matching to the measured 0.2229 after full running corrections.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.