pmns_theta23_match
plain-language theorem explainer
The theorem establishes that the predicted sin²θ₂₃, formed from the atmospheric weight plus a radiative correction linear in α, lies within 0.01 of the observed value 0.546. Neutrino phenomenologists seeking a geometric account of the PMNS matrix would cite the result when checking consistency with the cubic ledger. The proof is a term-mode reduction that unfolds the prediction, imports the α bounds, and closes the inequality by linear arithmetic.
Claim. $|sin^2 θ_{23}^{pred} - 0.546| < 0.01$, where the prediction is assembled from the atmospheric weight and the radiative correction proportional to the fine-structure constant α.
background
Recognition Science derives the PMNS angles from edge-dual couplings on the cubic ledger, with the 8-tick window overlap fixing the generational mixing ratios and unitarity enforced by closure. The module replaces numerical fits by topological proofs; α is supplied by Constants.Alpha as the reciprocal of the derived alphaInv, and the coefficient 6 in the radiative term is fixed by cube topology. Upstream lemmas on α bounds and the simplicial ledger supply the numerical interval needed to compare against the PDG datum.
proof idea
The term proof unfolds sin2_theta23_pred together with atmospheric_weight and atmospheric_radiative_correction. It obtains the lower and upper bounds on α from CKMGeometry.alpha_lower_bound and alpha_upper_bound, rewrites the absolute-value goal via abs_lt, and discharges both sides simultaneously by linarith.
why it matters
The result supplies the θ₂₃ component of the MixingCert structure in mixing_verified, which certifies the full CKM-PMNS derivation. It realizes the Phase 7.2 program of obtaining all mixing parameters from the eight-tick octave and cubic ledger geometry, and it populates one row of the PMNS scorecard. The match thereby supports the claim that the observed angles descend directly from the same phi-ladder structure that fixes D = 3 and the alpha band.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.