cert
plain-language theorem explainer
Packages three structural facts for RS forcing-chain Module 3 into a single certificate: domain cost vanishes on the diagonal, is nonnegative for positive arguments, and the canonical threshold is strictly positive. Anyone assembling or discharging the Module 3 gap-45 bundle cites this witness. The construction is a pure structure instance that wires three preexisting sibling lemmas.
Claim. There is a certificate recording that $\mathrm{domainCost}(r,r)=0$ for all $r\neq 0$, that $\mathrm{domainCost}(m,e)\ge 0$ whenever $m>0$ and $e>0$, and that the canonical threshold is strictly positive.
background
Module 3 of the RS forcing chain treats the structural gap $g_D=D^2(D+2)$, which equals $45$ at $D=3$, as the minimum depth for self-reference. The module is marked a structural theorem (zero sorry, zero axioms).
The certificate type bundles three properties of a real-valued domain cost and a positive threshold. Domain cost is the local cost comparison used in this module; the diagonal vanishing clause says matched measure and evidence carry zero cost, while nonnegativity says cost never goes negative for positive inputs. The threshold field is the module's canonical positive cutoff.
Upstream, ObserverForcing already records that every recognition-event cost is nonnegative via the J-cost nonnegativity lemma (0 \le e.cost from Jcost_nonneg on a positive state). The present certificate reuses the same nonnegativity idea at the domain-cost level rather than the event level.
proof idea
Pure structure construction, not a tactic proof. The three fields of the certificate are filled by direct assignment to the sibling lemmas already proved in-module: diagonal vanishing from domainCost_at_eq, nonnegativity from domainCost_nonneg, and positivity of the cutoff from canonicalThreshold_pos. No further rewriting or case analysis occurs.
why it matters
Gives a single named witness that Module 3's cost and threshold obligations hold, matching the module claim that gap-45 at $D=3$ is structural. In the broader forcing chain this sits with the $D=3$ landmark (T8) and the self-reference depth story behind $g_D=45$. No downstream consumers are recorded yet; the natural parent is any checker or aggregator that demands an inhabited Module-3 certificate (the sibling inhabitedness lemma is the immediate companion). It does not itself derive $g_D$ or force $D=3$; it only certifies the local cost/threshold package those arguments rely on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.