potential_negative

formal source

  82  -G * M / r
  83
  84/-- The gravitational potential is negative for positive mass at positive distance. -/
  85theorem potential_negative (M r : ℝ) (hM : 0 < M) (hr : 0 < r) :
  86    gravitational_potential M r < 0 := by
  87  unfold gravitational_potential
  88  have eq : -G * M / r = -(G * M / r) := by ring
  89  rw [eq]
  90  exact neg_lt_zero.mpr (div_pos (mul_pos G_pos hM) hr)
  91
  92/-! ## No Separate Quantization Needed -/
  93
  94/-- **G-001 Resolution**: There is no "quantum gravity" problem in RS.
  95
  96    Gravity is not a fundamental force requiring quantization.
  97    Gravity is the large-scale curvature of the ledger lattice.
  98    The ledger IS already the quantum structure.
  99    "Quantizing gravity" is like "quantizing temperature" — a category error.
 100
 101    The ledger provides:
 102    1. Discrete states (quantum structure) at small scales
 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