cert
plain-language theorem explainer
Packages three structural facts for the gap-45 module into one certificate: domain cost vanishes on the diagonal, stays nonnegative for positive mass and energy, and the canonical threshold is positive. Anyone citing the D=3 minimum-rung self-reference package uses this witness. The body is a pure structure assembly from three local lemmas.
Claim. There is a certificate bundling: (i) for every nonzero real $r$, the domain cost of $(r,r)$ is zero; (ii) for all positive mass $m$ and energy $e$, the domain cost of $(m,e)$ is nonnegative; (iii) the canonical threshold is strictly positive.
background
This module is Physics RS Structural 004. Its stated content is the gap-45 identity $D^2(D+2)=9\cdot 5=45$, read as the minimum rung for stable self-reference when spatial dimension is forced to $D=3$ (forcing chain T8). Status is structural: zero sorry, zero axioms.
The certificate type collects three properties of a local domain cost on pairs of reals (mass/energy style arguments) together with a positive canonical threshold. Domain cost is the module's specialization of recognition cost; upstream, recognition-event cost is already known nonnegative via the J-cost nonnegativity lemma (0 \le J on positive states). Vanishing on the diagonal means equal arguments incur zero domain cost, the identity/minimum locus.
Sibling facts supply the three fields: diagonal vanishing, nonnegativity for positive inputs, and positivity of the canonical threshold.
proof idea
One-line structure construction. The definition inhabits RSPHYStructural004Cert by assigning the three existing local lemmas: diagonal vanishing of domain cost, nonnegativity of domain cost on positive mass and energy, and positivity of the canonical threshold. No new arithmetic is performed here.
why it matters
Gives a single named witness that the gap-45 structural package's cost and threshold side-conditions hold. In the Recognition framework this sits under the D=3 forcing (T8) and the eight-tick/octave counting that makes $D^2(D+2)=45$ the minimum self-reference rung. Downstream edges are empty in the graph snapshot, so the certificate is presently a module-level export rather than an intermediate lemma in a longer proof chain. It closes the structural theorem claim of the module (0 sorry, 0 axiom) by bundling the cost-interface obligations in one place.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.