GrayCover
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not require the path to close (path (T-1) to path 0 need not satisfy OneBitDiff).
- Does not guarantee minimality of T (separate theorems derive 2^d ≤ T).
- Does not supply an explicit path construction (handled in siblings such as grayCycle3Path).
- Applies only for finite nonzero T.
formal statement (Lean)
62structure GrayCover (d T : Nat) [NeZero T] where
63 path : Fin T → Pattern d
64 complete : Function.Surjective path
65 oneBit_step : ∀ i : Fin T, OneBitDiff (path i) (path (i + 1))
66
67/-! Minimality: any cover of all `d`-bit patterns needs at least `2^d` ticks. -/