pattern_to_nat_bound

formal source

 124
 125**Status**: Straightforward calculation
 126-/
 127theorem pattern_to_nat_bound :
 128  ∀ (d : ℕ) (p : Pattern d),
 129    (∑ k : Fin d, if p k then 2^(k.val) else 0) < 2^d :=
 130  GrayCodeFacts.pattern_to_nat_bound
 131
 132/-- **Classical Result**: Consecutive Gray codes differ in one bit.
 133
 134For any n < 2^d - 1, gray(n) and gray(n+1) differ in exactly one bit position.
 135
 136**Proof**:
 137- gray(n) XOR gray(n+1) = [n XOR (n>>1)] XOR [(n+1) XOR ((n+1)>>1)]
 138- This simplifies to a single power of 2 (bit at position of least significant 0 in n)
 139
 140**References**:
 141- Savage (1997), Theorem 2.1
 142- Knuth (2011), Theorem 7.2.1.1.A
 143
 144**Status**: Defining property of Gray codes
 145-/
 146theorem gray_code_one_bit_property :
 147  ∀ (d n : ℕ), n + 1 < 2^d →
 148    ∃! k : ℕ, k < d ∧
 149      (n ^^^ (n >>> 1)).testBit k ≠ ((n+1) ^^^ ((n+1) >>> 1)).testBit k :=
 150  GrayCodeFacts.gray_code_one_bit_property
 151
 152end GrayCodeAxioms
 153end Patterns
 154end IndisputableMonolith