RSMATStructural008Cert
plain-language theorem explainer
Certificate structure bundling three materials-domain cost facts: diagonal vanishing of domain cost, non-negativity on positive arguments, and positivity of the canonical threshold. Materials workers citing RS rung-spacing (adjacent rungs by factor φ) would reference it. Pure data bundle with no proof body; concrete inhabitants are assembled from sibling lemmas.
Claim. A materials structural certificate consists of three properties: (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.
background
Module RS_MAT_Structural_008 treats Recognition Science rung spacing in materials: adjacent rungs on the φ-ladder are separated by the golden ratio φ ≈ 1.618. Status is structural (zero sorry, zero axiom).
Domain cost is the materials-side cost functional on pairs of positive reals (mass-like and energy-like coordinates). Its diagonal vanishing says matched arguments carry zero excess cost; non-negativity mirrors the global recognition cost law. The canonical threshold is the positive cutoff used to separate structural regimes on that ladder.
Upstream, ObserverForcing records that every recognition event has nonnegative cost via J-cost non-negativity at positive state. The present certificate specializes that discipline to the materials domain cost and threshold.
proof idea
No proof body: this is a structure declaration, not a theorem. It packages three Prop fields that any inhabitant must supply. Downstream, the noncomputable value cert fills those fields by the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos; cert_inhabited then wraps that value as Nonempty.
why it matters
Gives a single named certificate type for Materials structural module 8 so downstream code can demand the three rung-spacing cost invariants together rather than piecemeal. Immediate consumers are the module's own cert definition and the inhabitation theorem cert_inhabited.
In the broader RS chain this sits under materials applications of the φ-ladder (T6 fixed point) and the non-negative J-cost discipline (T5 uniqueness of J). It does not itself force φ or D = 3; it only certifies the local cost and threshold facts needed for rung-spacing arguments in materials.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.