chainFlux
plain-language theorem explainer
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.
Claim. For 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.