RSMATStructural002Cert
plain-language theorem explainer
Certificate structure bundling three structural properties of the materials-domain recognition cost: it vanishes on equal nonzero arguments, stays nonnegative for positive mass and energy, and the canonical threshold is positive. Materials work citing the golden-ratio J-cost minimum uses this bundle as the formal interface. Pure structure definition; inhabitance is discharged by a separate cert instance.
Claim. A materials structural certificate is a triple of facts: (i) for every real $r \neq 0$, the domain cost satisfies $C(r,r)=0$; (ii) for all $m,e>0$, one has $C(m,e)\ge 0$; (iii) the canonical threshold $T$ obeys $T>0$.
background
This module is Materials RS Structural Module 2. Its stated setting is the RS J-cost minimum at the golden ratio: $J(\varphi)=\varphi-3/2\approx 0.11803$, the recognition cost of $\varphi$. Status is structural (zero sorry, zero axiom).
The domain cost $C(m,e)$ is the materials-side cost functional on a mass-like and energy-like pair of positive reals (siblings domainCost, domainCost_at_eq, domainCost_nonneg). The canonical threshold is a fixed positive scale used as a cutoff in the same module (canonicalThreshold, canonicalThreshold_pos).
Upstream, recognition costs are already known to be nonnegative: ObserverForcing records that every recognition event has cost $\ge 0$, via nonnegativity of the J-cost on positive states. The present certificate lifts that nonnegativity pattern into an explicit materials interface, together with a diagonal-vanishing identity and a positive threshold.
proof idea
No proof body: this is a structure whose three fields are propositions. Inhabitance is not claimed here. Downstream, cert fills the fields by the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos, and cert_inhabited packages that instance as Nonempty.
why it matters
Gives the typed interface that Materials RS Structural Module 2 must satisfy before any materials claim can cite the golden-ratio cost minimum. Downstream, cert is the concrete witness and cert_inhabited proves the type is nonempty, closing the structural obligation with zero sorry.
In the broader RS chain this sits under the J-cost uniqueness story (T5: $J(x)=(x+x^{-1})/2-1$) and the forced self-similar fixed point $\varphi$ (T6). The module headline $J(\varphi)=\varphi-3/2$ is the materials-facing evaluation of that minimum away from the identity $x=1$. The certificate does not derive $\varphi$ or $J$; it only freezes the cost and threshold properties materials lemmas are allowed to assume.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.