chainFlux_zero_of_balanced
plain-language theorem explainer
The theorem establishes that chain flux vanishes for any recognition chain when the ledger is balanced, with debits equaling credits for every unit. Researchers deriving conservation properties or zero-net configurations in the Recognition framework would cite it to simplify calculations in closed systems. The proof is a direct one-line delegation to the base Recognition module's corresponding lemma.
Claim. Let $M$ be a recognition structure, $L$ a ledger on $M$, and $ch$ a chain in $M$. If $L$ is balanced, i.e., for all units $u$ the debit of $u$ equals the credit of $u$, then the chain flux of $L$ along $ch$ equals zero.
background
This declaration resides in the RRF.Core.Recognition module, a re-export bridge that makes Recognition definitions available under the RRF namespace. A RecognitionStructure supplies a type $U$ of units and a binary recognition relation $R$. A Chain is a finite sequence of units $f_0, f_1, ..., f_n$ such that consecutive pairs satisfy $R$. The Ledger records double-entry bookkeeping via debit and credit maps. chainFlux is defined as the difference in the phi-potential between the chain's terminal and initial units: phi(last) minus phi(head).
proof idea
The proof is a one-line wrapper that applies the chainFlux_zero_of_balanced lemma from the base IndisputableMonolith.Recognition module, forwarding the ledger $L$, chain $ch$, and balance hypothesis $hbal$.
why it matters
The result supplies the zero-flux conservation law needed for RRF derivations, feeding directly into the twoStep chain construction where flux is shown to vanish. It re-exports the balanced-ledger property from the core Recognition module, aligning with the framework's treatment of recognition as a closed accounting system. No open scaffolding remains; the declaration completes the bridge for downstream RRF flux identities.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.