kappa_ne_zero
plain-language theorem explainer
The Einstein gravitational constant derived from the J-cost ledger cannot vanish. Researchers deriving gravity as continuum curvature from defect distributions would cite this to ensure the coupling is well-defined. The proof is a one-line term applying the positivity fact to conclude nonvanishing.
Claim. The Einstein gravitational constant $κ_{RS}$ obtained from the unique J-cost function satisfies $κ_{RS} ≠ 0$.
background
The Zero-Parameter Gravity module derives gravity from the J-cost framework: defects in the ledger lattice induce large-scale curvature, with the Einstein equations as the continuum limit. The J-cost is the unique solution to the Recognition Composition Law, given by $J(x) = ½(x + x^{-1}) - 1$, symmetric about its minimum at $x=1$. The constant $κ$ equals $8φ^5$ in RS-native units where $c=1$, $ℏ=φ^{-5}$. Upstream constants supply the RS form of Newton's $G = λ_{rec}^2 c^3 / (π ℏ)$ and the log-reparametrization of the functional equation.
proof idea
One-line term proof that applies ne_of_gt directly to the positivity result for the RS coupling.
why it matters
This result secures the nonzero coupling required for the Einstein field equations as the continuum limit of ledger curvature (G-002). It supports the automatic equivalence principle (G-003) because inertial and gravitational mass both arise from the same J-cost, with no room for a vanishing factor. The declaration closes a degeneracy that would otherwise collapse the zero-parameter derivation of gravity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.