cert
plain-language theorem explainer
Packages three structural facts about the materials domain cost into one certificate: the cost vanishes on the diagonal, stays nonnegative for positive arguments, and the canonical threshold is positive. Materials and ladder-spacing arguments cite this as the single witness that the rung-cost is well-posed. The body is a pure structure assembly wiring three already-proved sibling lemmas.
Claim. There is a materials structural certificate whose three fields assert: (i) for every nonzero real $r$, the domain cost at $(r,r)$ is zero; (ii) for all positive reals $m,e$, the domain cost at $(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 differ by the golden ratio $\varphi = 1.618\ldots$. Status is structural (zero sorry, zero axiom).
The domain cost is the local cost functional on mass/energy-like reals used to score rung mismatch. Its diagonal vanishing and nonnegativity mirror the global J-cost facts from the forcing chain (T5 uniqueness of $J(x)=(x+x^{-1})/2-1$, and nonnegativity of recognition-event cost). The canonical threshold is the positive cutoff against which domain-cost values are compared.
Upstream, cost_nonneg in ObserverForcing states that every recognition event has nonnegative cost via $J$-cost nonnegativity. The certificate structure simply records the three materials-side analogues as a single inhabited record.
proof idea
Pure definitional assembly of the certificate structure. The three fields are filled by the sibling lemmas already proved in-module: diagonal vanishing (domainCost_at_eq), nonnegativity for positive arguments (domainCost_nonneg), and positivity of the canonical threshold (canonicalThreshold_pos). No extra tactics or algebraic work; the def is the witness.
why it matters
Gives a single named inhabitant of the materials structural certificate so downstream materials lemmas can assume one object rather than three separate hypotheses. Sits in the structural layer of RS materials (rung factor $\varphi$), consistent with T6 ($\varphi$ as self-similar fixed point) and the phi-ladder mass formula. No used_by edges are recorded yet; the natural consumer is the sibling inhabitance fact and any later materials theorem that needs a bundled well-posedness witness for domain cost. Closes no open scaffold; it is the concrete certificate value itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.