pith. machine review for the scientific record. sign in
structure definition def or abbrev high

Chain

show as:
view Lean formalization →

A Chain over a RecognitionStructure M is a finite sequence of n+1 elements drawn from M.U such that each consecutive pair satisfies the recognition relation M.R. Ledger algebra and conservation proofs cite this structure to represent atomic recognition sequences. The declaration is a direct structure with fields for length, the indexing function, and the connection predicate.

claimLet $M$ be a recognition structure with universe $U$ and binary relation $R$. A chain in $M$ consists of a natural number $n$, a function $f$ from the finite set of $n+1$ indices to $U$, and a proof that $R(f(i),f(i+1))$ holds for every $i$ from $0$ to $n-1$.

background

The module supplies a minimal RecognitionStructure consisting only of a type $U$ and a binary predicate $R : U → U → Prop$. This interface is introduced as a compilation stub so that Chain can be stated without importing the full concrete recognition data. Upstream results supply the same minimal shape in the Recognition module, where $U$ is instantiated by the RS-native units (tick and voxel) and $R$ becomes the concrete recognition predicate.

proof idea

The declaration is a direct structure definition. It introduces the three fields n, f, and ok with no further computation or proof obligations inside the structure itself.

why it matters in Recognition Science

Chain supplies the basic object on which flux and conservation are defined. It is referenced by chainFlux (difference of phi values between endpoints), the Conserves class, and the T3 continuity theorem that closed chains carry zero flux. In the broader framework it encodes finite recognition sequences that later support the eight-tick octave and the derivation of conservation from the recognition composition law.

scope and limits

formal statement (Lean)

  11structure Chain (M : RecognitionStructure) where
  12  n : Nat
  13  f : Fin (n+1) → M.U
  14  ok : ∀ i : Fin n, M.R (f i.castSucc) (f i.succ)
  15
  16namespace Chain
  17
  18variable {M : RecognitionStructure} (ch : Chain M)
  19

used by (40)

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

… and 10 more

depends on (13)

Lean names referenced from this declaration's body.