cert
plain-language theorem explainer
Packages the three field witnesses that certify Module 9 of the RS forcing chain: diagonal vanishing of domain cost, nonnegativity for positive arguments, and positivity of the canonical threshold. Anyone citing the J-cost ratio-symmetry certificate uses this bundle. The definition is a pure structure assembly of three already-proved sibling lemmas.
Claim. There is a certificate consisting of: (i) $\mathrm{domainCost}(r,r)=0$ for all $r\neq 0$; (ii) $\mathrm{domainCost}(m,e)\ge 0$ whenever $m>0$ and $e>0$; (iii) the canonical threshold is strictly positive.
background
Module 9 of the RS forcing chain records the structural fact that Recognition Science cost is ratio-symmetric: the J-cost satisfies $J(x)=J(1/x)$. In RS-native units the cost functional is built from $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$), forced unique by T5 of the unified forcing chain.
Here domainCost is the two-argument cost on positive reals used by the module; its diagonal vanishing and nonnegativity are the concrete expressions of that symmetry and of the global fact that recognition cost never goes negative. The canonical threshold is the positive cutoff against which cost comparisons are made in the chain.
Upstream, ObserverForcing already proves that every recognition event has nonnegative cost via Cost.Jcost_nonneg. The structure RSForcingChain009Cert simply names the three Prop fields this module must discharge.
proof idea
One-line structure inhabitant. The three fields are filled by the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos respectively; no further tactic work occurs. The definition is marked noncomputable only because the ambient real arithmetic is.
why it matters
This is the named certificate object for Foundation Module 9 (J-cost symmetry / ratio symmetry), status STRUCTURAL THEOREM with zero sorry and zero axioms. It sits on the forcing-chain spine after T5 J-uniqueness: once $J$ is fixed as $(x+x^{-1})/2-1$, diagonal vanishing and nonnegativity are immediate structural consequences that later modules may assume by pointing at this cert.
No downstream consumers are wired in the current graph (used_by empty), but the sibling cert_inhabited and any later forcing-chain aggregator that requires an RSForcingChain009Cert instance are the intended call sites. It does not itself advance T6–T8 (phi, eight-tick, $D=3$); it only locks the cost-symmetry layer those steps rest on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.