grayInverse
The grayInverse definition computes the inverse binary-reflected Gray code by accumulating bitwise XOR of an input with its successive right shifts. Discrete mathematicians and engineers formalizing combinatorial encodings cite this when establishing bijections between natural numbers and Gray codes. The implementation encodes the standard cumulative-XOR series inside a 64-iteration recursive loop that terminates early on zero shifts.
claimThe map sending a natural number $g$ to the value $n = g_0 + g_1 + g_2 + g_3 + g_4 + g_5 + g_6 + g_7 + g_8 + g_9 + g_{10} + g_{11} + g_{12} + g_{13} + g_{14} + g_{15} + g_{16} + g_{17} + g_{18} + g_{19} + g_{20} + g_{21} + g_{22} + g_{23} + g_{24} + g_{25} + g_{26} + g_{27} + g_{28} + g_{29} + g_{30} + g_{31} + g_{32} + g_{33} + g_{34} + g_{35} + g_{36} + g_{37} + g_{38} + g_{39} + g_{40} + g_{41} + g_{42} + g_{43} + g_{44} + g_{45} + g_{46} + g_{47} + g_{48} + g_{49} + g_{50} + g_{51} + g_{52} + g_{53} + g_{54} + g_{55} + g_{56} + g_{57} + g_{58} + g_{59} + g_{60} + g_{61} + g_{62} + g_{63}$ where each $g_k$ is the $k$-bit right shift of $g$ and addition is bitwise XOR, with the sum truncated at the first zero term.
background
The definition sits inside the Gray Code Classical Results module, which records standard properties of the binary-reflected Gray code as axioms while full bitwise formalization remains pending. The forward map is the familiar $n$ to $n$ XOR $(n$ right-shift $1)$, and the inverse recovers the original integer by the cumulative XOR series given in the module background. The module imports Mathlib and the parent Patterns namespace; the two upstream declarations supply a constants-and-functionals bundle for Galerkin-state models and a meta-realization certificate structure, both required by the surrounding import graph.
proof idea
The definition introduces an auxiliary recursive loop that carries a shift counter, an accumulator, and a fuel counter initialized to 64. At each step the input is right-shifted by the current counter; if the result is zero the accumulator is returned, otherwise the shifted value is XORed into the accumulator, the shift is incremented, fuel is decremented, and the loop continues. The outer call supplies the initial values 0, 0, 64.
why it matters in Recognition Science
grayInverse supplies the concrete operation required by the GrayCodeFacts class, which in turn discharges the inversion and bound-preservation theorems used by brgcPath_injective in GrayCycleGeneral. It therefore closes the classical-combinatorial fragment referenced in the module's survey of Savage and Knuth, allowing the Patterns domain to treat Gray-code encodings as reliable primitives inside the larger Recognition Science development. No direct link to the T0-T8 forcing chain or the Recognition Composition Law appears here; the declaration remains a supporting definition for pattern-level bookkeeping.
scope and limits
- Does not prove that the cumulative-XOR map is the two-sided inverse of the forward Gray code.
- Does not extend the computation past 64 bits.
- Does not establish injectivity or surjectivity of the Gray-code map.
- Does not connect to J-uniqueness, the phi-ladder, or spatial-dimension forcing.
formal statement (Lean)
38def grayInverse (g : ℕ) : ℕ :=
proof body
Definition body.
39 let rec loop (shift : ℕ) (acc : ℕ) (fuel : ℕ) : ℕ :=
40 match fuel with
41 | 0 => acc
42 | fuel' + 1 =>
43 let shifted := g >>> shift
44 if shifted = 0 then acc
45 else loop (shift + 1) (acc ^^^ shifted) fuel'
46 loop 0 0 64
47
48/-- Hypothesis envelope for Gray code classical properties. -/