cert
plain-language theorem explainer
Packages three elementary facts about the module-6 domain cost and canonical threshold into a single certificate record for the RS forcing chain. Anyone assembling or discharging the D=3 / eight-tick structural package cites this witness. The body is a pure structure instance: each field is filled by an already-proved sibling lemma.
Claim. There is a certificate consisting of: (i) $\mathrm{domainCost}(r,r)=0$ for every nonzero real $r$; (ii) $\mathrm{domainCost}(m,e)\ge 0$ whenever $m>0$ and $e>0$; (iii) the canonical threshold is strictly positive.
background
Module 6 of the RS forcing chain records the structural claim that spatial dimension $D=3$ is forced by the eight-tick period $2^3$, with no free parameters. The local certificate type bundles three positivity and normalization facts about a real-valued domain cost on pairs of positive reals, together with a positive canonical threshold used as a comparison scale.
The domain cost is the module's working cost functional (sibling of the global $J$-cost). Upstream, ObserverForcing already records that every recognition-event cost is nonnegative via $J$-cost nonnegativity: "The cost of any recognition event is non-negative." The three fields here are the corresponding domain-level statements: vanishing on the diagonal, nonnegativity off the axes, and a positive threshold.
proof idea
One-line structure instance. The three certificate fields are filled by the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos respectively; no further tactic work occurs.
why it matters
This is the inhabited certificate object for Foundation module 6, whose module claim is the T8 landmark: $D=3$ spatial dimensions forced from the eight-tick octave (period $2^3$). It does not itself derive $D=3$; it packages the cost-normalization and threshold-positivity side conditions that the structural theorem relies on. Downstream use is not yet wired in this graph snapshot, but the sibling cert_inhabited and the module's zero-sorry structural status indicate this record is the discharge witness for the module-6 certificate interface. Framework role: bookkeeping glue on the T7–T8 segment of the forcing chain (eight-tick octave forcing $D=3$).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.