IndisputableMonolith.Patterns.GrayCodeAxioms
Axioms and inversion facts for binary-reflected Gray codes on the hypercube. Converts a Gray word back to its natural index by cumulative XOR, and records the standard one-bit adjacency and bound-preservation properties. Downstream Gray-cycle constructions cite these as the algebraic interface. The content is definitional plus elementary bit-arithmetic lemmas.
claimThe inverse Gray map $g^{-1}:\mathbb{N}\to\mathbb{N}$ recovers the index from a binary-reflected Gray word by cumulative XOR. The module records that $g^{-1}\circ g = \mathrm{id}$ and $g\circ g^{-1}=\mathrm{id}$ on the relevant bounds, that $g^{-1}$ preserves the $2^d$ bound, and that successive Gray codes differ in exactly one bit.
background
Binary-reflected Gray code (BRGC) enumerates the vertices of the $d$-cube so that consecutive codes differ by a single bit flip. The forward map is the classical formula $g(n)=n\oplus(n\gg 1)$. The inverse undoes that map by cumulative XOR of the Gray bits, restoring the original natural index.
In the Patterns layer this sits under the hypercube-cover language used for eight-tick and general-$d$ recognition cycles. The parent Patterns module supplies the ambient pattern and cover types; this file isolates the Gray-specific arithmetic so that cycle constructions need not re-prove bit identities.
Sibling declarations include the inverse function itself, mutual inversion lemmas, bound preservation for Gray-to-nat and pattern-to-nat, and the one-bit adjacency property that makes BRGC a Hamiltonian path on $Q_d$.
proof idea
Definition module plus elementary lemmas on bit operations. The inverse is defined by cumulative XOR. Mutual inversion with the forward Gray map is proved by standard induction on bit width. Bound preservation is a direct estimate on the support of the bits. The one-bit property is the classical BRGC adjacency fact, recorded here as an axiom-style interface for downstream cycle builders.
why it matters in Recognition Science
Feeds the binary-reflected Gray code construction module, which builds the Hamiltonian cycle on $Q_d$ from the recursive BRGC scheme, and the general-$d$ GrayCycle workstream, which exposes an adjacent Gray cover/cycle via $g(n)=n\oplus(n\gg 1)$ as GrayCover d (2^d) / GrayCycle d.
In Recognition Science the eight-tick octave (forcing step T7) and the $D=3$ spatial claim (T8) rely on clean hypercube traversals; Gray adjacency is the combinatorial engine for those period-$2^d$ covers. Isolating inversion and one-bit facts here keeps the cycle modules free of low-level XOR bookkeeping.
scope and limits
- Does not construct the full BRGC sequence or prove it is a Hamiltonian cycle.
- Does not fix dimension $d=3$ or the eight-tick period; those live downstream.
- Does not address non-binary or non-reflected Gray variants.
- Does not derive physical constants or mass-ladder claims from the bit arithmetic.