cert
plain-language theorem explainer
Packages three elementary domain-cost facts into a single certificate for Foundation Module 2 (eight-tick forcing). Anyone citing the structural theorem that the recognition epoch has period 8 can point at this bundle rather than the three lemmas separately. The definition is a pure structure inhabitant: each field is filled by an already-proved sibling lemma.
Claim. There is a certificate recording that (i) the domain cost vanishes on the diagonal, $\mathrm{cost}(r,r)=0$ for all $r\neq 0$; (ii) the domain cost is nonnegative for positive arguments; and (iii) the canonical threshold is strictly positive.
background
Foundation Module 2 treats the RS eight-tick cycle: once spatial dimension is forced to $D=3$, the recognition epoch has period $2^D=8$. The module is marked structural (zero sorry, zero axiom).
The certificate structure collects three real-analytic facts about a domain cost function and a canonical threshold. Domain cost is the local cost pairing used in this module; it is required to vanish when the two arguments coincide (away from zero) and to stay nonnegative on the positive quadrant. The canonical threshold is a fixed positive real that later gates recognition events.
Upstream, nonnegativity of recognition-event cost is already known from ObserverForcing: "The cost of any recognition event is non-negative," proved via the standard $J$-cost nonnegativity lemma. The present certificate reuses the same nonnegativity idea at the domain-cost level.
proof idea
One-line structure inhabitant. The three fields of RSForcingChain002Cert are filled by the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos respectively. No additional tactic work or algebraic reduction occurs here.
why it matters
Module 2 sits on the forcing chain at the eight-tick octave (primer landmark T7: period $2^3$, forced by T8 $D=3$). This certificate is the packaged witness that the local cost and threshold data needed for that structural theorem are in place.
No downstream consumers are recorded yet in the graph; the immediate sibling cert_inhabited is the natural next step that turns the definition into an inhabited-type fact. The bundle keeps the module's public interface small: callers import one certificate rather than three separate lemmas when they need the Module-2 cost/threshold package.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.