pith. sign in
module module high

IndisputableMonolith.Patterns.GrayCycle

show as:
view Lean formalization →

The GrayCycle module defines one-bit adjacency for binary patterns, where two states differ in exactly one coordinate. It supplies the predicates and structures for Gray covers and cycles that support single-update transitions in ledger models and recursive constructions in higher dimensions. The module is definitional, exporting these notions from the base Patterns import without theorems or proofs.

claimOneBitDiff$(p, q)$ holds when patterns $p$ and $q$ differ in precisely one coordinate. A Gray cycle in dimension $d$ is a cyclic sequence of $2^d$ distinct patterns in which every consecutive pair (including the wrap-around) satisfies OneBitDiff.

background

This module belongs to the Patterns domain, which models discrete state transitions on binary strings. It introduces OneBitDiff as the predicate capturing Hamming distance exactly 1, corresponding to a single atomic coordinate change. GrayCycle and GrayCover are then built as sequences or coverings closed under this adjacency relation, relying on the upstream Patterns module for the underlying pattern space and coordinate structure.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the adjacency core imported by LedgerParityAdjacency to link single atomic ledger updates to one-bit parity flips, forming the mathematical center of Workstream B2. It is also used by GrayCycleBRGC and GrayCycleGeneral to construct explicit Gray cycles via BRGC recursion, supporting the eight-tick octave and general-dimension pattern arguments in the forcing chain.

scope and limits

used by (3)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (20)