cert
plain-language theorem explainer
A packaged certificate that the module-5 domain cost vanishes on the diagonal, stays non-negative for positive arguments, and that the canonical threshold is strictly positive. Forcing-chain auditors cite it as the single inhabitant of the Module 5 structural certificate. The body is a three-field structure instance wiring in the already-proved sibling lemmas.
Claim. There is a certificate recording three facts: for every nonzero real $r$, the domain cost of $(r,r)$ is zero; for all positive reals $m,e$, the domain cost of $(m,e)$ is nonnegative; and the canonical threshold is strictly positive.
background
Module 5 sits in the RS forcing chain T0–T8, the structural spine that forces the J-cost, $\varphi$, the eight-tick octave, and $D=3$ with zero sorry. The local certificate type bundles three elementary cost facts needed before later chain steps can treat the domain cost as a genuine recognition cost.
Domain cost is the module’s working cost on pairs of positive reals (imported from the Cost layer and specialized here). The first field demands that equal arguments give cost zero, i.e. the diagonal is the identity locus. The second demands non-negativity off the diagonal for positive inputs, matching the upstream ObserverForcing fact that “the cost of any recognition event is non-negative.” The third demands that the module’s canonical threshold (the positive cutoff used to separate trivial from nontrivial recognition) is strictly positive.
Together these three propositions are exactly the fields of RSForcingChain005Cert; the definition below is the concrete witness.
proof idea
Pure structure construction, not a tactic proof. Each field is filled by the corresponding sibling lemma already proved in the same module: diagonal vanishing by the domain-cost-at-equality lemma, non-negativity by the domain-cost non-negativity lemma, and threshold positivity by the canonical-threshold positivity lemma. No further rewriting or case analysis occurs.
why it matters
Gives the forcing-chain Module 5 file a single named certificate object that later structural theorems can assume or inhabit rather than re-proving the three cost axioms. The module header marks the whole file as a STRUCTURAL THEOREM (0 sorry, 0 axiom) in the T0–T8 chain; this definition is the concrete bundle those claims sit inside. It does not itself advance a numbered T-step (J-uniqueness, $\varphi$, eight-tick, $D=3$), but it locks the cost hygiene those steps rely on. No downstream consumers are wired yet in the graph; the immediate sibling is the inhabitedness wrapper that exposes this certificate as a default instance.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.