solarTangent_band
plain-language theorem explainer
The theorem establishes that the solar neutrino mixing tangent equals the reciprocal of the golden ratio and lies strictly inside (0.617, 0.623). Neutrino physicists parametrizing the PMNS matrix would cite the interval when matching the RS golden-ratio prediction to the measured tan θ₁₂ near 0.62. The proof unfolds the definition to φ^{-1} and applies the pre-proved bounds 1.61 < φ < 1.62 together with reciprocal inequalities and linear arithmetic.
Claim. $0.617 < φ^{-1} < 0.623$, where $φ = (1 + √5)/2$ is the golden ratio and $φ^{-1}$ is identified with the tangent of the solar mixing angle θ₁₂.
background
The module treats the five PMNS parameters (θ₁₂, θ₂₃, θ₁₃, δ_CP, two Majorana phases) as the configuration dimension D = 5. It isolates the solar tangent as tan θ₁₂ ≈ arctan(φ^{-1}) and the atmospheric angle as maximal mixing at π/4. The definition solarTangent simply sets this quantity to φ^{-1}, allowing direct numerical verification against the experimental window near 33.4°.
proof idea
The term proof first unfolds solarTangent to obtain φ^{-1}. It splits the conjunction, rewrites the lower bound via lt_inv_comm₀ and discharges it by linarith using phi_gt_onePointSixOne. The upper bound is handled symmetrically by inv_lt_comm₀ followed by linarith with phi_lt_onePointSixTwo.
why it matters
The result supplies the solar_tangent_band field inside the pmnsCert certificate that collects the five parameters, the maximal-mixing condition, and this interval. It implements the RS structural observation that θ₁₂ ≈ arctan(φ^{-1}) lies inside the measured band, closing one concrete numerical check required to match the phi-ladder predictions to neutrino data.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.