cert
plain-language theorem explainer
Packages three already-proved facts into the structural certificate for materials gap-45: domain cost vanishes on the equal-argument diagonal, stays nonnegative for positive mass and energy, and the canonical threshold is strictly positive. Materials and RS-structure auditors cite it as the inhabited witness that Module 4 is closed. The body is a pure structure instance, wiring sibling lemmas into the certificate fields.
Claim. There is a certificate asserting: (i) for every nonzero real $r$, the domain cost at $(r,r)$ is zero; (ii) for all positive reals $m,e$, the domain cost at $(m,e)$ is nonnegative; (iii) the canonical threshold is strictly positive.
background
Module RS_MAT_Structural_004 records the materials gap-45 fact: at spatial dimension $D=3$, the combination $D^2(D+2)=9\cdot 5=45$ is the minimum rung for stable self-reference. Status is structural (zero sorry, zero axiom).
The certificate structure bundles three properties of a domain cost functional on pairs of reals: vanishing when the two arguments coincide (and are nonzero), nonnegativity for positive arguments, and positivity of a fixed canonical threshold. Domain cost is the materials-side specialization of the Recognition Science J-cost; upstream, ObserverForcing already records that every recognition-event cost is nonnegative via $J$-cost nonnegativity.
Sibling lemmas in the same module discharge each field: equality on the diagonal, nonnegativity off-diagonal, and positivity of the threshold constant.
proof idea
One-line structure instance. The three certificate fields are filled by the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos respectively. No new algebra is performed; the definition only witnesses that those three facts inhabit the certificate structure.
why it matters
Closes the certificate side of Materials Structural Module 4 (gap-45). In the RS forcing chain, $D=3$ is T8 and the eight-tick octave is T7; gap-45 is the materials reading of the minimal self-reference rung once those are fixed. The certificate makes the three cost/threshold obligations a single named witness, so downstream materials arguments can assume the package rather than re-prove diagonal vanishing, nonnegativity, and threshold positivity. No used-by edges are recorded yet; the natural consumer is any theorem that needs an inhabited gap-45 structural certificate (e.g. the sibling inhabitedness lemma).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.