gravity_not_force_mediated
plain-language theorem explainer
Gravity is classified as emergent rather than force-mediated: the RS gravitational coupling is strictly positive. Anyone citing the no-graviton certificate or registry item G-004 needs this fact. The proof is a one-line identification with the already-proved positivity of the zero-parameter coupling κ_rs = 8φ⁵.
Claim. Gravity is emergent in the Recognition Science sense: the zero-parameter gravitational coupling satisfies $\kappa_{\mathrm{rs}} > 0$.
background
In Recognition Science, gravity is not a fundamental force carried by a gauge boson. This module formalizes registry item G-004 ("Is there a graviton?") by treating that question as a category error: gravity is large-scale curvature of the ledger lattice, like asking which particle mediates temperature.
The predicate that gravity is emergent is defined as the strict positivity of the zero-parameter coupling $\kappa_{\mathrm{rs}}$. Upstream, ZeroParameterGravity sets $\kappa_{\mathrm{rs}} = 8\phi^5$ and proves $\kappa_{\mathrm{rs}} > 0$ from $\phi > 0$ together with the constant factor 8. The coupling is algebraic in the golden ratio alone; no gauge-group generator enters.
proof idea
One-line term proof. The claim is definitionally the positivity statement $0 < \kappa_{\mathrm{rs}}$, which is exactly the upstream lemma ZeroParameterGravity.kappa_pos. That lemma unfolds $\kappa_{\mathrm{rs}} = 8\phi^5$, then applies mul_pos with a numeric check that $8 > 0$ and pow_pos on $\phi^5$.
why it matters
Supplies the emergent field of the bundled certificate no_graviton_cert, alongside algebraic coupling-from-φ, two GW polarizations, and a positive BMV rate. Anchors the RS answer to G-004: no separate graviton quantum is required, because the coupling is a number-theoretic consequence of the cost function (tied to T5 J-uniqueness and φ forced at T6), not a gauge coupling. Marks the fork between emergent ledger curvature and particle-mediated gravity; the sibling BMV prediction $\kappa_{\mathrm{rs}} \approx 88.7$ is the experimental discriminator.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.