pith. machine review for the scientific record. sign in
theorem proved term proof

natToGray_inverts_grayToNat

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

  97theorem natToGray_inverts_grayToNat :
  98  ∀ g : ℕ, g < 2^64 →
  99    let n := grayInverse g

proof body

Term-mode proof.

 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-/

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (5)

Lean names referenced from this declaration's body.