cert
plain-language theorem explainer
Packages the three analytic side-conditions of the v3 eight-tick certificate: domain cost vanishes on the diagonal, stays nonnegative for positive arguments, and the canonical threshold is positive. Cited by anyone assembling the structural 8 = 2^D derivation. Construction is a pure structure instance wiring three sibling lemmas.
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 derives the eight-tick recognition cycle as a structural theorem: with spatial dimension $D=3$, one full lattice traversal has $2^D=8$ binary states, so the octave period is forced (T7 in the forcing chain). Status is zero sorry and zero axiom.
The certificate structure bundles three elementary cost facts used by that derivation. Domain cost is the local recognition cost on measure/expectation pairs; it is required to vanish when the two arguments coincide (identity events sit at the J-cost minimum) and to stay nonnegative off the diagonal. The canonical threshold is the positive cutoff against which those costs are compared.
Upstream, nonnegativity of recognition-event cost is already known from ObserverForcing via $J$-cost nonnegativity on positive states. The three fields here specialize that discipline to the domain-cost interface of the v3 eight-tick argument.
proof idea
Pure structure construction, not a tactic proof. The three fields of EightTick_v3Cert are filled by the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos respectively. No further rewriting or case analysis occurs.
why it matters
Gives a single named inhabitant of the v3 eight-tick certificate so downstream material can assume the cost package without re-proving diagonal vanishing, nonnegativity, or threshold positivity. It sits inside the Foundation eight-tick derivation that realizes T7 (eight-tick octave, period $2^3$) once $D=3$ is forced (T8). No used-by edges are recorded yet; the immediate consumer is the inhabitedness witness and any later theorem that takes the certificate as a hypothesis. Closes the analytic side-conditions of the structural 8-tick claim rather than the dimensional forcing itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.