pith. machine review for the scientific record. sign in
theorem proved tactic proof

potential_negative

show as:
view Lean formalization →

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)

  85theorem potential_negative (M r : ℝ) (hM : 0 < M) (hr : 0 < r) :
  86    gravitational_potential M r < 0 := by

proof body

Tactic-mode proof.

  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 -/

depends on (28)

Lean names referenced from this declaration's body.