RSMATStructural006Cert
plain-language theorem explainer
Certificate bundle for Materials structural module 6 (phi as self-similar fixed point): domain cost vanishes on the diagonal, is nonnegative for positive arguments, and the canonical threshold is positive. Downstream code cites it to build a concrete inhabited instance. Pure structure definition; the three fields are discharged by sibling lemmas.
Claim. A certificate packing three claims: (i) for every nonzero real $r$, the domain cost of $(r,r)$ is zero; (ii) for all positive reals $m,e$, the domain cost of $(m,e)$ is nonnegative; (iii) the canonical threshold is strictly positive.
background
Module RS_MAT_Structural_006 is the materials-side structural package for RS phi uniqueness: $\varphi$ as the self-similar fixed point $\varphi=1+1/(1+1/(1+\cdots))$. Status is structural theorem (zero sorry, zero axiom).
The certificate refers to a domain cost on pairs of reals (materials mass/energy style arguments) and a canonical threshold scalar. Nonnegativity of recognition cost is the upstream pattern: ObserverForcing records that every recognition event has nonnegative cost via $J$-cost nonnegativity at positive state.
Sibling lemmas in the same module supply the three field proofs: diagonal vanishing, domain-cost nonnegativity under positive inputs, and positivity of the canonical threshold.
proof idea
No proof body: this is a structure declaration. The three fields are Prop-valued requirements. Inhabitation is deferred to the sibling cert definition, which fills the fields by domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos. Upstream cost_nonneg on recognition events is the conceptual ancestor of the nonnegativity field, not a direct tactic step here.
why it matters
Gives a single named bundle for the structural side-conditions of materials module 6 so downstream code can demand one object rather than three loose lemmas. Used by the concrete cert instance and by cert_inhabited (Nonempty of the certificate). Sits under the module claim that phi uniqueness is a structural theorem. Ties to the forcing-chain landmark T6 (phi forced as self-similar fixed point) and to the general RS cost calculus ($J$-cost nonnegative, identity at ratio 1). Does not itself force phi; it packages cost/threshold hygiene the materials layer expects when that uniqueness is in play.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.