grayToNat
The grayToNat definition supplies the standard inverse map for the binary-reflected Gray code, recovering the original natural number from its Gray-encoded form via successive XOR with right shifts. Combinatorialists studying hypercube Hamiltonians cite this as the recovery step that inverts the single-bit transition encoding. The body implements the recovery as a tail-recursive accumulation of XORs bounded by 64 iterations to ensure termination for machine integers.
claimThe function $grayToNat(g)$ returns the natural number $n$ obtained by the cumulative XOR $n = g ⊕ (g ≫ 1) ⊕ (g ≫ 2) ⊕ ⋯$ until the shifted argument vanishes.
background
The binary-reflected Gray code generates a Hamiltonian cycle on the d-dimensional hypercube Q_d in which consecutive codes differ by exactly one bit and the first and last entries also differ by one bit. This module supplies the forward and inverse maps for the encoding; the inverse converts a Gray code integer back to its binary representation. The local setting is the Patterns layer, which treats Gray codes as combinatorial primitives for traversals and encodings.
proof idea
The definition introduces a recursive auxiliary function aux that begins with shift 0 and accumulator 0, then repeatedly right-shifts the input g, XORs the nonzero result into the accumulator, increments the shift, and decrements a fuel counter of 64. Termination occurs either when the shifted value is zero or fuel is exhausted.
why it matters in Recognition Science
This definition is invoked by the two inversion theorems grayToNat_inverts_natToGray and natToGray_inverts_grayToNat in GrayCodeAxioms, which establish that the maps are mutual inverses below 2^64. It supplies the concrete implementation of the Gray-code bijection used in hypercube traversals, feeding the combinatorial structures that appear in the Recognition Science treatment of patterns and self-similar encodings.
scope and limits
- Does not prove bijectivity or the Hamiltonian-cycle property of the Gray code.
- Does not extend the construction beyond 64-bit machine integers.
- Does not supply the correctness proofs; those reside in the Axioms module.
- Does not accept or handle non-natural-number inputs.
Lean usage
theorem gray_inverse_correct (g : ℕ) (h : g < 2^64) : grayToNat (natToGray g) = g := GrayCodeAxioms.natToGray_inverts_grayToNat g hformal statement (Lean)
38def grayToNat (g : ℕ) : ℕ :=
proof body
Definition body.
39 -- Inverse Gray code: repeatedly XOR with shifted versions
40 -- g XOR (g >> 1) XOR (g >> 2) XOR ...
41 -- For bounded values, this terminates
42 let rec aux (shift : ℕ) (acc : ℕ) (fuel : ℕ) : ℕ :=
43 match fuel with
44 | 0 => acc
45 | fuel' + 1 =>
46 let shifted := g >>> shift
47 if shifted = 0 then acc
48 else aux (shift + 1) (acc ^^^ shifted) fuel'
49 aux 0 0 64 -- 64 shifts is enough for any practical number
50
51-- Properties and classical results are provided via
52-- `IndisputableMonolith.Patterns.GrayCodeAxioms.GrayCodeFacts`.
53-- This module remains axiom-free and parametric over those facts.
54
55end Patterns
56end IndisputableMonolith