kappa_ne_zero
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not compute the explicit numerical value of the coupling.
- Does not incorporate quantum corrections or higher-order terms.
- Does not derive the constant from observational data.
- Does not address possible modifications outside the J-cost ledger.
formal statement (Lean)
51theorem kappa_ne_zero : kappa_rs ≠ 0 := ne_of_gt kappa_pos
proof body
Term-mode proof.
52
53/-! ## The Equivalence Principle -/
54
55/-- **G-003 Resolution**: The equivalence principle is automatic.
56
57 In RS, all mass comes from J-cost defect. Both "inertial mass"
58 (resistance to state change, from J''(1) = 1) and "gravitational mass"
59 (source of curvature, from J(x) itself) are computed from the SAME
60 unique cost function J(x) = ½(x + x⁻¹) − 1.
61
62 Since J is the unique solution to the RCL (T5), there is only one
63 notion of mass. The equivalence principle is forced by cost uniqueness.
64
65 The formal content: J is symmetric (J(x) = J(1/x)), has unique minimum
66 at x = 1, and its second derivative J''(1) = 1 is universal — the same
67 for ALL bodies regardless of composition. This universality IS the EP.
68
69 See also: EquivalencePrinciple.lean for the SingleSourceMassTheory
70 formalization and the rs_equivalence_principle theorem. -/