sin2_theta23_pred
plain-language theorem explainer
The definition sets the predicted sin²θ₂₃ for the PMNS matrix to the sum of the maximal parity mix weight and a face-mediated radiative correction. Neutrino physicists validating geometric mixing predictions against oscillation data would cite this when checking the atmospheric angle. It is realized as a direct algebraic sum of two constants from the mixing geometry layer.
Claim. $sin^2 θ_{23} = 1/2 + 6α$, where α denotes the fine-structure constant.
background
This definition appears in the module that derives CKM and PMNS mixing matrices from the cubic ledger via edge-dual coupling of 8-tick windows and topological ratios. The atmospheric weight supplies the base maximal parity mix of 1/2. The radiative correction supplies the adjustment estimated as six times the fine-structure constant, reflecting face-mediated leakage in the geometry.
proof idea
This is a one-line definition that directly sums the atmospheric weight and the atmospheric radiative correction.
why it matters
It supplies the atmospheric angle input to the MixingCert structure that packages the full geometric mixing proofs. Downstream results such as pmns_theta23_match and PMNSScoreCardCert use it to confirm agreement with the observed value 0.546 within 1%. The construction participates in the unitarity forced by 8-tick closure and the topological ratios of the mixing geometry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.