grayToNat
plain-language theorem explainer
The grayToNat definition supplies the inverse binary-reflected Gray code map via cumulative XOR of right-shifts. Combinatorial number theorists studying hypercube Hamiltonian cycles would cite this construction for its explicit inverse. The implementation uses a fuel-bounded recursive auxiliary function that accumulates XORs until the shifted argument vanishes.
Claim. The inverse Gray code map $i:ℕ→ℕ$ is defined by $i(g)=g⊕(g≫1)⊕(g≫2)⊕⋯$ (truncated when the shift vanishes).
background
The module constructs the binary-reflected Gray code that generates a Hamiltonian cycle on the d-dimensional hypercube Q_d. The recursive rule is BRGC(0)=[0] and BRGC(n+1)=[0·BRGC(n), 1·BRGC(n) reversed], ensuring every vertex is visited once with consecutive entries differing in one bit. This definition supplies the concrete inverse operation that recovers the original binary index from a Gray code word. The module remains axiom-free; inversion properties are supplied by the sibling GrayCodeFacts interface.
proof idea
The definition introduces an auxiliary recursive function aux(shift, acc, fuel) that computes the right-shift of the input by the current shift, XORs the result into the accumulator when nonzero, increments the shift, and decrements fuel. Recursion stops at fuel exhaustion or when the shifted value is zero; the top-level call uses shift 0, acc 0, and fuel 64.
why it matters
This definition is the concrete implementation referenced by the two inversion theorems grayToNat_inverts_natToGray and natToGray_inverts_grayToNat in GrayCodeAxioms. Those theorems establish mutual left-inverses below 2^64 and thereby support the Hamiltonian-cycle properties listed in the module doc. The construction sits in the Patterns domain and supplies the combinatorial inverse needed for any downstream use of Gray-code traversals; no direct link to the forcing chain or J-cost appears here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.