grayToNat_inverts_natToGray
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not prove the inversion for any n at or above 2^64.
- Does not supply an explicit inductive proof on bit positions.
- Does not address Gray codes in non-power-of-two bounds or non-binary bases.
- Does not incorporate J-cost, phi-ladder, or forcing-chain primitives.
formal statement (Lean)
83theorem grayToNat_inverts_natToGray :
84 ∀ n : ℕ, n < 2^64 → grayInverse (n ^^^ (n >>> 1)) = n :=
proof body
Term-mode proof.
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-/