TBM_theta13
plain-language theorem explainer
The declaration supplies the exact zero value for the reactor mixing angle under the tri-bimaximal mixing ansatz. Neutrino model builders comparing Recognition Science golden-ratio predictions to the standard TBM benchmark would reference it. The construction is a direct constant assignment with no further reduction or lemma application.
Claim. In the tri-bimaximal mixing scheme the reactor neutrino mixing angle satisfies $θ_{13}=0$.
background
The module derives the PMNS neutrino mixing matrix from Recognition Science φ-quantized angles. Large observed mixings (θ12≈34°, θ23≈45°, θ13≈8.6°) are contrasted with the tri-bimaximal pattern that sets θ13 exactly to zero while fixing the other angles to golden-ratio expressions. Upstream results supply a Hypothesis bundle encoding projection-defect and energy-control conditions for Galerkin states, together with the structural theorem that reduces seven axioms to four substantive conditions plus three definitional facts.
proof idea
The declaration is a direct constant assignment of the real number zero; no lemmas are invoked and the body contains only the literal value.
why it matters
It supplies the TBM baseline against which the sibling phi_prediction_theta13 is measured inside the PMNS derivation. The module doc-comment identifies this step as part of the RS mechanism that replaces the exact TBM zero with a small φ-generated correction. It touches the open question of how the eight-tick octave and φ-ladder produce the observed 8.6° reactor angle.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.