cert
plain-language theorem explainer
Packages three already-proved gravity-domain facts into a single structural certificate: the domain cost vanishes on the diagonal, is nonnegative for positive mass and energy, and the canonical threshold is strictly positive. Gravity and RS auditors cite it as the inhabited witness that Module 1's structural claims hold with zero sorry. Construction is a three-field structure literal wiring sibling lemmas.
Claim. There is an inhabited structural certificate whose fields assert: (i) for every nonzero real $r$, the domain cost at $(r,r)$ is zero; (ii) for all positive mass $m$ and energy $e$, the domain cost $\mathrm{domainCost}(m,e)$ is nonnegative; (iii) the canonical threshold is strictly positive.
background
This module records the first RS structural gravity package: the cost functional is the unique $J(x)=\frac12(x+1/x)-1$ (equivalently $\cosh(\log x)-1$), with $\varphi$ the golden ratio and $D=3$ forced by the T5–T8 chain. Status is structural theorem (zero sorry, zero axiom).
The certificate structure bundles three domain-level properties of a real-valued cost on mass–energy pairs. Diagonal vanishing says equal arguments incur zero cost (identity recognition). Nonnegativity is the gravity-side restatement of the global fact that every recognition event has nonnegative cost, which upstream is proved by reducing to $J$-cost nonnegativity on positive states. The canonical threshold is a positive real cutoff used as a structural scale in the gravity layer.
Sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos already establish the three fields; this definition only names the bundled witness.
proof idea
One-line structure inhabitant. The three fields are filled by direct assignment to the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos. No new algebra: the definition is pure packaging of prior proofs into RSGRVStructural001Cert.
why it matters
Gives the named, inhabited certificate that Module 1's structural gravity claims are discharged. Downstream consumers (none yet linked in the graph) can take a single term rather than three separate lemmas when they need diagonal vanishing, cost nonnegativity, and a positive threshold together.
In the RS forcing chain this sits under the gravity reading of T5 $J$-uniqueness and the nonnegative cost law from ObserverForcing. It does not itself force $\varphi$ or $D=3$; those are ambient module claims. It closes the local "certificate inhabited" obligation for RS_GRV_Structural_001 and pairs with the sibling cert_inhabited fact.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.