GrayCover
plain-language theorem explainer
GrayCover packages a surjective path of length T through all d-bit patterns where consecutive states differ by exactly one bit flip. Pattern theorists cite it to formalize Gray-code adjacency when building cycle objects in Recognition Science. The declaration is a structure definition that directly bundles the path map, a surjectivity witness, and the OneBitDiff condition on successive elements.
Claim. Let $d,T$ be natural numbers with $T$ nonzero. A Gray cover is a map $path: Fin T → (Fin d → Bool)$ that is surjective onto all patterns and satisfies OneBitDiff$(path(i), path(i+1))$ for every $i$, where OneBitDiff$(p,q)$ asserts that $p$ and $q$ differ in exactly one coordinate.
background
The GrayCycle module takes Pattern d to be the set of all functions Fin d → Bool. OneBitDiff p q is the predicate that exactly one coordinate k satisfies p k ≠ q k. This structure upgrades the plain coverage facts from the parent Patterns module by adding the adjacency requirement. The module documentation states that GrayCycle supplies the stronger adjacent object needed to align with ledger-compatible adjacency and relies on the standard recursive BRGC construction.
proof idea
GrayCover is a structure definition with no proof body. It declares three fields: the path function of type Fin T → Pattern d, the completeness field asserting surjectivity of that path, and the oneBit_step field asserting OneBitDiff between each consecutive pair.
why it matters
GrayCover is the base type instantiated by grayCover3 for the explicit period-8 cycle on 3 bits and by brgcGrayCover for the general BRGC case. It supplies the adjacency condition required by the GrayCycle module and supports the eight-tick octave (period 2^3) together with the emergence of D = 3 in the forcing chain. Downstream results such as grayCover_min_ticks and grayCover_eight_tick_min derive the lower bound 2^d ≤ T directly from instances of this structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.