eightTickWitness
plain-language theorem explainer
The eight-tick witness is the Prop that a complete cover of the 3-bit pattern space exists with exact period 8. RecogSpec packs, inevitability scaffolding, and honest-closure certificates cite it as the discrete octave condition. It is a bare existential definition; existence is discharged later by the period-exactly-8 lemma.
Claim. There exists a complete cover $w$ of $3$-dimensional binary patterns such that the period of $w$ equals $8$ (i.e., a surjective path $\mathrm{Fin}\,8\to\mathrm{Pattern}\,3$).
background
A complete cover of dimension $d$ packages a period $N\in\mathbb{N}$, a path $\mathrm{Fin},N\to\mathrm{Pattern},d$, and a proof that the path is surjective: every $d$-bit pattern appears at least once. For $d=3$ the pattern space has cardinality $2^3=8$, so an exact minimal cover has period $8$.
RecogSpec packages Recognition Science claims as named Prop witnesses rather than free-floating theorems. The eight-tick condition is the discrete octave forced by the forcing chain: after $D=3$ spatial bits are fixed (T8), recognition updates close on a $2^D$-tick cycle (T7).
Upstream, CompleteCover is the structure that makes "exact cover of period $N$" a first-class object; the companion existence result states that a complete cover of length exactly $2^d$ exists for every $d$.
proof idea
No proof body: this is a @[simp] definition of a Prop. The right-hand side is the raw existential
$\exists w:\mathrm{CompleteCover},3,; w.\mathrm{period}=8$.
Discharge lives one line downstream: eightTick_from_TruthCore is the one-line wrapper that applies Patterns.period_exactly_8 to inhabit the witness.
why it matters
This witness is the RecogSpec handle for the T7 eight-tick octave (period $2^3$ once $D=3$ is forced). Downstream it is required by eightTick_from_TruthCore, folded into the explicit universal dimensionless pack and dimlessPack_explicit, and appears among the conjuncts that inevitability_dimless_holds assembles. Honest-closure certificates also depend on it when they list which discrete structural claims are on the books.
Without a named Prop for "period exactly 8," the dimensionless inevitability scaffold would have to re-state the cover existence inline; the witness keeps that obligation modular and simp-normalizable.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.