chainFlux_zero_of_balanced
plain-language theorem explainer
Balanced ledgers force zero flux along any recognition chain. Researchers tracing conservation in the Recognition Science forcing chain cite this when closing net-flow arguments for closed systems. The proof is a one-line simp wrapper that unfolds the flux definition and applies the zero-potential result for balanced ledgers.
Claim. If $L$ is a ledger over recognition structure $M$ satisfying $L.debit(u)=L.credit(u)$ for every unit $u$, then chain flux of $L$ along any chain $ch$ equals zero.
background
Ledger is the structure carrying debit and credit maps from the universe of a recognition structure to integers. Chain is the finite sequence of units connected by the recognition relation. chainFlux is defined as the difference in the phi potential evaluated at the chain's last and head elements. The module documentation opens with T1 (MP): nothing cannot recognize itself. Upstream Chain and chainFlux definitions appear in the Chain module; phi_zero_of_balanced supplies the key fact that the potential vanishes under the balance hypothesis.
proof idea
One-line wrapper that applies simp to the chainFlux definition together with phi_zero_of_balanced instantiated at the given ledger and balance hypothesis.
why it matters
The lemma supplies the zero-flux conservation step that feeds the twoStep example inside the same module and is re-exported as the bridge theorem in RRF.Core.Recognition. It closes the balanced case inside the T1 recognition principle and supports later steps that require net flux to vanish on closed ledgers.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.