`grayToNat_inverts_natToGray`

proved

show as: view math explainer →

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

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Patterns.GrayCodeAxioms on GitHub at line 83.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

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.