OneBitDiff_symm
plain-language theorem explainer
Symmetry of the one-bit difference relation on d-dimensional patterns. Researchers constructing Gray codes or Hamiltonian cycles on hypercubes cite this to confirm undirected adjacency. The proof unpacks the unique differing coordinate, swaps the inequality via commutativity, and re-applies uniqueness.
Claim. If two patterns $p, q : (Fin d) → Bool$ differ in exactly one coordinate, then $q$ and $p$ differ in exactly one coordinate.
background
In the GrayCycle module, the state space consists of patterns, which are maps from Fin d to Bool representing vertices of the d-dimensional hypercube. The one-bit difference relation holds when there exists a unique coordinate k such that the patterns disagree at k, encoding Hamming distance one. This lemma establishes symmetry of that adjacency relation.
proof idea
The tactic proof introduces the hypothesis, destructures it into the unique witness k, the inequality at k, and the uniqueness property, then rebuilds the symmetric witness by swapping the inequality with ne_comm and reuses uniqueness for the converse direction.
why it matters
This lemma supports explicit one-bit adjacency in GrayCycle constructions and feeds the brgc_oneBit_step theorem that verifies transitions in the binary reflected Gray code. It advances the module's upgrade from cardinality coverage to adjacent cycles, aligning with ledger-compatible adjacency in the Recognition Science setting for the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.