pith. sign in
module module high

IndisputableMonolith.Patterns.GrayCodeAxioms

show as:
view Lean formalization →

The GrayCodeAxioms module defines the inverse Gray code that recovers a natural number from its Gray code word via cumulative XOR. Researchers constructing Hamiltonian cycles on hypercubes cite it when establishing bijectivity of the binary-reflected Gray code map. The module supplies supporting definitions and facts imported by the GrayCode and GrayCycleGeneral modules.

claimThe inverse Gray code satisfies $g^{-1}(g) = g_0 + (g_0 + g_1) + (g_0 + g_1 + g_2) + ...$ where each $g_i$ is the $i$-th right shift of the input word and $+$ denotes bitwise XOR.

background

The module sits inside the Patterns namespace and imports the core Patterns definitions for pattern structures. It introduces the inverse conversion specifically for the binary-reflected Gray code, whose forward map is the standard $n$ XOR $(n >> 1)$ operation. This inverse ensures the mapping between natural numbers and hypercube vertices is bijective.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module supplies the invertibility facts required by the GrayCode module, which constructs the binary-reflected Gray code as a Hamiltonian cycle on the d-dimensional hypercube, and by the GrayCycleGeneral module, which lifts the same BRGC formula to arbitrary dimension d.

scope and limits

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (7)