exists_grayCover
plain-language theorem explainer
For any positive integer d a Gray cover of period 2^d exists whose path begins at the binary-reflected Gray code origin. Discrete mathematicians working on hypercube traversals or adjacent pattern coverings cite the result when an explicit surjective one-bit-step sequence is required. The proof is a direct term that supplies the pre-constructed brgcGrayCover object and confirms the initial path entry by reflexivity.
Claim. For every positive integer $d$, there exists a Gray cover $w$ of dimension $d$ and period $2^d$ (a surjective path from the cyclic group of order $2^d$ to the set of all $d$-bit patterns together with one-bit adjacency on consecutive steps) such that the path of $w$ at position 0 equals the binary-reflected Gray code path of $d$ at 0.
background
A GrayCover of dimension $d$ and period $T$ consists of a path function from Fin $T$ to Pattern $d$ that is surjective onto all $2^d$ patterns and satisfies one-bit difference between each consecutive pair (including wrap-around). The brgcPath function supplies the binary-reflected Gray code sequence recursively: for dimension $d+1$ it concatenates the $d$-bit path with its reflection prefixed by a leading bit. This module supplies the general-$d$ case via the standard BRGC formula under the GrayCodeFacts interface when $d$ is bounded, while the imported GrayCycleBRGC file provides the corresponding axiom-free recursive construction.
proof idea
The proof is a one-line term wrapper that applies brgcGrayCover $d$ $hdpos$ as the witness for the existential quantifier and uses reflexivity to match the path-at-zero condition, since brgcGrayCover is defined to set its path field exactly to brgcPath $d$.
why it matters
The declaration supplies the existence certificate that completes the general-dimension Gray cover construction in the patterns module, feeding the BRGC-based path into any downstream use of adjacent coverings. It directly implements the workstream-A generalization described in the module documentation, relying on the surjectivity and injectivity arguments already established inside brgcGrayCover. No open questions are attached; the result is fully proved and closes the bounded case for arbitrary $d>0$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.