OneBitDiff_symm
plain-language theorem explainer
Symmetry of the one-bit difference relation on patterns is established to support undirected adjacency in cycle constructions. Researchers building Hamiltonian paths on hypercubes cite it when verifying that Gray-code steps remain valid after reversal. The tactic proof extracts the unique differing coordinate, swaps the inequality via commutativity, and reuses the uniqueness predicate.
Claim. Let $p, q : Fin d → Bool$. If there exists a unique $k : Fin d$ such that $p(k) ≠ q(k)$, then there exists a unique $k : Fin d$ such that $q(k) ≠ p(k)$.
background
Patterns are maps Fin d → Bool. OneBitDiff p q is the predicate that exactly one coordinate differs, written ∃! k : Fin d, p k ≠ q k. The GrayCycle structure packages a path through all 2^d patterns that is injective and satisfies OneBitDiff between consecutive phases (including wrap-around). This lemma supplies the undirected character of that adjacency relation. The module builds explicit cycles without relying on external Gray-code axioms, using the standard recursive construction instead.
proof idea
Tactic proof. Introduce the hypothesis, case on the unique witness triple, then refine the goal by swapping the inequality with ne_comm and reapplying the uniqueness quantifier to the swapped pair.
why it matters
The lemma supplies the symmetry needed for the adjacency condition inside GrayCycle. It is invoked directly by brgc_oneBit_step to certify each step of the recursive BRGC path. In the Recognition framework this closes the basic undirected-adjacency fact required before the full Hamiltonian cycle can be used for ledger-compatible counting at dimension d, aligning with the 2^D coverage already obtained from period_exactly_8.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.