cert
plain-language theorem explainer
Packages three structural facts about the gravity domain cost into a single certificate: the cost vanishes on the diagonal, stays non-negative for positive mass and energy, and the canonical threshold is strictly positive. Gravity and RS structural auditors cite it as the inhabited witness for module 5. The body is a pure field-assembly of three already-proved sibling lemmas.
Claim. There is a certificate asserting: (i) for every nonzero real $r$, the domain cost of $(r,r)$ is zero; (ii) for all positive reals $m,e$, the domain cost of $(m,e)$ is nonnegative; (iii) the canonical threshold is strictly positive.
background
Module 5 of the RS gravity structural series records facts tied to the eight-tick octave: one full traversal of the binary recognition lattice has period $2^D = 8$ (forcing chain T7 with $D=3$). Status is structural: zero sorry, zero axioms.
The certificate type bundles three properties of a real-valued domain cost on mass/energy pairs. Diagonal vanishing says equal arguments carry zero cost. Non-negativity for positive arguments is the gravity-side shadow of the general fact that every recognition event has non-negative cost (via the J-cost $J(x)=(x+x^{-1})/2-1$). The third field only asks that a fixed positive threshold exist.
Upstream, cost_nonneg in ObserverForcing states that the cost of any recognition event is non-negative, proved from non-negativity of J-cost on positive states.
proof idea
One-line structure inhabitant. Each of the three fields is filled by the corresponding sibling lemma already proved in-module: diagonal vanishing by domainCost_at_eq, non-negativity by domainCost_nonneg, and positivity of the threshold by canonicalThreshold_pos. No extra algebra or case splits occur at this site.
why it matters
Gives the inhabited structural certificate for Gravity RS module 5, the eight-tick structural layer (period $2^3=8$, T7). Downstream consumers that need a single named witness for diagonal cost vanishing, cost non-negativity, and a positive threshold can take this value rather than reassemble the three lemmas. No further used-by edges are recorded yet; the companion cert_inhabited sibling is the natural next step that turns the definition into an existence fact. Lands inside the structural (not dynamical) half of the RS gravity stack.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.