mass_ratio_phi_connection
plain-language theorem explainer
The declaration confirms that the neutrino mass ratio and φ^7 are both positive. This acts as an initial consistency check for the Recognition Science prediction that the atmospheric to solar mass-squared difference ratio approximates φ^7 within roughly 15 percent. Neutrino physicists building φ-quantized PMNS models would cite it as a basic positivity anchor. The proof is a short term-mode construction that splits the conjunction, unfolds the ratio definition, and applies norm_num plus positivity.
Claim. Let $r$ denote the ratio of atmospheric to solar neutrino mass-squared differences. Then $r > 0$ and $φ^7 > 0$.
background
The PMNSMatrix module derives the Pontecorvo-Maki-Nakagawa-Sakata neutrino mixing matrix from Recognition Science, where flavor mixing angles are φ-quantized and large angles (θ12 ≈ 34°, θ23 ≈ 45°, θ13 ≈ 8.6°) emerge from golden-ratio geometry. The mass ratio is the observed ratio of squared mass differences Δm²31 / Δm²21, placed near 33.8 in data. Upstream results supply the J-cost structure from PhiForcingDerived.of and the 8-tick phases from EightTick.phase, which calibrate the φ-ladder for mass formulas.
proof idea
The proof applies constructor to split the conjunction into two goals. It unfolds mass_ratio together with deltam31_sq and deltam21_sq, then uses norm_num to verify the numerical positivity of the ratio. The second goal invokes phi_pos and applies positivity to conclude φ^7 > 0.
why it matters
This supplies the minimal positivity fact required to support the mass-ratio connection inside the PMNS derivation. It aligns with the module target of deriving PMNS elements from φ-angles and with the T6 self-similar fixed point plus the phi-ladder mass formula. The declaration fills an early step toward the paper proposition on neutrino mixing angles from golden-ratio geometry, though the numerical approximation itself remains open for later closure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.