StructMaterialsM63Cert
plain-language theorem explainer
Certificate bundle for Recognition Science structural materials predictions at recognition rung 63. It packages three properties: domain cost vanishes on the diagonal, is nonnegative for positive mass/energy arguments, and the canonical threshold is strictly positive. Anyone citing the RS materials structural claim at this rung references this type. Pure structure definition; no proof body.
Claim. A materials-domain structural certificate at recognition rung 63 is a triple of facts: (i) the domain cost satisfies $C(r,r)=0$ for every real $r\neq 0$; (ii) $C(m,e)\ge 0$ whenever $m>0$ and $e>0$; (iii) the canonical threshold $T$ obeys $T>0$.
background
The module states a structural RS prediction for the Materials domain at recognition rung 63 (Plan v7, 120th pass), with status structural theorem: zero sorry, zero axiom. Local cost is a domain-specialized real function domainCost on pairs of reals (mass- and energy-like arguments), not the raw recognition-event cost.
Upstream, the foundation lemma cost_nonneg asserts that every recognition event has nonnegative cost, via nonnegativity of the J-cost on positive states. The materials certificate lifts that spirit to a two-argument domain cost and adds a diagonal-vanishing identity plus a positive threshold constant canonicalThreshold used as a decision cut in the materials layer.
Sibling lemmas in the same module discharge the three fields: diagonal identity, nonnegativity for positive arguments, and positivity of the threshold. The structure only names the interface those lemmas inhabit.
proof idea
No proof body: this is a structure (record type) with three propositional fields. Inhabitation is deferred to the downstream definition that fills the fields with domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos. The type itself only constrains what a valid materials rung-63 certificate must assert.
why it matters
Gives the typed interface for the Materials structural certificate at rung 63. Downstream, cert builds a concrete inhabitant by wiring the three sibling lemmas into the fields, and cert_inhabited records Nonempty of that type, closing the module's structural claim.
In the RS stack this is bookkeeping for a domain-level structural theorem rather than a forcing-chain step (T5–T8) or an RCL identity. It ties materials predictions to the same nonnegative-cost discipline as observer forcing, specialized to rung 63 on the phi-ladder materials track. No open scaffold remains in this module once cert is defined.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.