row_pmns_theta13
plain-language theorem explainer
The row_pmns_theta13 theorem certifies that the RS-derived prediction for sin²θ₁₃ lies within absolute error 0.002 of the observed center 0.022. Neutrino phenomenologists assembling PMNS mixing tables would cite this row when checking the reactor angle against PDG or NuFIT data. The proof is a direct one-line reference to the match theorem in MixingDerivation, which applies reciprocal bounds on φ^8 to confirm the numerical interval.
Claim. $|sin^2 θ_{13}^{pred} - 0.022| < 0.002$, where $sin^2 θ_{13}^{pred}$ is the reactor weight defined in the mixing derivation.
background
The PMNSScoreCard module assembles a certificate for the full PMNS mixing angles and Jarlskog invariant against PDG-like targets. The local setting is Phase 2 particle spectrum validation, where predicted values come from MixingDerivation and observed centers are sin²θ₁₂ ≈ 0.307, sin²θ₁₃ ≈ 0.0220, sin²θ₂₃ ≈ 0.545. The identifier sin2_theta13_pred is defined as the reactor_weight, a real number obtained from the RS mixing construction. The upstream theorem pmns_theta13_match states that the absolute difference from 0.022 is less than 0.002 and notes that the proof requires bounds on φ^{-8} supplied by the phi interval numerics.
proof idea
The declaration is a one-line wrapper that directly invokes the pmns_theta13_match theorem from the MixingDerivation module. No additional tactics or reductions are performed; the proof body is simply the reference to that upstream result.
why it matters
This row is referenced inside pmnsScoreCardCert_holds to populate the theta13 field of the PMNSScoreCardCert structure, thereby packaging the reactor-angle match for the overall scorecard. It supplies the concrete interval check for the PMNS reactor angle in the Phase 2 validation, drawing on the phi-ladder predictions that originate in the T5 J-uniqueness and T6 self-similar fixed-point steps of the forcing chain. The remaining open question is the scheme dependence of sin²θ_W and its effect on the extracted PMNS parameters.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.