Pith. sign in
theorem

eightTick_from_TruthCore

proved
show as:
module
IndisputableMonolith.RecogSpec.Spec
domain
RecogSpec
line
183 · github
papers citing
none yet

plain-language theorem explainer

There exists a complete 3-bit cover whose period is exactly 8. Anyone building the dimensionless inevitability certificate or the honest-closure verification stack cites this as the eight-tick octave witness. The proof is a one-line appeal to the already-proved exact period-8 cover in Patterns.

Claim. There exists a complete cover $w$ of the $3$-bit pattern space such that the period of $w$ equals $8$.

background

In Recognition Science the discrete recognition clock is forced to an eight-tick octave: period $2^3 = 8$ once spatial dimension is three (forcing chain T7–T8). A complete cover of bit-width 3 is a combinatorial object that exhausts the $2^3$ binary patterns on a cyclic schedule; its period is the length of that schedule.

The RecogSpec layer packages that existence claim as a minimal Prop witness consumed by higher certificates. The local setting is the bridge from pattern combinatorics (Patterns) into dimensionless inevitability and honest-closure verification. Upstream, the witness is defined as $\exists w : \mathrm{CompleteCover}, 3,; w.\mathrm{period} = 8$.

proof idea

One-line term proof. The goal is definitionally the existence statement that some complete 3-bit cover has period 8, and that statement is supplied directly by Patterns.period_exactly_8. No further rewriting or case analysis is required.

why it matters

This is the Lean face of forcing-chain step T7 (eight-tick octave, period $2^3$), with bit-width 3 matching T8's $D = 3$. Downstream it is required by inevitability_dimless_holds, which assembles the full dimensionless inevitability package, and by the HonestClosureCert verification structure (honest framing of what is proved, including $\varphi$-closed observables). Without the witness, RecogSpec cannot certify that the recognition clock closes after eight ticks, so both the inevitability scaffold and the honest-closure certificate fail to close.

Switch to Lean above to see the machine-checked source, dependencies, and usage graph.