cert
plain-language theorem explainer
Packages three elementary cost facts into a single certificate that the eight-tick domain is well-posed: diagonal cost vanishes, cost is nonnegative off the identity, and the canonical threshold is positive. Anyone citing the structural completeness of the period-8 lattice uses this bundle rather than the three lemmas separately. The body is a pure structure instance, wiring three sibling proofs.
Claim. There is a certificate consisting of: (i) $\mathrm{domainCost}(r,r)=0$ for every $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 asserts that the eight-tick cycle is complete: a period-8 lattice covers all $2^D=8$ binary states exactly once per cycle, and no shorter period does. That claim is the Recognition Science T7 landmark (eight-tick octave, period $2^3$), here treated as a structural theorem with no sorry and no axioms.
The certificate structure bundles three cost-side side conditions rather than a direct covering statement. Domain cost is the local cost functional on pairs of positive reals (imported from the Cost layer); it is required to vanish on the diagonal and stay nonnegative. The canonical threshold is a positive real cutoff used to separate complete from incomplete cycles.
Upstream, nonnegativity of recognition-event cost is already known from ObserverForcing: every recognition event has cost $\ge 0$ because $J$-cost is nonnegative on positive states. The three fields of the certificate are discharged by in-module siblings domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos.
proof idea
One-line structure instance. The three fields of EightTickCompleteCert are filled by the three sibling lemmas already proved in the same module: diagonal vanishing, nonnegativity of domain cost on the positive quadrant, and positivity of the canonical threshold. No further tactic work.
why it matters
Gives a single named inhabitant of the eight-tick completeness certificate so downstream foundation code can depend on one object rather than three scattered lemmas. It sits inside the T7 step of the forcing chain (eight-tick octave, period $2^3$), which together with T8 ($D=3$) forces the $2^D=8$ state count. The module status line marks the whole development as a structural theorem with zero sorry and zero axioms; this definition is the concrete witness that the cost-side hypotheses of that theorem are inhabited. No downstream users are recorded yet; the natural consumer is any completeness or covering argument that needs the bundled certificate rather than raw cost lemmas.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.