EightTickCompleteCert
plain-language theorem explainer
A certificate bundle packing three elementary cost facts used to underwrite eight-tick completeness: diagonal vanishing of domain cost, nonnegativity for positive arguments, and positivity of the canonical threshold. Anyone assembling or discharging the completeness certificate cites this structure. It is a pure structure definition with no proof body; inhabitants are built by plugging in the sibling lemmas.
Claim. An eight-tick completeness certificate is a triple of facts: (i) for every nonzero real $r$, the domain cost of $(r,r)$ is zero; (ii) for all positive reals $m,e$, the domain cost of $(m,e)$ is nonnegative; (iii) the canonical threshold is strictly positive.
background
The module treats the Recognition Science claim that the period-8 lattice is complete: it covers all $2^D=8$ binary states exactly once per cycle, and no shorter period does. That is the T7 eight-tick octave landmark (period $2^3$), here packaged as a structural theorem with no sorry and no axioms.
Domain cost is the local cost functional on pairs of positive reals used in this completeness argument; the certificate requires it to vanish on the diagonal (matched measure and expectation) and stay nonnegative off-diagonal. The canonical threshold is the positive cutoff against which completeness is judged.
Upstream, nonnegativity of recognition-event cost is already known from ObserverForcing: "The cost of any recognition event is non-negative," via $J$-cost nonnegativity on positive states. The certificate's nonnegativity field is the domain-cost analogue of that fact.
proof idea
No proof body: this is a structure declaration. The three fields are Prop-valued requirements (diagonal vanishing, nonnegativity, threshold positivity). Downstream, the concrete inhabitant cert fills them by the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos; cert_inhabited then records Nonempty of the structure type.
why it matters
Gives a single named type for the cost/threshold side-conditions that the eight-tick completeness story depends on, so later theorems can assume or inhabit one object rather than three loose hypotheses. Downstream, cert builds the canonical inhabitant and cert_inhabited proves the type is nonempty, closing the local certificate API.
In the broader forcing chain this sits under T7 (eight-tick octave, period $2^3$) and the module claim that period 8 is the minimal full cover of the $2^D=8$ binary states when $D=3$. It does not itself re-prove the lattice cover; it standardizes the cost facts that completeness arguments quote. No open scaffold remains in this module (status: structural, zero sorry).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.