IndisputableMonolith.Patterns.GrayCode
The GrayCode module supplies definitions for converting natural numbers to binary-reflected Gray code representations via the standard formula gray(n) equals n bitwise XOR of (n right-shifted by 1). Researchers constructing discrete adjacency structures in Recognition Science cite it when building cycle covers. The module consists of definitions that import axioms from GrayCodeAxioms and supply primitives to downstream generalization work.
claimThe binary-reflected Gray code conversion is defined by $gray(n) = nopluslfloor n/2rfloor$.
background
This module sits inside the Patterns domain of Recognition Science and imports the core Patterns module together with GrayCodeAxioms. The axioms module states: 'This module declares well-known Gray code properties as axioms pending full bitwise formalization. The binary-reflected Gray code (BRGC) is a well-studied combinatorial object.' The supplied definitions therefore rest on those declared axioms rather than on proved bitwise lemmas.
proof idea
This is a definition module, no proofs.
why it matters in Recognition Science
The module feeds the Gray code primitives into LedgerUniqueness, which addresses the objection that other discrete ledgers might exist besides the phi-based, 8-tick, three-dimensional structure, and into GrayCycleGeneral, which constructs an adjacent Gray cover for arbitrary dimension d via the BRGC formula gray(n) = n XOR (n >>> 1).
scope and limits
- Does not contain proofs of any Gray code properties.
- Does not implement or verify bitwise operations inside Lean.
- Does not treat higher-dimensional or non-standard Gray codes.
- Does not supply numerical examples or test data.