cert
plain-language theorem explainer
Packages three proved properties of the materials domain cost (diagonal vanishing, nonnegativity, positive threshold) into the module-6 structural certificate. Materials and RS-forcing readers cite it as the inhabited witness that the local cost interface is well-formed. Construction is a pure field wiring of three sibling lemmas; no new algebra.
Claim. There is a materials structural certificate whose three fields hold: for every nonzero real $r$, the domain cost at $(r,r)$ is zero; for all positive reals $m,e$ the domain cost at $(m,e)$ is nonnegative; and the canonical threshold is strictly positive.
background
Module 6 of the materials structural layer records the RS claim that $\varphi$ is the unique self-similar fixed point of the continued fraction $1+1/(1+1/(\cdots))$, status structural (zero sorry, zero axiom). The local cost interface is a real bivariate domainCost together with a positive real canonicalThreshold.
The certificate structure demands three facts: the cost vanishes on the diagonal away from zero, stays nonnegative on the positive quadrant, and the threshold is positive. Upstream, nonnegativity of recognition cost is already known in the observer-forcing layer: every recognition event has cost $\ge 0$ because the $J$-cost is nonnegative on positive states. The materials lemmas specialize that pattern to the domain cost used here.
proof idea
Pure structure instance. The three fields are filled by the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos respectively. No tactics, no rewriting, no new inequalities: just name the already-proved components.
why it matters
Gives an inhabited certificate object for Materials Structural Module 6, so downstream code can depend on a single bundled witness rather than three separate lemmas. The module sits on the $\varphi$-uniqueness story (forcing-chain T6: $\varphi$ as the self-similar fixed point). No used_by edges are recorded yet; the natural consumer is any materials theorem that assumes the cost interface is certified before deriving thresholds or selection rules. Closes the local packaging step with zero sorry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.