IndisputableMonolith.Patterns.GrayCode
Defines the binary-reflected Gray code maps between natural numbers and bitstrings via the classical formula gray(n) = n XOR (n shifted right by 1), together with the inverse. Pattern and ledger modules cite these conversions when they need an explicit adjacent coding of the 2^D vertices of the hypercube. The module is definitional: it packages the standard BRGC encoding and decoding, relying on GrayCodeAxioms for classical bitwise identities.
claimThe module supplies the binary-reflected Gray code $g:\mathbb{N}\to\mathbb{N}$ given by $g(n)=n\oplus\lfloor n/2\rfloor$, its inverse $g^{-1}$, and the reflected construction that enumerates the vertices of the $D$-cube so that successive codes differ in exactly one bit.
background
Recognition Science needs a discrete walk on the hypercube that flips one coordinate at a time: the eight-tick octave (forcing step T7) and the $D=3$ spatial claim (T8) both rest on an adjacent cover of the $2^D$ vertices. Binary-reflected Gray code (BRGC) is the classical combinatorial object that does exactly that.
This module sits under Patterns and imports GrayCodeAxioms, which records well-known BRGC properties as axioms pending full bitwise formalization. The core maps are the standard conversion $n\mapsto n\oplus(n\gg 1)$, the inverse decode, and the reflected recursive construction that builds the full cycle.
Notation is ordinary: natural numbers stand for bitstrings, XOR and right-shift are the bitwise operations, and adjacency means Hamming distance one.
proof idea
This is a definition module, not a theorem package. It introduces the encoding and decoding functions (nat-to-Gray, binary-reflected Gray, Gray-to-nat) by the classical closed formulas, and defers the nontrivial bitwise identities (bijectivity, single-bit transitions, cycle closure) to the imported GrayCodeAxioms layer. No substantial tactic proofs live here; the content is the API that downstream Gray-cycle constructions call.
why it matters in Recognition Science
GrayCycleGeneral imports this module as Workstream A: it builds an adjacent Gray cover/cycle for general dimension $d$ from the BRGC formula and exposes it as Patterns.GrayCover $d$ $(2^d)$ / Patterns.GrayCycle $d$. That general cycle is the combinatorial spine for the eight-tick structure forced at T7 and for $D=3$ at T8.
LedgerUniqueness also imports it while answering the Gap 9 objection: why specifically $\varphi$, the 3-cube $Q_3$, and the 8-tick ledger rather than some other discrete conserved structure. An explicit, unique-up-to-reflection adjacent coding of the cube vertices is part of that uniqueness argument. Without a concrete BRGC API, those parent modules would have to re-derive the encoding inline.
scope and limits
- Does not prove bijectivity or single-bit adjacency; those live in GrayCodeAxioms.
- Does not construct the Gray cycle for general $d$; that is GrayCycleGeneral.
- Does not address ledger uniqueness or the $\varphi$/8-tick forcing; only supplies the coding API.
- Does not formalize bitwise operations from first principles beyond Mathlib.