IndisputableMonolith.Patterns.GrayCode
This module defines the conversion from natural numbers to binary-reflected Gray code using the standard formula gray(n) = n XOR (n >> 1). Researchers constructing discrete cycles or covers in Recognition Science ledger arguments would cite it. The module consists entirely of definitions with no internal proofs, delegating classical properties to the imported axioms submodule.
claimThe binary-reflected Gray code map $g:ℕ→ℕ$ defined by $g(n)=n⊕⌊n/2⌋$, together with the inverse conversion and related functions natToGray, binaryReflectedGray, grayToNat.
background
This module resides in the Patterns namespace and imports the general Patterns framework plus GrayCodeAxioms. The axioms submodule declares well-known Gray code properties as axioms pending full bitwise formalization, noting that the binary-reflected Gray code (BRGC) is a well-studied combinatorial object. The module supplies the concrete functions implementing the standard conversion gray(n) = n XOR (n >> 1).
proof idea
This is a definition module, no proofs.
why it matters in Recognition Science
The module supplies Gray code primitives used by GrayCycleGeneral to construct adjacent Gray covers for general dimension d via the BRGC formula and by Meta.LedgerUniqueness to address why the specific discrete ledger (phi, Q3, 8-tick) is selected over alternatives.
scope and limits
- Does not prove Gray code properties; those remain axiomatic in the Axioms submodule.
- Does not generalize beyond the binary-reflected Gray code.
- Does not address continuous or non-combinatorial analogs.
- Does not establish uniqueness or cycle closure on its own.