  94
  95**Status**: Consequence of inverse correctness
  96-/
  97theorem natToGray_inverts_grayToNat :
  98  ∀ g : ℕ, g < 2^64 →
  99    let n := grayInverse g
 100    n ^^^ (n >>> 1) = g :=
 101  GrayCodeFacts.natToGray_inverts_grayToNat
 102
 103/-- **Classical Result**: Gray code preserves bounds.
 104
 105If g < 2^d, then grayToNat(g) < 2^d.
 106
 107**Proof**: XOR operations preserve bit width
 108
 109**References**: Elementary bit manipulation
 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 :

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.