`grayToNat_inverts_natToGray`

proved

show as: view math explainer →

module: IndisputableMonolith.Patterns.GrayCodeAxioms
domain: Patterns
line: 83 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Patterns.GrayCodeAxioms on GitHub at line 83.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

  80
  81**Status**: Standard result in discrete mathematics
  82-/
  83theorem grayToNat_inverts_natToGray :
  84  ∀ n : ℕ, n < 2^64 → grayInverse (n ^^^ (n >>> 1)) = n :=
  85  GrayCodeFacts.grayToNat_inverts_natToGray
  86
  87/-- **Classical Result**: natToGray is a left inverse of grayToNat.
  88
  89The forward Gray code transformation inverts the inverse operation.
  90
  91**Proof**: Follows from bijectivity of Gray code map
  92
  93**References**: Same as above
  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 :

papers checked against this theorem

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