IndisputableMonolith.Patterns.GrayCycle
The GrayCycle module defines the OneBitDiff predicate for patterns differing in exactly one coordinate (Hamming distance 1) together with supporting Gray cycle and cover notions. Researchers on ledger parity bridges or general-D Gray constructions cite it as the combinatorial base layer. The module consists of definitions and elementary properties with no complex proofs.
claimLet $p,q$ be patterns. The predicate OneBitDiff$(p,q)$ holds precisely when the Hamming distance between $p$ and $q$ is 1. GrayCycle and GrayCover are the associated cycle and cover structures built from such one-bit adjacencies.
background
This module sits in the Patterns domain and imports IndisputableMonolith.Patterns plus Mathlib. Its core definition, OneBitDiff, states that two patterns differ in exactly one coordinate. Sibling definitions include GrayCycle, GrayCover, grayCover_min_ticks, grayCover_eight_tick_min, pattern3, gray8At and grayCycle3Path, all operating on finite binary or integer vectors under single-coordinate flips. The setting supplies the adjacency primitive required by downstream parity and Gray-code work.
proof idea
This is a definition module, no proofs.
why it matters in Recognition Science
It supplies the one-bit adjacency predicate used by LedgerParityAdjacency (the mathematical core of Workstream B2 on single atomic updates inducing one-bit parity changes) and by GrayCycleBRGC (axiom-free recursive BRGC construction) together with GrayCycleGeneral (bounded BRGC generalization for arbitrary dimension). The module therefore anchors the combinatorial foundation for both the ledger-parity bridge and the general-D Gray-cycle constructions in the Recognition framework.
scope and limits
- Does not prove existence of Gray cycles or covers.
- Does not relate patterns to the forcing chain T0-T8 or RS constants.
- Does not treat non-binary or infinite patterns.
- Does not supply explicit cycle constructions beyond the adjacency predicate.
used by (3)
depends on (1)
declarations in this module (20)
-
def
OneBitDiff -
lemma
OneBitDiff_symm -
structure
GrayCycle -
structure
GrayCover -
theorem
grayCover_min_ticks -
theorem
grayCover_eight_tick_min -
def
pattern3 -
def
gray8At -
def
grayCycle3Path -
theorem
gray8At_injective -
def
toNat3 -
lemma
toNat3_pattern3 -
theorem
pattern3_injective -
theorem
grayCycle3_injective -
theorem
grayCycle3_bijective -
theorem
grayCycle3_surjective -
theorem
grayCycle3_oneBit_step -
def
grayCycle3 -
theorem
grayCycle3_period -
def
grayCover3