grayToNat_inverts_natToGray
plain-language theorem explainer
The theorem asserts that the Gray code inverse recovers the original natural number n from its forward encoding n XOR (n right shift 1), whenever n is less than 2 to the 64. Researchers in combinatorial algorithms and digital encoding would reference this result when establishing bijectivity of Gray code transformations. The proof proceeds as a direct term application of the corresponding field in the GrayCodeFacts class.
Claim. For every natural number $n$ with $n < 2^{64}$, the inverse Gray code map satisfies $grayInverse(n ⊕ (n ≫ 1)) = n$, where $⊕$ denotes bitwise XOR and $≫$ denotes arithmetic right shift.
background
The Patterns.GrayCodeAxioms module declares well-known properties of the binary-reflected Gray code (BRGC) as axioms pending full bitwise formalization. The forward map is the standard construction gray(n) = n XOR (n >>> 1); grayInverse implements the cumulative XOR sequence that recovers the original binary representation. This local setting draws on classical references including Knuth (2011) Exercise 7.2.1.1.4 and Savage (1997) Section 2.1 to support pattern arguments without requiring complete Mathlib bitwise induction infrastructure.
proof idea
The proof is a term-mode one-liner that directly applies the grayToNat_inverts_natToGray field from the GrayCodeFacts class. No additional tactics or lemmas are expanded; the statement is discharged by the hypothesis envelope declared in the same module.
why it matters
This result supplies the left-inverse property that populates the GrayCodeFacts class, which is invoked to establish injectivity of brgcPath in GrayCycleGeneral. It occupies the classical discrete mathematics slot in the Patterns domain, allowing combinatorial encodings to interface with the Recognition framework without reinventing bitwise algebra. The module doc cites Knuth (2011) and Savage (1997) as sources and notes the formalization blocker for bitwise induction on Nat.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.