IndisputableMonolith.Patterns.GrayCode
The GrayCode module supplies definitions converting natural numbers to binary-reflected Gray codes via the formula gray(n) = n XOR (n >> 1). Researchers building discrete cycle covers in Recognition Science cite it when generalizing to arbitrary dimensions. The module consists of three direct definitions that import supporting axioms from GrayCodeAxioms.
claimThe binary-reflected Gray code map is defined by $g(n) = n \oplus \lfloor n/2 \rfloor$, together with the inverse conversions natToGray and grayToNat.
background
This module belongs to the Patterns domain and imports GrayCodeAxioms, whose doc states: "This module declares well-known Gray code properties as axioms pending full bitwise formalization." It further notes that the binary-reflected Gray code (BRGC) is a well-studied combinatorial object. The module introduces the three sibling definitions natToGray, binaryReflectedGray, and grayToNat that realize the classical conversion formula.
proof idea
this is a definition module, no proofs
why it matters in Recognition Science
The module supplies the BRGC primitives required by GrayCycleGeneral, which states it "constructs an adjacent Gray cover/cycle for general dimension d using the standard BRGC formula gray(n) = n XOR (n >>> 1)" and exposes Patterns.GrayCover d (2^d). It also supports LedgerUniqueness in addressing why the Recognition framework selects the specific 3D cube and 8-tick structure.
scope and limits
- Does not prove any Gray code properties; they remain axioms.
- Does not implement bitwise operations from first principles.
- Does not address applications outside pattern construction.