gravity_from_ledger_implies_kappa_ne_zero
plain-language theorem explainer
Gravity-from-ledger excludes a vanishing Einstein coupling. Researchers deriving general relativity from discrete recognition lattices cite the result to rule out the degenerate case κ=0. The proof is a one-line term that applies ne_of_gt directly to the positivity conjunct of the hypothesis.
Claim. If the eight-tick period equals 8 and the RS gravitational coupling satisfies $0 < 8φ^5$, then $8φ^5 ≠ 0$.
background
The Zero-Parameter Gravity module derives the Einstein field equations as the continuum limit of curvature on the ledger lattice induced by defect distributions. The coupling is fixed without free parameters as κ_RS = 8 φ^5, where φ is the self-similar fixed point of the J-cost functional equation. The eight_tick constant is forced to 8 by the requirement that D=3 spatial dimensions close the recognition cycle (2^D=8).
proof idea
The declaration is a one-line term proof that applies ne_of_gt to the second conjunct of the hypothesis, which asserts 0 < kappa_rs. The upstream definition kappa_rs := 8 * phi ^ 5 supplies the positivity needed for the inequality.
why it matters
This result closes the positivity argument inside the gravity-from-ledger bundle and supports G-002 by ensuring the derived Einstein coupling cannot vanish. It relies on the eight-tick octave (T7) and D=3 (T8) from the forcing chain, confirming that the lattice construction produces a viable nonzero κ inside the predicted numerical band.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.