CountLaw7ExactV2Cert
plain-language theorem explainer
Certificate structure bundling three analytic facts used by Count Law 7 (exact v2): the domain cost vanishes on the diagonal, stays nonnegative for positive measure and evidence, and the canonical threshold is strictly positive. Downstream code builds a concrete inhabitant and proves the type is nonempty. Pure packaging: three field obligations, no proof body.
Claim. A Count-Law-7 exact certificate is a triple of properties: (i) for every nonzero real $r$, the domain cost satisfies $\mathrm{domainCost}(r,r)=0$; (ii) for all $m,e>0$, $\mathrm{domainCost}(m,e)\ge 0$; (iii) the canonical threshold is strictly positive.
background
The module records the exact Count Law $2^D-1=7$ as a structural theorem (zero sorry, zero axiom), tying the sevenfold pattern (crystal systems, electroweak modes, GN flavor doublets, etc.) to spatial dimension $D=3$ from the forcing chain (T8).
Domain cost is the local cost functional on measure/evidence pairs; the certificate demands it vanish when measure equals evidence (nonzero) and stay nonnegative on the positive orthant. That nonnegativity is the continuous counterpart of the upstream fact that every recognition event has nonnegative cost, proved via $J$-cost nonnegativity on positive states.
The canonical threshold is the positive cutoff against which domain cost is compared in the counting argument. The structure does not compute the count; it only freezes the three inequalities the exact-v2 certificate needs.
proof idea
No proof body: this is a structure declaration. The three fields are Prop-valued obligations (diagonal vanishing of domain cost, nonnegativity for positive arguments, positivity of the canonical threshold). Inhabitation is deferred to the sibling cert, which fills the fields with domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos.
why it matters
Gives a single named type for the analytic side-conditions of Count Law 7 exact v2, so the module can expose one inhabited certificate rather than three loose lemmas. Downstream, cert assembles the concrete instance and cert_inhabited records Nonempty of the structure.
In the Recognition framework this sits under the $D=3$ forcing step (T8) and the eight-tick octave (T7): once space is three-dimensional, $2^3-1=7$ is the exact residual count the module advertises (crystal systems, electroweak modes, flavor doublets, and the other listed sevens). The certificate isolates the cost-and-threshold facts so the counting theorem can cite one object.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.