IndisputableMonolith.Patterns.GrayCode
The GrayCode module supplies definitions for converting natural numbers to binary-reflected Gray code and back using the standard XOR-shift operation. Researchers formalizing discrete combinatorial patterns in Recognition Science, especially for ledger structures or higher-dimensional cycles, would cite it. The module contains only definitions and imports axioms from GrayCodeAxioms with no internal proofs.
claimThe module defines the binary-reflected Gray code map $g(n) = n \oplus \lfloor n/2 \rfloor$ together with its inverse and the reflected sequence construction on natural numbers.
background
This module sits inside the Patterns domain and imports the parent Patterns module plus GrayCodeAxioms. The upstream GrayCodeAxioms doc states that the binary-reflected Gray code (BRGC) is a well-studied combinatorial object and declares its classical properties as axioms pending full bitwise formalization. The supplied module doc gives the explicit conversion rule gray(n) = n XOR (n >> 1). Sibling declarations implement natToGray, binaryReflectedGray, and grayToNat.
proof idea
This is a definition module, no proofs.
why it matters in Recognition Science
The module supplies the concrete BRGC implementation required by GrayCycleGeneral, which builds adjacent Gray covers for general dimension d, and by LedgerUniqueness, which uses the structure to address why the Recognition framework selects the specific eight-tick, three-dimensional ledger. It therefore closes the combinatorial layer between the axiomatic Gray code properties and the downstream uniqueness arguments.
scope and limits
- Does not derive Gray code properties from bitwise axioms inside this module.
- Does not treat Gray codes over structures other than natural numbers.
- Does not prove uniqueness or cycle properties; those live in downstream modules.