Pith. sign in
module module moderate

IndisputableMonolith.Patterns.GrayCodeAxioms

show as:
view Lean formalization →

GrayCodeAxioms supplies the inverse Gray code map that recovers a natural number from its Gray code representation through cumulative XOR. Researchers constructing Hamiltonian cycles on hypercubes cite the module when establishing bijectivity of the binary-reflected Gray code. The module consists of the core inverse definition together with direct algebraic inversion facts.

claimThe inverse Gray code map satisfies $\gamma^{-1}(g) = \bigoplus_{i \geq 0} (g \gg i)$, recovering the original index via cumulative XOR and obeying the inversion identity $\gamma^{-1}(\gamma(n)) = n$.

background

The module extends the base pattern definitions imported from IndisputableMonolith.Patterns. It introduces the inverse Gray code operation that converts a Gray code value back to its natural-number index by successive XOR steps. This supplies the bijectivity tool needed for sequence and cycle constructions in the Patterns domain.

Upstream material in Patterns provides the foundational sequence and adjacency notions on which the Gray code axioms rest. The module therefore sits as a targeted extension that isolates the inversion step required by later constructions.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module feeds the GrayCode construction of the binary-reflected Gray code (BRGC) that generates a Hamiltonian cycle on the d-dimensional hypercube Q_d, and the GrayCycleGeneral module that lifts the same BRGC formula gray(n) = n XOR (n >>> 1) to arbitrary dimension. It supplies the inversion property required to verify that the generated sequence is a cycle.

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)