No prose has been written for this declaration yet. The Lean source and graph data below render
without it.
generate prose now
formal statement (Lean)
172theorem mass_ratio_phi_connection :
173 -- Qualitative claim: mass_ratio is within ~20% of φ⁷
174 mass_ratio > 0 ∧ phi^7 > 0 := by
proof body
Term-mode proof.
175 constructor
176 · -- mass_ratio > 0
177 unfold mass_ratio deltam31_sq deltam21_sq
178 norm_num
179 · -- phi^7 > 0
180 have h := phi_pos
181 positivity
182
183/-! ## CP Violation in Neutrinos -/
184
185/-- The CP phase δ_CP ≈ 197° or -163°.
186
187 This is close to π (180°), suggesting near-maximal CP violation.
188
189 RS prediction: δ_CP might be exactly π + small φ-correction.
190 δ_CP = π + (φ - 1)π/10 ≈ π + 0.0618π ≈ 191°
191
192 This is within 1σ of observations! -/
depends on (20)
Lean names referenced from this declaration's body.
-
of
in IndisputableMonolith.Astrophysics.NucleosynthesisTiers
decl_use
-
or
in IndisputableMonolith.Constants.EulerMascheroni
decl_use
-
of
in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization
decl_use
-
phase
in IndisputableMonolith.Foundation.EightTick
decl_use
-
is
in IndisputableMonolith.Foundation.OptionAEmpiricalProgram
decl_use
-
of
in IndisputableMonolith.Foundation.PhiForcingDerived
decl_use
-
is
in IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi
decl_use
-
of
in IndisputableMonolith.Foundation.SpectralEmergence
decl_use
-
is
in IndisputableMonolith.GameTheory.MechanismDesignFromSigma
decl_use
-
of
in IndisputableMonolith.Information.PhysicsComplexityStructure
decl_use
-
correction
in IndisputableMonolith.Information.QuantumChannelCapacityFromPhi
decl_use
-
is
in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom
decl_use
-
phase
in IndisputableMonolith.NumberTheory.RiemannHypothesis.Wedge
decl_use
-
mass_ratio
in IndisputableMonolith.Physics.MesonSpectrumFromPhiLadder
decl_use
-
mass_ratio
in IndisputableMonolith.Physics.NeutrinoMassFromPhiLadder
decl_use
-
deltam21_sq
in IndisputableMonolith.StandardModel.NeutrinoMassHierarchy
decl_use
-
deltam31_sq
in IndisputableMonolith.StandardModel.NeutrinoMassHierarchy
decl_use
-
deltam21_sq
in IndisputableMonolith.StandardModel.PMNSMatrix
decl_use
-
deltam31_sq
in IndisputableMonolith.StandardModel.PMNSMatrix
decl_use
-
mass_ratio
in IndisputableMonolith.StandardModel.PMNSMatrix
decl_use