RSForcingChain007Cert
plain-language theorem explainer
Certificate structure for forcing-chain module 7 (the count law 2^D-1=7 at D=3). It bundles three facts: domain cost vanishes on the diagonal, is nonnegative for positive arguments, and the canonical threshold is positive. Downstream code cites the inhabited instance, not the bare structure. Pure data bundle: field types only, no proof body.
Claim. A module-7 certificate is a triple of properties: (i) for every nonzero real $r$, the domain cost of the pair $(r,r)$ equals zero; (ii) for all positive reals $m$ and $e$, the domain cost of $(m,e)$ is nonnegative; (iii) the canonical threshold is strictly positive.
background
Module 7 of the RS forcing chain records the count law $2^D-1=7$ independent observable categories once spatial dimension is fixed at $D=3$ (forcing step T8). The module is marked structural: zero sorry, zero axioms.
Domain cost is the local cost on pairs of positive reals used throughout this module (measure/expectation style arguments). Upstream, ObserverForcing already shows every recognition event has nonnegative cost, via nonnegativity of the J-cost $J(x)=(x+x^{-1})/2-1$. The canonical threshold is the positive cutoff that separates trivial from nontrivial recognition in the same module.
The certificate simply names the three side conditions the rest of the module needs as one inhabited type.
proof idea
No proof body: this is a structure declaration whose three fields are Prop-valued requirements. Inhabitation is discharged by the sibling definition that fills the fields with the diagonal-vanishing lemma for domain cost, the nonnegativity lemma for domain cost, and positivity of the canonical threshold. The nonempty theorem is then the one-line constructor application of that inhabitant.
why it matters
This structure is the type of the module certificate. The sibling inhabitant and the Nonempty theorem close Module 7 of the forcing chain, which asserts the exact count law $2^D-1=7$ at $D=3$. That count is the combinatorial face of T8 (three spatial dimensions) and of the eight-tick octave (period $2^3$), since $2^3-1=7$ independent nonzero bit patterns. Auditors of the forcing chain cite the inhabited certificate to confirm the module's structural obligations are discharged without axioms. It does not itself derive $D=3$; it packages the cost/threshold facts the count-law module depends on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.