RSMATStructural005Cert
plain-language theorem explainer
Certificate structure bundling three materials-domain cost axioms: domain cost vanishes on equal nonzero arguments, is nonnegative for positive mass/energy pairs, and the canonical threshold is strictly positive. Materials and structural-forcing consumers cite it as a single witness type. It is a pure structure definition; inhabitants are assembled elsewhere from sibling lemmas.
Claim. A structural certificate is a triple of facts: (i) for every nonzero real $r$, the domain cost of the pair $(r,r)$ equals zero; (ii) for all positive reals $m,e$, the domain cost of $(m,e)$ is nonnegative; (iii) the canonical threshold is strictly positive.
background
This module is Materials RS Structural Module 5. The local setting is the RS eight-tick: one complete traversal of the binary recognition lattice with period $2^D = 8$ (framework landmark T7). Status is structural theorem, zero sorry and zero axiom.
Domain cost is the materials-side cost functional on pairs of positive reals (mass/energy-like arguments). The first field demands it vanish on the diagonal away from zero, i.e. matched arguments carry zero cost. The second field is the materials analogue of the foundation fact that recognition cost is nonnegative: upstream, cost_nonneg states "The cost of any recognition event is non-negative," proved via nonnegativity of the J-cost on positive states. The third field asserts positivity of the module's canonical threshold (the cutoff used to separate structural regimes).
The structure does not compute these facts; it only packages their statement types so a single inhabitant can be passed downstream.
proof idea
No proof body: this is a structure declaration (definition). The three fields are Prop-valued requirements. An inhabitant is built in the sibling cert by assigning domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos to the three fields. Nonemptiness is then recorded by cert_inhabited as ⟨cert⟩.
why it matters
Gives the Materials layer a named certificate type for three structural cost properties tied to the eight-tick lattice (T7, period $2^3 = 8$). Downstream, cert is the concrete noncomputable inhabitant, and cert_inhabited proves Nonempty RSMATStructural005Cert, so later materials theorems can assume a single packed witness rather than three separate lemmas.
The nonnegativity field mirrors foundation ObserverForcing cost nonnegativity (J-cost minimum at the identity), keeping materials cost aligned with the Recognition Composition Law and T5 J-uniqueness. The diagonal-vanishing and positive-threshold fields fix the zero locus and the structural cutoff used in this module's regime splits. No open scaffold remains in this file; the certificate is fully discharged by the sibling lemmas.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.