pmns_theta12_match
plain-language theorem explainer
The theorem shows that the Recognition-derived prediction for sin²θ₁₂, obtained from φ^{-2} minus ten times the fine-structure constant, differs from the measured value 0.307 by less than 0.01. Neutrino physicists and model builders interested in geometric origins of mixing angles would reference this result. The proof works by establishing tight numeric bounds on φ^{-2} and α, then applying linear arithmetic to verify the absolute difference lies inside the required interval.
Claim. $|s - 0.307| < 0.01$ where $s = φ^{-2} - 10α$, with $φ$ the golden ratio and $α$ the fine-structure constant.
background
In the Recognition Science framework the PMNS mixing angles arise from overlaps of 8-tick generation windows on the cubic ledger. The solar angle θ₁₂ is predicted at leading order by the combination φ^{-2} - 10α, where the coefficient 10 is fixed by cube topology. The module derives all CKM and PMNS elements geometrically, replacing ad-hoc parameters with topological ratios. Upstream, the fine-structure constant α is defined as 1/α_inv in Constants.Alpha, and bounds on φ^{-2} come from Numerics.phi_neg2_gt and phi_neg2_lt.
proof idea
The proof unfolds sin2_theta12_pred to φ^{-2} - 10*Constants.alpha. It obtains lower and upper bounds on φ^{-2} via simpa from phi_neg2_gt and phi_neg2_lt, and on α from CKMGeometry.alpha_lower_bound and alpha_upper_bound. Linear arithmetic (linarith) then shows that the resulting interval for the difference sits inside (0.297, 0.317). Finally rw [abs_lt] and two linarith applications close the goal.
why it matters
This result supplies the θ₁₂ entry in the MixingCert produced by mixing_verified, which in turn populates the PMNS scorecard row. It completes one step of the Phase 7.2 geometric derivation of the full mixing matrix from the 8-tick octave structure. The match supports the claim that the eight-tick closure forces unitary mixing with angles fixed by φ and α.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.