grayCycle3_bijective
plain-language theorem explainer
The Gray cycle path on three-bit patterns is a bijection from the eight cycle indices to the eight possible patterns. Workers formalizing hypercube traversals or Gray-code embeddings in discrete geometry would reference this result to certify exact coverage without repetition. The argument first equates the cardinalities of the domain and codomain to eight and then invokes the general criterion that an injection between finite sets of equal size is bijective.
Claim. The function $f : {0,1,2,3,4,5,6,7} → ({0,1}^3)$ given by the three-bit Gray cycle construction is bijective.
background
In the GrayCycle module, Pattern d is defined as the set of all functions from Fin d to Bool, representing d-bit strings. The grayCycle3Path is constructed by composing the gray8At indexing function with the pattern3 embedding, yielding a map from Fin 8 to Pattern 3. This realizes a Hamiltonian cycle on the 3-dimensional hypercube, where edges correspond to single-bit flips. The module upgrades cardinality results from Patterns to an adjacency-respecting cycle. Upstream, card_pattern establishes that the cardinality of Pattern d equals 2^d, while grayCycle3_injective proves that grayCycle3Path is injective.
proof idea
The proof proceeds in tactic mode by first computing the cardinalities: Fintype.card (Fin 8) equals 8 by simplification, and Fintype.card (Pattern 3) equals 8 via the card_pattern lemma specialized to d=3. With these equalities in hand, it applies the library fact Fintype.bijective_iff_injective_and_card to conclude bijectivity from the already-established injectivity of grayCycle3Path and the matching cardinalities.
why it matters
This bijectivity result directly supplies the missing half for the subsequent grayCycle3_surjective theorem, completing the demonstration that the Gray cycle visits every 3-bit pattern exactly once. It supports the eight-tick octave structure (period 2^3) required by the forcing chain at step T7 and aligns the pattern counting with D=3 spatial dimensions at T8. The construction avoids reliance on external Gray-code axioms, keeping the development self-contained within the Patterns hierarchy.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.