brgcGrayCover
plain-language theorem explainer
A Gray cover for d-bit patterns with exact period 2^d is supplied for every dimension d satisfying 1 ≤ d ≤ 64. Pattern theorists working inside the Recognition Science framework cite the construction when they require an explicit adjacent traversal of the hypercube that respects 64-bit word arithmetic. The body assembles the cover by setting the path to the binary-reflected Gray code function, deriving surjectivity from injectivity plus matching cardinality, and attaching the one-bit adjacency property from an auxiliary lemma.
Claim. For each natural number $d$ with $0 < d ≤ 64$, there exists a map $γ : ℤ/2^dℤ → {0,1}^d$ that is surjective and satisfies that $γ(i)$ and $γ(i+1)$ differ in exactly one coordinate for every $i$.
background
In the Patterns module a Pattern of dimension d is defined as the type Fin d → Bool. The GrayCover structure for parameters d and T (with T nonzero) consists of a path function Fin T → Pattern d together with a surjectivity proof and a one-bit difference condition on consecutive values. The cardinality lemma states that the number of d-bit patterns equals 2^d exactly. This definition lives in the bounded bitwise development of GrayCycleGeneral, which routes successor adjacency through GrayCodeAxioms and therefore carries the explicit hypothesis d ≤ 64; the module documentation contrasts it with the fully recursive, axiom-free construction available in GrayCycleBRGC.
proof idea
The definition populates the GrayCover record by assigning the path field to brgcPath d. Surjectivity follows from first proving injectivity via the brgcPath_injective lemma, observing that Fintype.card (Fin (2^d)) equals Fintype.card (Pattern d) by the card_pattern lemma, and then applying the Fintype bijective_iff_injective_and_card lemma to obtain bijectivity. The oneBit_step field is supplied directly by the brgc_oneBit_step lemma.
why it matters
This definition supplies the concrete witness required by the exists_grayCover_of_le64 theorem in the same module, which in turn supports the general existence statement for Gray covers. It occupies the bounded slot in the Gray cycle development that feeds the Recognition Science pattern-recognition layer appearing in the Measurement and Complexity modules. The parent recursive construction in GrayCycleBRGC removes the 64-bit restriction entirely and yields the unconditional existence theorem exists_grayCover.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.