Chain
plain-language theorem explainer
The abbreviation re-exports the Chain structure, a sequence of recognition steps satisfying the relation R on a RecognitionStructure, into the RRF namespace. Ledger algebraists and flux modelers cite it when constructing conservation statements or graded ledgers over recognition paths. It is realized as a direct alias to the upstream definition with no added content.
Claim. A chain over a recognition structure $M$ consists of a length $n$, a map $f : Fin(n+1) → M.U$, and a proof that $M.R(f(i), f(i+1))$ holds for every $i < n$.
background
The RRF.Core.Recognition module supplies a namespace bridge that re-exports core Recognition definitions for use inside the Recognition Science framework. RecognitionStructure supplies a carrier type U together with a binary relation R. Chain assembles finite paths in which each consecutive pair satisfies R. The upstream Chain structure is defined with minimal axioms for standalone compilation: it records the length n, the path function f, and the recognition condition ok.
proof idea
This is a one-line alias that directly re-exports the Chain definition from IndisputableMonolith.Recognition.
why it matters
The re-export lets downstream modules such as LedgerAlgebra.GradedLedger and Chain.chainFlux reference recognition sequences under the RRF namespace. It supports conservation statements (Conserves) and flux calculations that close the recognition ledger. In the broader framework the structure supplies the discrete paths needed for the forcing chain T0–T8 and for the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.