exists_grayCycle_of_le64
plain-language theorem explainer
Existence of a Gray cycle in dimension d whose path coincides with the binary-reflected Gray code path holds for every d satisfying 0 < d ≤ 64. Pattern theorists working on hypercube Hamiltonian cycles in the Recognition Science framework cite this for bounded bitwise constructions. The proof is a one-line wrapper that directly invokes the packaged BRGC Gray cycle definition and applies reflexivity to the path field.
Claim. For every natural number $d$ with $0 < d ≤ 64$, there exists a Gray cycle $w$ of dimension $d$ such that the path of $w$ equals the binary-reflected Gray code path of dimension $d$.
background
GrayCycle is the structure whose fields are a path map from Fin(2^d) to Pattern d, an injectivity proof, and a one-bit adjacency proof for consecutive phases including wrap-around. The module develops a bounded BRGC construction that defines the path via the bitwise formula gray(n) = n XOR (n >>> 1) and routes successor adjacency through GrayCodeAxioms, which impose the d ≤ 64 restriction. Upstream, the GrayCycle structure is introduced in Patterns.GrayCycle while the recursive unbounded BRGC path and its GrayCycle packaging appear in GrayCycleBRGC.
proof idea
The proof is a one-line wrapper that applies the brgcGrayCycle definition (which assembles path, injectivity, and one-bit step under the d ≤ 64 hypothesis) and uses reflexivity to equate the path field.
why it matters
This supplies an explicit existence witness for Gray cycles under the bounded BRGC assumptions inside the Patterns domain. It fills the Workstream A generalization slot for d up to 64 and connects directly to the GrayCycle structure; the D=3 case stays axiom-free in a separate file while the general case here depends on the 64-bit bound. The module doc notes that the canonical axiom-free certificate lives in GrayCycleBRGC.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.