pith. sign in
module module high

IndisputableMonolith.Patterns.GrayCycle

show as:
view Lean formalization →

Patterns.GrayCycle introduces the one-bit difference relation on patterns and defines GrayCycle and GrayCover structures. Ledger parity arguments and BRGC-based general-dimension constructions import it directly. The module supplies foundational definitions and short supporting lemmas in the Patterns namespace.

claimLet $P$ be a pattern space. OneBitDiff$(p,q)$ holds precisely when the Hamming distance between $p$ and $q$ equals 1. A GrayCycle of dimension $d$ is a cyclic sequence of length $2^d$ in which every consecutive pair (including the closing pair) satisfies OneBitDiff; a GrayCover is the corresponding non-cyclic path version.

background

The module belongs to the Patterns domain and imports the base Patterns definitions. It introduces OneBitDiff as the relation in which two patterns differ in exactly one coordinate. GrayCycle and GrayCover are then defined as sequences respecting this adjacency relation, providing the discrete combinatorial substrate for eight-tick octave constructions.

proof idea

This is a definition module. It declares OneBitDiff together with GrayCycle and GrayCover, then records elementary consequences such as symmetry of OneBitDiff and length bounds on covers.

why it matters in Recognition Science

The module supplies the adjacency primitives required by LedgerParityAdjacency for its single-atomic-update parity bridge lemma in Workstream B2. It is also the direct dependency for GrayCycleBRGC and GrayCycleGeneral, which lift the same objects to arbitrary dimension via the binary-reflected Gray code recursion. This places the pattern layer beneath the forcing-chain steps that reach D=3.

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)