IndisputableMonolith.Patterns.GrayCycle
This module defines the predicate OneBitDiff for patterns differing in exactly one coordinate and introduces GrayCycle and GrayCover types. It is imported by ledger-parity adjacency work and by explicit Gray cycle constructions in higher dimensions. The module supplies basic definitions and lemmas that downstream files extend with concrete realizations.
claimThe module introduces the predicate $\mathsf{OneBitDiff}(p,q)$ asserting that patterns $p$ and $q$ differ in exactly one coordinate (Hamming distance 1), together with the types $\mathsf{GrayCycle}\,d$ and $\mathsf{GrayCover}\,d\,n$ for cycles and covers in dimension $d$.
background
This module belongs to the Patterns domain and imports the parent Patterns module. Its central definition is the predicate OneBitDiff, which states that two patterns differ in exactly one coordinate. Sibling declarations include GrayCycle, GrayCover, grayCover_min_ticks and gray8At, which build sequences where consecutive elements satisfy the one-bit condition.
The local setting prepares the ground for Gray-code realizations of the eight-tick octave. The module does not yet construct explicit cycles; it only records the adjacency relation that later modules instantiate via BRGC recursion.
proof idea
This is a definition module, no proofs.
why it matters in Recognition Science
The module supplies the core one-bit adjacency predicate used by LedgerParityAdjacency to connect single-coordinate ledger updates to parity changes (Workstream B2). It is also imported by GrayCycleBRGC and GrayCycleGeneral, which realize axiom-free and general-dimension Gray cycles via the BRGC formula. It therefore anchors the pattern layer that supports the T7 eight-tick octave in the Recognition framework.
scope and limits
- Does not construct explicit Gray cycles for any dimension.
- Does not prove existence or minimality of Gray covers.
- Does not relate patterns to physical constants or mass ladders.
- Does not address ledger states or parity directly.
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