pmns_theta23_born_forced
plain-language theorem explainer
The equality sets the predicted squared sine of the atmospheric PMNS mixing angle exactly equal to the maximal parity mix weight plus the face-mediated radiative correction. Neutrino physicists deriving mixing parameters from the cubic ledger geometry cite this when assembling the full PMNS set. The proof is a one-line wrapper that unfolds the definition of the predicted quantity and applies reflexivity.
Claim. $sin^2 theta_{23}^{pred} = w_{atm} + delta_{rad,atm}$ where $w_{atm}$ denotes the maximal parity mix and $delta_{rad,atm}$ is the face-mediated correction proportional to the fine-structure constant.
background
Module Phase 7.2 derives CKM and PMNS matrices geometrically from the cubic ledger via 8-tick window overlaps that fix edge-dual couplings and enforce unitarity. sin2_theta23_pred is introduced as the sum atmospheric_weight + atmospheric_radiative_correction. atmospheric_weight is defined as the maximal parity mix (value 1/2); atmospheric_radiative_correction is defined as 6 * alpha with the attached note that the atmospheric angle is forced from this maximal parity mix plus the face-mediated term.
proof idea
The proof is a one-line wrapper that unfolds the definition of sin2_theta23_pred and applies reflexivity.
why it matters
This declaration supplies the explicit definition of the predicted atmospheric angle inside the PMNS mixing derivation, supporting the module's claim that 8-tick closure forces unitary mixing matrices with topological ratios. It aligns with the Recognition framework's T7 eight-tick octave and the geometric origin of mixing angles. No downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.