cert
plain-language theorem explainer
Packages three elementary cost facts into the Module-7 forcing certificate: diagonal vanishing of domain cost, nonnegativity for positive mass/energy, and positivity of the canonical threshold. Anyone citing the RS count law 2^D−1=7 at D=3 uses this record as the inhabited witness. Construction is a pure structure literal wiring three sibling lemmas.
Claim. There is a certificate record asserting: (i) for every $r\neq 0$, the domain cost of the pair $(r,r)$ is zero; (ii) for all $m,e>0$, 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$: at spatial dimension $D=3$ there are exactly seven independent observable categories. The module is marked structural (zero sorry, zero axiom).
The certificate structure bundles three cost-side obligations used by that count. Domain cost is the local cost functional on pairs of positive reals (mass/energy style arguments); it is required to vanish on the diagonal $r\mapsto(r,r)$ and to stay nonnegative off it. The canonical threshold is a fixed positive scale against which those costs are compared.
Upstream, nonnegativity of recognition-event cost is already known from ObserverForcing via $J$-cost nonnegativity on positive states. The present certificate reuses the same nonnegativity pattern at the domain-cost level.
proof idea
One-line structure literal. The three fields of RSForcingChain007Cert are filled by the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos respectively. No further tactic work; the definition is pure packaging.
why it matters
Gives an inhabited witness that Module 7's cost hypotheses hold, so the RS count law $2^D-1=7$ can be cited as a closed structural fact at $D=3$. That count is the combinatorial face of the forcing chain's dimension step (T8: $D=3$) and sits next to the eight-tick octave (T7: period $2^3$). No downstream consumers are wired yet in the graph; the natural parent is any theorem that assumes an RSForcingChain007Cert instance, including the sibling inhabitedness wrapper. Closes the certificate side of a zero-sorry foundation module rather than an open scaffold.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.