cert
plain-language theorem explainer
Certificate packing three structural properties of the materials domain cost: vanishing on the diagonal, non-negativity for positive arguments, and a strictly positive canonical threshold. Materials workers citing the golden-ratio J-cost minimum use this bundle as a single witness. The definition is a pure structure instance that wires three already-proved sibling lemmas into the certificate fields.
Claim. A materials 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$ and $e$, the domain cost of $(m,e)$ is nonnegative; (iii) the canonical threshold is strictly positive. The declaration supplies one such certificate by assembling those three properties.
background
Module RS_MAT_Structural_002 treats the Recognition Science J-cost minimum at the golden ratio: $J(\varphi)=\varphi-3/2\approx 0.11803$. Status is structural (zero sorry, zero axiom). In RS the cost functional is $J(x)=(x+x^{-1})/2-1$, forced unique by the T5 step of the unified forcing chain and obeying the Recognition Composition Law.
The certificate structure packages three domain-level properties of a materials cost domainCost: diagonal vanishing (equal mass and energy arguments cost nothing), non-negativity on the positive quadrant, and positivity of a canonical threshold used as a materials cutoff. Upstream, the foundation lemma cost_nonneg already records that every recognition event has nonnegative cost via Jcost_nonneg.
Sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos discharge the three fields; this declaration only assembles them.
proof idea
Pure structure instance, not a tactic proof. The three certificate fields are filled by direct assignment: diagonal vanishing from domainCost_at_eq, non-negativity from domainCost_nonneg, and threshold positivity from canonicalThreshold_pos. No further rewriting or case analysis occurs.
why it matters
Gives a single named witness that the materials domain cost obeys the structural axioms expected of an RS J-cost: zero on matched arguments, nonnegative off-diagonal, and a positive threshold. That matches the module claim that the golden-ratio recognition cost $J(\varphi)=\varphi-3/2$ is the structural minimum. No downstream consumers are recorded yet; the natural parent is any materials theorem that assumes an RSMATStructural002Cert rather than the three lemmas separately. Lands in the Materials domain of the RS mirror and sits downstream of the foundation non-negativity fact for recognition costs (T5 J-uniqueness background).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.