grayToNat_preserves_bound

formal source

 110
 111**Status**: Simple bitwise reasoning
 112-/
 113theorem grayToNat_preserves_bound :
 114  ∀ g d : ℕ, g < 2^d → d ≤ 64 → grayInverse g < 2^d :=
 115  GrayCodeFacts.grayToNat_preserves_bound
 116
 117/-- **Classical Result**: Pattern to number conversion bound.
 118
 119Converting a d-bit pattern to a number gives a value < 2^d.
 120
 121**Proof**: Sum of 2^i for i < d equals 2^d - 1 < 2^d
 122
 123**References**: Elementary combinatorics
 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