chainFlux
plain-language theorem explainer
Chain flux computes the integer difference in phi valuation between the terminal and initial elements of a recognition chain on a given ledger. Researchers establishing conservation laws or zero-flux lemmas in the RRF core cite this definition when handling closed chains. The implementation is a one-line re-export that delegates directly to the base Recognition.chainFlux computation.
Claim. Let $M$ be a recognition structure, $L$ a ledger on $M$, and $ch$ a chain in $M$. The chain flux is defined as $phi(L, last(ch)) - phi(L, head(ch))$, where $phi$ is the valuation map on the ledger.
background
The RRF.Core.Recognition module re-exports core concepts from the base Recognition library. A RecognitionStructure consists of a type U equipped with a binary recognition relation R. A Chain is a finite sequence of elements in U connected by successive recognitions, given as a structure carrying length n, a map from Fin(n+1) to U, and proofs that each consecutive pair satisfies the relation R. A Ledger supplies double-entry bookkeeping for recognition events.
proof idea
This is a one-line wrapper that applies the base chainFlux definition from the Recognition module.
why it matters
This definition supplies the flux operation required by the Conserves class and the T3_continuity theorem, which establish zero flux for closed chains (head equal to last) under conservation. It bridges the original Recognition framework to the RRF re-export layer, supporting atomicity and continuity results. Parent results include chainFlux_zero_of_loop and chainFlux_zero_of_balanced, which derive zero flux from loop or balance conditions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.