GrayCover
plain-language theorem explainer
GrayCover encodes a surjective path of length T on the d-dimensional hypercube where each step flips exactly one bit. Formalizers of hypercube traversals and Gray-code adjacency in Recognition Science cite it to upgrade pure coverage results to ledger-compatible steps. The declaration is a plain structure with three fields and no computational content.
Claim. A Gray cover of dimension $d$ and period $T$ (with $T > 0$) consists of a map $p : Fin T → (Fin d → Bool)$ that is surjective onto all $2^d$ patterns together with the condition that $p(i)$ and $p(i+1)$ differ in exactly one coordinate for every $i$.
background
The module Patterns.GrayCycle works in the state space Pattern d := Fin d → Bool. Adjacency is supplied by the sibling definition OneBitDiff, which asserts that two patterns differ in exactly one coordinate (Hamming distance 1). The module upgrades the earlier cardinality fact Patterns.period_exactly_8 (a surjection Fin 8 → Pattern 3) by adding the one-bit step requirement, producing an object aligned with ledger-compatible adjacency. The structure carries an implicit NeZero T hypothesis to ensure the index type is nonempty.
proof idea
This is a structure definition; the three fields are simply declared with their types and no proof obligations are generated.
why it matters
GrayCover is the parent type for grayCover_min_ticks (which recovers the bound 2^d ≤ T) and for grayCover3 (the explicit 3-bit instance of period 8). It supplies the adjacency layer required to connect the hypercube traversal to the eight-tick octave (T7) and to the D = 3 spatial dimension in the forcing chain. Downstream BRGC constructions instantiate the same structure for arbitrary d.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.