theorem
proved
gravity_from_ledger
show as:
view math explainer →
Gravity falls out of the ledger. Equivalence principle automatic.
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Gravity.ZeroParameterGravity on GitHub at line 106.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
103 2. Continuous curvature (gravity) at large scales
104 3. Both from the SAME J-cost dynamics
105 4. No UV divergences because the lattice provides a natural cutoff -/
106theorem gravity_from_ledger :
107 Foundation.DimensionForcing.eight_tick = 8 ∧
108 0 < kappa_rs :=
109 ⟨rfl, kappa_pos⟩
110
111/-- Extract the discrete 8-tick anchor from the gravity-from-ledger bundle. -/
112theorem gravity_from_ledger_implies_eight_tick
113 (h : Foundation.DimensionForcing.eight_tick = 8 ∧ 0 < kappa_rs) :
114 Foundation.DimensionForcing.eight_tick = 8 :=
115 h.1
116
117/-- Extract positivity of the Einstein coupling from the gravity-from-ledger bundle. -/
118theorem gravity_from_ledger_implies_kappa_pos
119 (h : Foundation.DimensionForcing.eight_tick = 8 ∧ 0 < kappa_rs) :
120 0 < kappa_rs :=
121 h.2
122
123/-- Gravity-from-ledger bundle excludes a vanishing Einstein coupling. -/
124theorem gravity_from_ledger_implies_kappa_ne_zero
125 (h : Foundation.DimensionForcing.eight_tick = 8 ∧ 0 < kappa_rs) :
126 kappa_rs ≠ 0 := ne_of_gt h.2
127
128/-! ## Numerical Bounds on κ -/
129
130/-- Numerical bounds on κ = 8φ⁵.
131 From 10.7 < φ⁵ < 11.3 and κ = 8φ⁵: 85.6 < κ < 90.4. -/
132theorem kappa_bounds : (85.6 : ℝ) < kappa_rs ∧ kappa_rs < 90.4 := by
133 unfold kappa_rs
134 have h1 := phi_fifth_bounds.1
135 have h2 := phi_fifth_bounds.2
136 constructor <;> nlinarith