cert
plain-language theorem explainer
Packages three elementary domain-cost facts (vanishes on the diagonal, nonnegative for positive arguments, positive canonical threshold) into one certificate for Foundation RS Module 1. Anyone wiring the structural forcing chain or checking the recognition lattice setup would cite it. Construction is a pure field assignment of three already-proved sibling lemmas; no new mathematics.
Claim. There is a certificate consisting of: (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
Foundation RS Module 1 packages the recognition lattice: all physical predictions are to derive from the J-cost $J(x)=\frac12(x+1/x)-1$ (equivalently $\cosh(\log x)-1$), with zero sorry and zero axioms. The module status is structural theorem.
Domain cost is the local cost functional on pairs of positive reals (measure vs expectation) built from that J. The certificate structure demands three properties: cost vanishes when the two arguments agree and are nonzero; cost is nonnegative on the positive quadrant; and a fixed positive threshold (the canonical recognition threshold) sits above zero.
Upstream, nonnegativity of recognition-event cost is already known from ObserverForcing: "The cost of any recognition event is non-negative," via $J$-cost nonnegativity on positive states. The three field witnesses here are the in-module lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos.
proof idea
Pure structure inhabitation. The definition assigns the three required fields of the certificate structure to the corresponding sibling lemmas: diagonal vanishing to the domain-cost-at-equality lemma, nonnegativity to the domain-cost nonnegativity lemma, and threshold positivity to the canonical-threshold positivity lemma. No tactics, no rewriting, no new proof obligations.
why it matters
This is the inhabited certificate object for Foundation RS Module 1, the first structural block of the RS forcing chain. The module claims a recognition lattice with zero sorry and zero axiom, grounded in the unique J-cost (forcing-chain landmark T5: $J(x)=(x+x^{-1})/2-1$).
Downstream use is not yet wired in this graph (no used_by edges), but the sibling cert_inhabited and any later chain assembler that requires an RSForcingChain001Cert instance will consume it. It does not itself force $\varphi$, the eight-tick octave, or $D=3$; those are later T6–T8 steps. Its job is only to freeze the elementary cost and threshold facts into a single named witness so the structural theorem status of the module is checkable.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.