sin2_theta23_pred
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 in Recognition Science
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.
scope and limits
- Does not derive the angle from dynamical field equations.
- Does not incorporate matter-induced oscillation effects.
- Does not compute CP-violating phases or the Jarlskog invariant.
Lean usage
theorem theta23_match : |sin2_theta23_pred - 0.546| < 0.01 := pmns_theta23_matchformal statement (Lean)
128noncomputable def sin2_theta23_pred : ℝ := atmospheric_weight + atmospheric_radiative_correction