grayCover3
plain-language theorem explainer
The declaration assembles a concrete GrayCover instance for three-bit patterns over period eight. Workers on hypercube adjacency or the eight-tick octave in Recognition Science would reference this object. It is formed by direct record construction from the pre-proved path, surjectivity, and one-bit transition facts.
Claim. Let $P : {0,1}^3$ denote the set of 3-bit patterns. The function $g : {0,1,2,3,4,5,6,7} → P$ given by the 3-bit Gray cycle, together with the facts that $g$ is surjective and that $g(i)$ and $g(i+1)$ differ in exactly one coordinate for each $i$, constitutes a GrayCover of dimension 3 and period 8.
background
GrayCover(d,T) is the structure whose fields are a path map Fin T → Pattern d, a surjectivity proof, and a one-bit adjacency proof (OneBitDiff) between consecutive images. Pattern d is the type Fin d → Bool; OneBitDiff records that two patterns differ in precisely one coordinate. The module upgrades the earlier cardinality result period_exactly_8 to an explicit adjacent cycle on the 3-dimensional hypercube.
proof idea
One-line record constructor that supplies the three required fields: the path grayCycle3Path, the surjectivity theorem grayCycle3_surjective, and the adjacency theorem grayCycle3_oneBit_step.
why it matters
The definition supplies the explicit GrayCover realizing the period-8 cycle required by the T7 eight-tick octave and T8 three-dimensional forcing steps. It converts the surjective counting fact from Patterns into the adjacency condition needed for ledger-compatible walks. No downstream citations are recorded.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.