exists_grayCycle
plain-language theorem explainer
For every positive integer dimension d a Gray cycle exists whose path at phase zero coincides with the binary-reflected Gray code path. Pattern theorists and researchers constructing Hamiltonian cycles on hypercubes cite the result as the unconditional existence statement for general d. The proof is a one-line wrapper that directly supplies the recursive BRGC object and closes the equality by reflexivity.
Claim. For every natural number $d$ satisfying $0 < d$, there exists a Gray cycle $w$ of dimension $d$ such that the path function of $w$ evaluated at phase 0 equals the binary-reflected Gray code path evaluated at 0.
background
A GrayCycle d is the structure consisting of a path map from Fin(2^d) to Pattern d, an injectivity proof, and a one-bit adjacency condition on consecutive phases that includes the wrap-around from the last phase back to phase 0. The module supplies a bounded bitwise version of the BRGC construction and a separate recursive version that removes the d ≤ 64 restriction. The upstream brgcGrayCycle definition in GrayCycleBRGC packages the recursive path, its injectivity, and its one-bit step lemmas into a single GrayCycle instance for any d > 0.
proof idea
One-line wrapper that applies brgcGrayCycle from the BRGC module to the given d and positivity hypothesis, then uses reflexivity to witness the required path equality at phase 0.
why it matters
The declaration supplies the canonical axiom-free existence witness for a Gray cycle in arbitrary dimension, completing the general-D development that the module contrasts with its bounded sibling. It delegates to the recursive BRGC construction whose injectivity and adjacency properties are already established upstream. The result sits inside the broader pattern-covering workstream that feeds discrete structures into the Recognition Science forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.