chainFlux
Chain flux is the integer difference in the phi evaluation between the final and initial elements of a recognition chain under a fixed ledger. Modelers of discrete conservation laws in recognition structures cite this definition when deriving zero-flux lemmas for closed loops. The definition is realized by direct subtraction of the two endpoint phi values.
claimFor a ledger $L$ on recognition structure $M$ and a chain $ch$ in $M$, the chain flux equals $phi(L, last(ch)) - phi(L, head(ch))$.
background
A Ledger equips a recognition structure with debit and credit maps from its universe $U$ to the integers. A Chain is a finite sequence of elements of $U$ linked by the recognition relation $R$, with head and last extracting the initial and terminal elements. The module opens under the MP principle that nothing cannot recognize itself, and the definition re-exports the same chain-flux expression already present in the Chain module.
proof idea
One-line wrapper that subtracts the phi value at the head from the phi value at the last element of the chain.
why it matters in Recognition Science
The definition supplies the left-hand side for the Conserves class, which states that head-equals-last implies zero flux, and thereby supports the T3 continuity theorem. It also feeds the zero-flux lemmas for balanced ledgers and loops, closing the atomicity step in the T0-T8 forcing chain.
scope and limits
- Does not define the explicit form of the phi function.
- Does not extend the notion to infinite or cyclic chains.
- Does not impose balance or conservation conditions on the ledger.
formal statement (Lean)
59def chainFlux {M} (L : Ledger M) (ch : Chain M) : ℤ :=
proof body
Definition body.
60 phi L (Chain.last ch) - phi L (Chain.head ch)
61