RSMATStructural001Cert
plain-language theorem explainer
Certificate bundle of three structural properties for the materials-domain cost: it vanishes when both arguments agree and are nonzero, it is nonnegative on positive arguments, and the canonical threshold is strictly positive. Materials workers citing RS structural predictions (J-cost, forced D=3) would reference this bundle. It is a pure structure definition; inhabitation is supplied separately by the concrete cert value.
Claim. A materials structural certificate is a triple of facts: (i) for every nonzero real $r$, the domain cost satisfies $C(r,r)=0$; (ii) for all positive reals $m,e$, one has $C(m,e)\ge 0$; (iii) the canonical threshold $T$ obeys $T>0$.
background
The module states an RS structural prediction for materials: the cost is the standard J-form $J(x)=\frac12(x+1/x)-1$, with $\varphi$ the golden ratio and spatial dimension $D=3$ forced. Status is structural theorem (zero sorry, zero axiom).
domainCost is the materials-side cost functional on pairs of positive reals (mass- and energy-like arguments), built from that J-cost. The diagonal identity $C(r,r)=0$ is the cost minimum at matched arguments, matching the classical fact that $J(1)=0$. Nonnegativity of cost is the materials analogue of the foundation result that every recognition event has nonnegative cost (cost_nonneg in ObserverForcing: "The cost of any recognition event is non-negative").
canonicalThreshold is the positive cutoff used downstream as a materials decision or stability bound; its positivity is packaged here rather than proved in isolation.
proof idea
No proof body: this is a structure declaration. The three fields are Prop-valued hypotheses naming the diagonal vanishing law, the nonnegativity law, and threshold positivity. Inhabitation is not claimed here; the sibling definition cert fills the fields with domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos, and cert_inhabited then exhibits Nonempty via that value.
why it matters
Gives a single named certificate type for the first materials structural module, so downstream code can depend on one object rather than three loose lemmas. Immediate consumers are cert (the concrete inhabitant) and cert_inhabited (nonemptiness). Sits under the module claim that J-cost, $\varphi$, and $D=3$ are forced structural content (T5 J-uniqueness, T6 $\varphi$ fixed point, T8 dimension forcing in the primer chain). Does not itself advance mass ladders or $\alpha$-band numerics; it only freezes the cost-and-threshold interface those later materials results expect.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.