GrayCodeFacts

formal source

  46  loop 0 0 64
  47
  48/-- Hypothesis envelope for Gray code classical properties. -/
  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
  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