cert
plain-language theorem explainer
Packages three elementary cost facts into a single D=3 configuration certificate: diagonal vanishing of domain cost, nonnegativity off the diagonal, and positivity of the canonical threshold. Cited by anyone assembling the eight-tick forcing of spatial dimension three. The body is a pure structure inhabitant that wires three already-proved sibling lemmas into the certificate fields.
Claim. There exists a certificate asserting: (i) $\mathrm{domainCost}(r,r)=0$ for every real $r\neq 0$; (ii) $\mathrm{domainCost}(m,e)\ge 0$ whenever $m>0$ and $e>0$; (iii) the canonical threshold is strictly positive.
background
This module records the structural claim that spatial dimension $D=3$ is forced by eight-tick closure: the recognition cycle has period $8=2^3$, so exactly three binary recursions close the lattice, and that is the unique minimal self-similar dimension (forcing landmark T8).
The certificate structure bundles three cost-side side conditions used by that argument. Domain cost is the local cost functional on pairs of positive reals (built from the RS $J$-cost $J(x)=(x+x^{-1})/2-1$). The first field demands that cost vanish on the diagonal $m=e$; the second that it stay nonnegative for positive arguments; the third that a fixed positive threshold (the cutoff used to separate admissible configurations) be strictly above zero.
Upstream, nonnegativity of recognition-event cost is already available from ObserverForcing via $J$-cost nonnegativity at positive states; the in-module siblings specialize that pattern to domain cost and supply the diagonal and threshold facts.
proof idea
Pure structure construction, not a tactic proof. The three fields of the certificate are filled by direct assignment to the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos. No further rewriting or case analysis occurs.
why it matters
Gives a single named inhabitant of the D=3 cost certificate so downstream dimension-forcing arguments can quote one object rather than three separate lemmas. Sits inside the ConfigDim D3 v3 session, whose module claim is the structural theorem that $D=3$ follows from eight-tick closure (period $8=2^3$), matching forcing-chain landmark T8. No downstream consumers are wired yet in the graph; the immediate sibling cert_inhabited is the natural next step that records non-emptiness of the certificate type. Does not itself prove $D=3$; it only packages the cost hypotheses that the dimension argument relies on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.