RSForcingChain002Cert
plain-language theorem explainer
Certificate structure packaging three domain-cost facts for Foundation Module 2 (eight-tick cycle). Anyone citing the module's inhabited cert depends on this bundle: diagonal vanishing of domain cost, nonnegativity for positive arguments, and positivity of the canonical threshold. Pure structure definition with no proof body; proofs live in the sibling lemmas assembled by cert.
Claim. A Module-2 forcing certificate is a triple of facts: (i) for every nonzero real $r$, the domain cost satisfies $\mathrm{cost}(r,r)=0$; (ii) for all positive reals $m,e$, $\mathrm{cost}(m,e)\ge 0$; (iii) the canonical threshold is strictly positive.
background
Foundation Module 2 treats the RS eight-tick cycle: period $2^D=2^3=8$ recognition states per epoch, forced by spatial dimension $D=3$. The module is marked structural (zero sorry, zero axioms).
Domain cost is the local cost on pairs of reals used in this module, tied to the J-cost $J(x)=(x+x^{-1})/2-1$ from the forcing chain. The canonical threshold is a fixed positive scale against which cost comparisons are made. Upstream, ObserverForcing records that every recognition event has nonnegative cost, via $J$-cost nonnegativity on positive states.
The certificate does not redefine those objects; it only packages the three Prop obligations any Module-2 witness must discharge.
proof idea
No proof body: this is a structure declaration. The three fields are named hypotheses (diagonal vanishing, nonnegativity, threshold positivity). Inhabitation is deferred to the sibling def cert, which fills the fields from domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos. Those lemmas carry the actual arguments; this declaration only fixes the interface.
why it matters
Gives a single named type for Module 2's structural obligations so downstream code can depend on Nonempty RSForcingChain002Cert rather than three loose lemmas. Direct consumers are cert (the canonical inhabitant) and cert_inhabited.
Sits in the forcing-chain lane for the eight-tick octave (primer T7: period $2^3$), with the module framing forced by $D=3$ (T8). Packaging only; the physics content is in the sibling proofs and the broader UnifiedForcingChain. No open scaffold: claim status is definition.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.