cert
plain-language theorem explainer
Packages three structural facts about the gravity-domain recognition cost into a single certificate: the cost vanishes on the diagonal, stays nonnegative for positive mass and energy, and the canonical threshold is strictly positive. Gravity and RS auditors cite it as the inhabited witness for Structural Module 2. The body is a pure structure assembly of three already-proved sibling lemmas.
Claim. There is a certificate recording that the domain cost $C$ satisfies $C(r,r)=0$ for all $r\neq 0$, that $C(m,e)\ge 0$ whenever $m>0$ and $e>0$, and that the canonical threshold $T$ obeys $T>0$.
background
This module is Gravity RS Structural Module 2. Its stated content is the golden-ratio recognition cost: the RS $J$-cost attains its minimum at $\varphi$ with $J(\varphi)=\varphi-3/2\approx 0.11803$. Status is structural (zero sorry, zero axiom).
The certificate type bundles three properties of a domain cost $C(m,e)$ used in the gravity layer: diagonal vanishing $C(r,r)=0$ for $r\neq 0$; nonnegativity for positive mass and energy arguments; and positivity of a canonical threshold. Upstream, the foundation lemma cost_nonneg already records that every recognition-event cost is nonnegative via $J$-cost nonnegativity on positive states.
Sibling lemmas supply the three fields: diagonal identity of the domain cost, its nonnegativity on the positive quadrant, and positivity of the canonical threshold.
proof idea
One-line structure assembly. The definition inhabits RSGRVStructural002Cert by assigning the three fields to the sibling results domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos. No new algebra is performed; the certificate is just the packaged witness.
why it matters
Gives the inhabited structural certificate for Gravity Module 2, the layer that records the golden-ratio $J$-cost minimum $J(\varphi)=\varphi-3/2$. In the forcing chain this sits downstream of T5 ($J$-uniqueness, $J(x)=(x+x^{-1})/2-1$) and T6 ($\varphi$ as the self-similar fixed point). No downstream consumers are wired yet in the graph; the immediate sibling cert_inhabited is the natural use site. The certificate is the audit handle that the domain-cost axioms needed for later GRV structural claims are discharged without sorry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.