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)
155theorem top_charm_ratio_bounds :
156 (17 : ℝ) < phi ^ 6 ∧ phi ^ 6 < (18 : ℝ) := phi_pow_6_bounds
proof body
Term-mode proof.
157
158/-! ## Neutrino sector -/
159
160/-- The neutrino squared-mass ratio m₃²/m₂² = φ⁷ ∈ (29, 30).
161 NuFIT 5.3: Δm²₃₁/Δm²₂₁ ≈ 29.0 (for normal ordering).
162 This is a seam-free prediction: no calibration anchor cancels. -/
depends on (8)
Lean names referenced from this declaration's body.
-
is
in IndisputableMonolith.Foundation.OptionAEmpiricalProgram
decl_use
-
is
in IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi
decl_use
-
for
in IndisputableMonolith.Foundation.UniversalForcingSelfReference
decl_use
-
is
in IndisputableMonolith.GameTheory.MechanismDesignFromSigma
decl_use
-
phi_pow_6_bounds
in IndisputableMonolith.Masses.NumericalPredictions
decl_use
-
cancels
in IndisputableMonolith.Masses.Ribbons
decl_use
-
is
in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom
decl_use
-
calibration
in IndisputableMonolith.Measurement.RSNative.Calibration.SingleAnchor
decl_use