cert_inhabited
plain-language theorem explainer
The Module 6 forcing certificate is inhabited: a witness packs domain-cost zero-on-diagonal, nonnegativity for positive arguments, and a strictly positive canonical threshold. Anyone wiring the D=3 / eight-tick structural chain cites this to discharge Nonempty. Proof is a one-line term packaging the prebuilt certificate value.
Claim. The Module 6 forcing certificate type is nonempty: there exists a record asserting (i) domain cost vanishes on the diagonal, $\mathrm{cost}(r,r)=0$ for all $r\neq 0$; (ii) domain cost is nonnegative for positive mass and energy arguments; (iii) the canonical threshold is strictly positive.
background
Module 6 of the RS forcing chain records that spatial dimension $D=3$ is forced by the eight-tick period $2^3$, with no free parameters. Status is structural: zero sorry, zero axioms. The local certificate is a three-field structure packaging elementary positivity facts used by that forcing step.
Domain cost is the module's cost functional on real mass/energy arguments. Its zero-on-diagonal clause says equal arguments incur zero cost (for nonzero $r$); nonnegativity says the cost is $\ge 0$ whenever both arguments are positive. The canonical threshold is a fixed positive real cutoff appearing in the same package. These three fields are exactly the structure's inhabitants.
proof idea
One-line term proof. The certificate value already assembled in-module is fed to the anonymous constructor of Nonempty, so inhabitance is immediate from the existence of that concrete record. No tactics, no further lemmas.
why it matters
Closes the Module 6 structural package for the forcing-chain step that forces $D=3$ from the eight-tick octave (framework landmarks T7 period $2^3$, T8 spatial dimension three). The certificate is the portable witness that domain-cost positivity and a positive threshold are available without parameters. No downstream consumers are wired in this snapshot, so the theorem is the terminal inhabitance marker for the module rather than an intermediate lemma in a longer proof.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.