cert
plain-language theorem explainer
Packages the three structural facts of materials module 7 into a single certificate: domain cost vanishes on equal arguments, is nonnegative for positive mass and energy, and the canonical threshold is positive. Materials and recognition-cost auditors cite it as the inhabited witness that J-cost ratio symmetry is in place. The body is a pure structure instance wiring three already-proved sibling lemmas.
Claim. There is a certificate recording that (i) for every nonzero real $r$, the domain cost of $(r,r)$ is zero; (ii) for all positive reals $m,e$, the domain cost of $(m,e)$ is nonnegative; and (iii) the canonical threshold is strictly positive.
background
Materials structural module 7 records the ratio symmetry of the Recognition Science J-cost: $J(x)=J(1/x)$. In RS-native units the cost of a recognition event is built from $J$, which is nonnegative and vanishes only at the identity $x=1$. The module introduces a domain-level cost on pairs of positive reals (mass and energy scales) together with a canonical positive threshold used as a comparison scale.
The certificate structure bundles three obligations: vanishing of domain cost when the two arguments agree and are nonzero; nonnegativity of domain cost on the positive quadrant; and positivity of the canonical threshold. Upstream, the foundation result that every recognition-event cost is nonnegative (via $J\ge 0$) supplies the conceptual template for the domain-level nonnegativity clause.
proof idea
One-line structure instance. The three fields of the certificate are filled by the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos respectively; no further tactic work is required.
why it matters
Gives a single named witness that the J-cost ratio-symmetry package for materials is fully discharged (module status: structural theorem, zero sorry, zero axiom). Downstream consumers can take the certificate rather than re-proving vanishing-on-diagonal, nonnegativity, and threshold positivity separately. In the broader forcing chain this sits under the T5 J-uniqueness landmark $J(x)=(x+x^{-1})/2-1$, which already forces $J(x)=J(1/x)$; the certificate is the materials-side packaging of that symmetry. No used-by edges are recorded yet, so the immediate role is local inhabitance (cert_inhabited) and audit completeness for the materials domain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.