cert
plain-language theorem explainer
Packages three structural facts about the materials domain cost into a single certificate: the cost vanishes on the equal-argument diagonal, stays nonnegative for positive mass and energy, and the canonical threshold is strictly positive. Materials and lattice-period arguments cite this bundle rather than the three lemmas separately. The definition is a pure structure inhabitant that wires those lemmas into the certificate fields.
Claim. There is a materials structural 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
This module is Materials RS Structural Module 5. It sits in the eight-tick setting: period $2^D = 8$, one full traversal of the binary recognition lattice (forcing-chain landmark T7). Status is structural theorem with no sorry and no axioms.
The certificate type collects three properties of the materials domain cost. Domain cost is the local cost functional on mass/energy-type arguments used in this materials layer; it is built from the Recognition Science $J$-cost $J(x) = (x + x^{-1})/2 - 1$. Upstream, nonnegativity of recognition-event cost is already known: any recognition event has nonnegative cost via $J$-cost nonnegativity on positive states.
Sibling facts supply the three fields: domain cost equals zero when both arguments match and are nonzero; domain cost is nonnegative on the positive quadrant; and the canonical threshold (the cutoff used for structural comparisons in this module) is positive.
proof idea
One-line structure inhabitant. The definition fills RSMATStructural005Cert by assigning the three preexisting lemmas to the three fields: diagonal vanishing from domainCost_at_eq, nonnegativity from domainCost_nonneg, and threshold positivity from canonicalThreshold_pos. No new algebra is performed; the proof is pure packaging.
why it matters
Gives a single named certificate that downstream materials arguments can assume instead of re-proving diagonal vanishing, cost nonnegativity, and threshold positivity. The module frames this as part of the eight-tick structural layer (period $2^3 = 8$), so the certificate is the local witness that the materials domain cost behaves like a genuine recognition cost on the lattice period.
No used_by edges are recorded yet, so the immediate consumers are sibling inhabitants such as cert_inhabited and any later materials theorems that take an RSMATStructural005Cert hypothesis. It closes the structural packaging step for Module 5 rather than advancing a new forcing-chain link; the physics content remains the T7 eight-tick octave and the $J$-cost nonnegativity inherited from observer forcing.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.