gravity_from_ledger_implies_kappa_pos
plain-language theorem explainer
Extracts the strict positivity of the RS-derived Einstein coupling from the gravity-from-ledger hypothesis bundle. Researchers deriving general relativity from the J-cost ledger invoke this to confirm that the gravitational constant remains positive once the eight-tick period is fixed. The proof is a one-line term projection onto the second conjunct of the input hypothesis.
Claim. Let κ denote the RS gravitational coupling. If the eight-tick period equals 8 and κ > 0, then κ > 0.
background
The module formalizes gravity as large-scale curvature of the ledger lattice induced by defect distributions, with the Einstein equations emerging in the continuum limit. The RS gravitational coupling is defined as κ = 8 φ^5, where φ is the self-similar fixed point from the Recognition Composition Law. The eight-tick period is the integration gap parameter forced by D = 3, appearing as the constant 8 in multiple upstream definitions.
proof idea
The proof is a one-line term that selects the second component of the bundled hypothesis pair.
why it matters
This declaration closes the positivity requirement inside the gravity-from-ledger bundle, supporting the claim that the Einstein field equations emerge with κ = 8 φ^5. It aligns with the eight-tick octave forced by spatial dimension D = 3 in the T0–T8 chain and with the module's G-002 registry item on the origin of the Einstein equations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.