sin2_theta13_pred
plain-language theorem explainer
The declaration defines the predicted sin²θ₁₃ as the reactor mixing weight φ^{-8}. Neutrino physicists checking geometric PMNS predictions against oscillation data would cite this when assembling mixing certificates. The definition is a direct alias to the upstream reactor_weight constant.
Claim. The predicted value of the squared sine of the PMNS reactor mixing angle equals the reactor weight: $sin^2 θ_{13} = φ^{-8}$, where $φ$ denotes the golden ratio.
background
In the Recognition Science framework the reactor mixing weight is the octave closure factor φ^{-8} arising from the eight-tick period (T7) in the forcing chain. The module derives CKM and PMNS mixing elements geometrically from the cubic ledger structure, with edge-dual coupling fixed by overlaps of 8-tick windows. Upstream, reactor_weight is introduced in MixingGeometry as the basic topological ratio that replaces numerical fitting for the reactor angle.
proof idea
This is a one-line wrapper that directly aliases the reactor_weight definition from MixingGeometry.
why it matters
The definition supplies the predicted sin²θ₁₃ value used inside MixingCert, pmns_theta13_match, and PMNSScoreCardCert. It fills the reactor-angle slot in the Phase 7.2 geometric derivation of the PMNS matrix and connects directly to the eight-tick octave closure and the phi-ladder constants. The match theorem that consumes it still requires external bounds on φ^{-8} from Numerics.Interval.PhiBounds.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.