pmns_theta13_born_forced
plain-language theorem explainer
The model sets the predicted sin squared of the PMNS theta13 angle equal to the reactor weight. Neutrino physicists deriving mixing angles from ledger geometry would cite this when matching predictions to reactor data. The proof reduces directly to the definition of the predicted quantity via unfolding and reflexivity.
Claim. In the geometric derivation of the Pontecorvo-Maki-Nakagawa-Sakata mixing matrix, the square of the sine of the mixing angle $θ_{13}$ equals the reactor weight parameter.
background
The module derives CKM and PMNS mixing elements from the cubic ledger structure. Edge-dual coupling sets generation overlaps via 8-tick windows; topological ratios fix elements such as |V_cb| = 1/24; and unitarity follows from 8-tick closure. Upstream, a Cycle is a sequence of vertices in the graded ledger that returns to the start; tick is the fundamental RS time quantum τ₀ = 1; and phase(k) for k in Fin 8 supplies the increments kπ/4.
proof idea
Unfolding the definition of the predicted sin²θ₁₃ and applying reflexivity establishes the equality to the reactor weight.
why it matters
This result completes the forced equality for θ₁₃ in the PMNS sector and connects to the eight-tick octave (T7) together with the phase increments from the 8-tick cycle. It supports unitarity of the mixing matrix in the Recognition framework, though no downstream uses appear yet. It precedes the module's treatment of CP violation arising from tick phases.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.