class
definition
def or abbrev
GrayCodeFacts
show as:
view Lean formalization →
formal statement (Lean)
49class GrayCodeFacts where
50 grayToNat_inverts_natToGray :
51 ∀ n : ℕ, n < 2^64 → grayInverse (n ^^^ (n >>> 1)) = n
52 natToGray_inverts_grayToNat :
53 ∀ g : ℕ, g < 2^64 →
54 let n := grayInverse g
proof body
Definition body.
55 n ^^^ (n >>> 1) = g
56 grayToNat_preserves_bound :
57 ∀ g d : ℕ, g < 2^d → d ≤ 64 → grayInverse g < 2^d
58 pattern_to_nat_bound :
59 ∀ (d : ℕ) (p : Pattern d),
60 (∑ k : Fin d, if p k then 2^(k.val) else 0) < 2^d
61 gray_code_one_bit_property :
62 ∀ (d n : ℕ), n + 1 < 2^d →
63 ∃! k : ℕ, k < d ∧
64 ((n ^^^ (n >>> 1)).testBit k ≠ ((n+1) ^^^ ((n+1) >>> 1)).testBit k)
65
66variable [GrayCodeFacts]
67
68/-- **Classical Result**: Gray code inverse is a left inverse.
69
70The inverse Gray code operation (cumulative XOR) correctly inverts the forward
71Gray code transformation.
72
73**Proof**: Induction on bit positions with XOR algebra
74
75**References**:
76- Knuth (2011), Exercise 7.2.1.1.4
77- Savage (1997), Section 2.1
78
79**Formalization Blocker**: Requires bitwise induction infrastructure for Nat
80
81**Status**: Standard result in discrete mathematics
82-/