potential_negative
plain-language theorem explainer
The result shows that gravitational potential for positive mass M at positive distance r is strictly negative. Researchers deriving Newtonian gravity from ledger curvature in Recognition Science cite it to fix the sign of the potential in zero-parameter models. The proof is a short tactic sequence that unfolds the potential, rewrites via ring, and invokes positivity of G together with the given inequalities on M and r.
Claim. Let $M>0$ and $r>0$ be real numbers. The gravitational potential $V(M,r):=-G M/r$ satisfies $V(M,r)<0$, where $G$ denotes the RS-derived gravitational constant.
background
The Zero-Parameter Gravity module formalizes gravity as large-scale curvature of the ledger lattice induced by defect distributions (G-001). The potential is the standard Newtonian expression whose sign is fixed once $G>0$ is known. Upstream lemmas establish this positivity: Constants.G gives the RS-native form $G=λ_rec^2 c^3/(π ħ)$ while Constants.G_pos proves $0<G$ by direct application of mul_pos and div_pos to the positive factors lambda_rec_pos, c_pos and pi_pos.
proof idea
Tactic proof. Unfold gravitational_potential to reach -G M/r. Rewrite the expression to -(G M/r) by ring. Apply neg_lt_zero.mpr to the strictly positive quantity obtained from div_pos (mul_pos G_pos hM) hr.
why it matters
The theorem supplies the sign required for attractive gravity in the G-001 resolution that gravity is ledger curvature rather than a separate quantized force. It is a prerequisite for downstream statements on equivalence principle automaticity and large-scale structure scaling. The module addresses the registry question of the correct quantum theory of gravity by showing that the ledger already supplies both discrete small-scale states and continuous large-scale curvature from the same J-cost dynamics.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.