grayInverse
plain-language theorem explainer
The grayInverse definition implements the standard inverse for binary-reflected Gray codes, recovering the original natural number from its encoded value by successive XOR of right-shifted copies. Combinatorial pattern work in Recognition Science cites it when establishing inversion or bound properties for discrete encodings. The body is a 64-step tail-recursive loop that accumulates XOR until the shifted input vanishes.
Claim. The inverse Gray code map recovers the original natural number via cumulative XOR: for input $g$, compute $g$ XOR $(g$ right-shift $1)$ XOR $(g$ right-shift $2)$ XOR ... until the shifted value is zero, with computation bounded at 64 bits.
background
Module Patterns.GrayCodeAxioms treats binary-reflected Gray code properties as axioms pending full bitwise formalization. The forward map is $n$ XOR $(n$ right-shift $1)$, while the inverse recovers the source by XORing the Gray value with all its right shifts. The module cites Savage (1997) and Knuth (2011) for the combinatorial background and notes O(log n) algorithms with numerical verification to arbitrary depth.
proof idea
This is a definition, not a theorem. It uses a let-rec loop with parameters shift, accumulator, and fuel (initially 64). Each iteration right-shifts the input by the current shift, XORs the result into the accumulator if nonzero, then recurses with incremented shift and decremented fuel; it returns the accumulator on fuel exhaustion or zero shift.
why it matters
grayInverse supplies the concrete operation required by the GrayCodeFacts class, which in turn provides the inversion lemmas grayToNat_inverts_natToGray and natToGray_inverts_grayToNat. Those lemmas are invoked to establish injectivity of brgcPath in GrayCycleGeneral. The definition therefore closes the combinatorial layer that supports pattern axioms, though it carries no direct link to the T0-T8 forcing chain or Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.