Chain
plain-language theorem explainer
Chain encodes a finite sequence of n+1 elements drawn from the universe U of a RecognitionStructure M, with the requirement that each consecutive pair satisfies the recognition relation R. Modelers of recognition sequences in the T1 forcing step cite this structure when building conservation statements or ledger flux calculations. The declaration is a bare structure definition that directly packages the length, the indexed map, and the adjacency predicate with no further proof obligations.
Claim. Given a recognition structure $M = (U, R)$, a chain of length $n$ is a map $f : [0..n] → U$ together with the assertion that $R(f(i), f(i+1))$ holds for every $i = 0, …, n-1$.
background
RecognitionStructure is the minimal pair consisting of a type U (the universe of recognizable objects) and a binary relation R : U → U → Prop. In the Recognition module the concrete instance M is obtained by setting U to the RS-native unit type and R to the structural equality predicate recog. The upstream Chain structure in IndisputableMonolith.Chain supplies the identical signature for standalone compilation, confirming that the present declaration is the Recognition-specific specialization. The module opens with the T1 statement that nothing can recognize itself, which supplies the local theoretical setting for all subsequent chain constructions.
proof idea
The declaration is a structure definition with an empty proof body. It simply records the three fields n, f, and ok; no lemmas or tactics are invoked.
why it matters
Chain supplies the primitive object on which conservation and flux are defined. It is used by GradedLedger, chainFlux, Conserves, and last, all of which appear in the ledger-algebra layer that enforces inflow = outflow at every vertex. The structure therefore realizes the T1 (MP) step of the forcing chain and serves as the common substrate for the eight-tick octave and D = 3 constructions that follow.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.