cert
plain-language theorem explainer
Packages three materials-domain cost facts into one certificate: the domain cost vanishes on the diagonal, is nonnegative for positive arguments, and the canonical threshold is strictly positive. Materials or RS structural audits cite it as the inhabited witness for the module's structural claims. The definition is a pure field assembly of three already-proved lemmas.
Claim. There is a materials structural certificate whose 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
This module records a Recognition Science structural prediction for materials: the cost is the unique $J$-form $J(x)=\frac12(x+1/x)-1$ (equivalently $\cosh(\log x)-1$), with $\varphi$ the golden ratio and spatial dimension $D=3$ forced. Status is a structural theorem block with no sorry and no extra axioms.
The certificate structure bundles three properties of a materials-domain cost functional domainCost relative to a positive canonicalThreshold. Diagonal vanishing says matched mass and energy scales carry zero domain cost. Nonnegativity is the materials-side shadow of the global fact that recognition cost is nonnegative (upstream: cost of any recognition event is $\ge 0$, via $J$-cost nonnegativity). The threshold field only demands positivity of the canonical cutoff used in the module.
Sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos discharge those three fields; this definition merely names the packed witness.
proof idea
One-line structure instance: assign cost_at_eq to the sibling lemma that domain cost vanishes on the diagonal, cost_nonneg to the sibling nonnegativity lemma for positive arguments, and threshold_pos to the sibling proof that the canonical threshold is positive. No extra algebra; pure packaging of three prior results.
why it matters
Gives an inhabited, named certificate for Materials RS Structural Module 1 so downstream material or forcing arguments can depend on a single object rather than three scattered lemmas. It sits on the $J$-uniqueness landmark (forcing-chain T5): domain cost is built so the diagonal minimum and nonnegativity match the unique $J$ solving the Recognition Composition Law. The module header also ties the same structural package to $\varphi$ and forced $D=3$ (T6, T8). No used_by edges are recorded yet; the immediate consumer is the sibling inhabitance fact and any later materials theorems that require a certified domain-cost witness. Closes no open scaffold; it is the concrete value inhabiting the certificate type.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.