sin2_theta13_observed
plain-language theorem explainer
The definition supplies the measured value sin²θ₁₃ = 0.0220 for the reactor neutrino mixing angle. Neutrino oscillation analysts and Recognition Science modelers cite it when matching φ-derived PMNS predictions to data. It is a direct numerical assignment with no lemmas or computation steps.
Claim. The observed value satisfies $sin^2 θ_{13} = 0.0220$.
background
The module constructs the PMNS neutrino mixing matrix from φ-quantized angles, with θ₁₂ ≈ 34°, θ₂₃ ≈ 45° (maximal), and θ₁₃ ≈ 8.6°. Flavor states ν_e, ν_μ, ν_τ mix with mass eigenstates ν₁, ν₂, ν₃ via the unitary matrix U whose elements depend on these angles and a CP phase. Upstream phase definitions provide the 8-tick angles kπ/4 and the complex exponential e^{i w} that build the matrix entries.
proof idea
The definition is a direct numerical binding of the experimental datum 0.0220. No lemmas are applied and no tactics are used.
why it matters
It supplies the target datum for the reactor angle in the PMNS derivation from golden-ratio geometry. The value supports the paper proposition on neutrino mixing angles from φ-angles and aligns with the eight-tick octave structure. No downstream theorems yet reference it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.