OneBitDiff_symm
Symmetry of the one-bit difference relation on patterns holds for arbitrary dimension d. Researchers constructing Gray codes or Hamiltonian cycles on hypercubes cite this to treat adjacency as undirected. The proof extracts the unique differing coordinate via rcases and re-applies uniqueness after swapping the inequality with ne_comm.
claimFor any natural number $d$ and maps $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
In the GrayCycle module a Pattern of dimension d is defined as a map Fin d → Bool, the vertices of the d-dimensional hypercube. OneBitDiff p q is the predicate that p and q differ in exactly one coordinate, i.e., their Hamming distance is 1; this supplies the adjacency edges for the required Hamiltonian cycle of length 2^d with wrap-around. The module upgrades earlier cardinality facts such as period_exactly_8 to an explicit adjacent cycle, without relying on external Gray-code axioms. Upstream results include the GrayCycle structure itself, which demands that consecutive path elements satisfy OneBitDiff, and the Streams and Measurement Pattern abbreviations that identify finite Boolean windows.
proof idea
The proof is a short tactic sequence. After intro h the hypothesis is destructured by rcases into the unique index k, the inequality hk, and the uniqueness predicate hkuniq. The first subgoal is closed by simpa [ne_comm] using hk. The uniqueness subgoal rewrites the incoming inequality via ne_comm to obtain p k' ≠ q k' and then applies hkuniq directly.
why it matters in Recognition Science
OneBitDiff_symm supplies the symmetry needed to view OneBitDiff as an undirected edge inside the GrayCycle structure. It is invoked by brgc_oneBit_step in the BRGC construction to certify that consecutive codewords differ by one bit. In the Recognition Science setting this supports the eight-tick octave and the 2^D pattern counting that underpins the phi-ladder mass formula and the ledger-compatible adjacency story.
scope and limits
- Does not prove existence of a GrayCycle for any d.
- Does not construct or verify an explicit path.
- Does not relate OneBitDiff to J-cost or defectDist.
- Does not extend to continuous or non-Boolean settings.
formal statement (Lean)
40lemma OneBitDiff_symm {d : Nat} {p q : Pattern d} :
41 OneBitDiff p q → OneBitDiff q p := by
proof body
Tactic-mode proof.
42 intro h
43 rcases h with ⟨k, hk, hkuniq⟩
44 refine ⟨k, ?_, ?_⟩
45 · simpa [ne_comm] using hk
46 · intro k' hk'
47 -- rewrite hk' as p k' ≠ q k' to use uniqueness
48 have hk'' : p k' ≠ q k' := by simpa [ne_comm] using hk'
49 exact hkuniq k' hk''
50
51/-! ## The GrayCycle structure (adjacency + wrap-around) -/
52