grayInverse
plain-language theorem explainer
grayInverse supplies the cumulative-XOR map that inverts the binary-reflected Gray code on naturals. Discrete mathematicians and formalizers of combinatorial encodings cite the function when stating bijectivity or bound preservation for Gray-code paths. The body is a fixed-fuel recursive loop that accumulates XORs of right-shifted copies until the shifted value vanishes.
Claim. For $g ∈ ℕ$ the inverse Gray-code map is defined by the finite cumulative XOR $g ⊕ (g ≫ 1) ⊕ (g ≫ 2) ⊕ ⋯$ performed within a 64-bit window.
background
The module declares classical Gray-code properties as axioms pending full bitwise formalization. The binary-reflected Gray code is the map $n ↦ n ⊕ (n ≫ 1)$; its inverse is the cumulative XOR described in the module doc-comment, with published proofs and O(log n) algorithms referenced to Savage (1997) and Knuth (2011). This sits inside the Patterns domain, where combinatorial encodings support pattern-recognition axioms.
proof idea
The declaration is a definition whose body introduces an auxiliary recursive function loop. The function matches on fuel; when fuel is positive it computes the right-shift of g, returns the accumulator if the shift is zero, otherwise recurses with incremented shift and accumulator XOR the shift, decrementing fuel. The entry point calls the loop with shift 0, accumulator 0 and fuel 64.
why it matters
The definition is the concrete operation referenced by the GrayCodeFacts class to state the inversion theorems grayToNat_inverts_natToGray and natToGray_inverts_grayToNat; those facts are used by brgcPath_injective to obtain injectivity of the BRGC path map. It therefore supplies the classical combinatorial layer required by the pattern axioms in the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.