grayToNat
plain-language theorem explainer
The grayToNat definition computes the inverse of the binary-reflected Gray code by accumulating the XOR of an input with its successive right shifts. Combinatorialists and pattern theorists working on hypercube traversals cite it for the efficient inversion that preserves the single-bit-flip property. The implementation is a bounded recursive auxiliary function that terminates after at most 64 shifts for any practical natural number.
Claim. The map sending a Gray-coded natural number $g$ to the binary number $n = g + (g >> 1) + (g >> 2) + ...$ (with bitwise XOR) recovers the original binary representation.
background
The module defines the binary-reflected Gray code (BRGC) that generates a Hamiltonian cycle on the d-dimensional hypercube Q_d. The recursive construction prepends a bit and reverses the list at each dimension, guaranteeing that consecutive codes differ by exactly one bit and that the first and last codes also differ by one bit. This supplies a concrete, axiom-free implementation of the inverse operation whose algebraic properties are stated separately in the GrayCodeAxioms sibling module.
proof idea
The definition is a one-line wrapper around a tail-recursive auxiliary function. The auxiliary starts with shift 0 and accumulator 0, repeatedly replaces the accumulator by its XOR with the input right-shifted by the current shift, increments the shift, and stops when the shifted value is zero or the fuel counter reaches zero (set to 64).
why it matters
grayToNat supplies the concrete inverse required by the two inversion theorems in GrayCodeAxioms (grayToNat_inverts_natToGray and natToGray_inverts_grayToNat). Those theorems establish mutual left-inverses and thereby the bijectivity of the Gray-code map on bounded naturals. The construction supports discrete pattern modeling inside the Recognition Science framework, where binary-reflected traversals appear in the combinatorial layer that feeds the eight-tick octave and phi-ladder structures.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.