exists_grayCover_of_le64
plain-language theorem explainer
For each natural number d with 0 < d ≤ 64 the binary-reflected Gray code path supplies a Gray cover of all d-bit patterns with exact period 2^d. Researchers constructing or enumerating adjacent pattern sequences in bounded dimensions cite this existence result to obtain a concrete witness. The proof is a direct term that instantiates the pre-built brgcGrayCover under the given bounds and confirms path equality by reflexivity.
Claim. For every natural number $d$ satisfying $0 < d ≤ 64$ there exists a Gray cover $w$ of dimension $d$ and period $2^d$ whose path function coincides with the binary-reflected Gray code path brgcPath$(d)$.
background
A GrayCover d T is a structure consisting of a path map Fin T → Pattern d that is surjective onto all d-bit patterns and satisfies one-bit adjacency between successive positions, including the wrap-around step. The function brgcPath d is defined by applying the standard binary-reflected Gray code formula to each index in Fin (2^d). This module supplies the bounded bitwise version of the construction, which routes successor adjacency and 64-bit inverses through GrayCodeAxioms and therefore carries the explicit hypothesis d ≤ 64; the fully recursive, axiom-free counterpart lives in GrayCycleBRGC.
proof idea
The proof is a one-line term wrapper that applies brgcGrayCover d hdpos hd to obtain the witness and uses reflexivity to match the path component.
why it matters
The theorem packages the bounded BRGC construction as an existence statement, providing the interface that downstream GrayCycle objects can invoke for d ≤ 64. It fills the role of a concrete adjacent cover before the module transitions to the axiom-free recursive definition in GrayCycleBRGC. Within the Recognition framework it supplies a structured enumeration of patterns that aligns with the self-similar fixed-point and eight-tick octave requirements.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.