cert
plain-language theorem explainer
Packages a certificate that the domain cost vanishes on the diagonal, stays non-negative off it, and that the canonical threshold is positive. Anyone citing the exact Count Law 7 (2^D−1=7 from D=3) uses this bundle as the structural witness. The definition is a three-field structure instance wiring sibling lemmas into the certificate type.
Claim. There is a certificate consisting of: (i) $\mathrm{domainCost}(r,r)=0$ for all $r\neq 0$; (ii) $\mathrm{domainCost}(m,e)\ge 0$ whenever $m>0$ and $e>0$; (iii) the canonical threshold is strictly positive.
background
The module states Count Law 7 as a structural theorem: $2^D-1=7$ once spatial dimension is forced to $D=3$, and lists the familiar sevens (crystal systems, electroweak modes, diatonic notes, etc.) as instances of that count. Status is zero-sorry, zero-axiom.
The certificate type collects three analytic facts about a domain cost on positive reals: it is zero when measure and expectation coincide (off zero), it is non-negative when both arguments are positive, and a fixed canonical threshold is positive. Upstream, the ObserverForcing cost non-negativity result records that every recognition event has non-negative J-cost, via the standard non-negativity of the J-cost functional.
Sibling lemmas in the same file supply the three fields: equality of domain cost on the diagonal, non-negativity of domain cost, and positivity of the canonical threshold.
proof idea
One-line structure instance. The three fields of the certificate are filled by the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos. No further tactic work; the definition is pure assembly of already-proved local facts into the certificate record.
why it matters
Gives the inhabited certificate object for Count Law 7 Exact v2, the structural claim that $2^D-1=7$ once the forcing chain has fixed $D=3$ (T8). The module presents this as a proved structural theorem with no sorry and no axioms, tying the octave/tick combinatorics of the foundation layer to the familiar count of seven. No downstream consumers are recorded yet; the immediate sibling cert_inhabited is the natural next use. Framework landmarks: T8 ($D=3$) and the eight-tick octave (T7) that make $2^3-1=7$ the forced count.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.