RSGRVStructural008Cert
plain-language theorem explainer
Certificate bundle for RS gravity structural module 8 (phi rung spacing). It packages three facts: domain cost vanishes on the diagonal, domain cost is nonnegative for positive arguments, and the canonical threshold is positive. Downstream code inhabits the bundle via the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos. Pure structural packaging with no proof body.
Claim. A certificate for RS gravity structural module 8 is a triple of properties: (i) the domain cost vanishes on the diagonal, $\mathrm{cost}(r,r)=0$ whenever $r\neq 0$; (ii) $\mathrm{cost}(m,e)\ge 0$ for all $m>0$ and $e>0$; (iii) the canonical threshold is strictly positive.
background
Module 8 of the RS gravity structural series treats rung spacing on the Recognition ladder: adjacent rungs differ by the golden ratio $\varphi\approx 1.618$, the self-similar fixed point forced at T6. The module is marked structural (zero sorry, zero axiom).
The domain cost is the two-argument cost used to compare mass and energy (or radius) parameters in this gravity setting. It is built from the Recognition J-cost $J(x)=(x+x^{-1})/2-1$, whose nonnegativity is classical: upstream, cost_nonneg states that every recognition event has nonnegative cost, via $J\ge 0$ for positive states.
The canonical threshold is the positive cutoff against which that cost is compared when deciding structural admissibility of a rung configuration. The three fields of this structure are exactly the algebraic facts needed to treat that comparison as well-posed.
proof idea
No proof: this is a structure declaration. It names three Prop-valued fields (diagonal vanishing, nonnegativity, threshold positivity) and nothing else. Inhabitation is deferred to the sibling definition cert, which fills the fields by domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos.
why it matters
Gives a single named type for the structural obligations of gravity module 8, so later gravity lemmas can depend on one certificate rather than three scattered hypotheses. Downstream, cert builds a concrete inhabitant and cert_inhabited records Nonempty of the type, closing the module's structural claim.
In the forcing chain this sits under T6 ($\varphi$ as self-similar fixed point) and the mass/rung ladder (yardstick times $\varphi^{\mathrm{rung}-8+\mathrm{gap}(Z)}$). The nonnegativity field is the gravity-side shadow of the global J-cost nonnegativity used throughout Recognition Science. The module claims full structural discharge (0 sorry); this certificate is the packaging step that makes that claim checkable.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.