phi_zero_of_balanced
plain-language theorem explainer
A ledger on any recognition structure with debit equal to credit at every unit has phi vanishing everywhere. Researchers deriving zero-flux results or applying the Recognition Composition Law cite this to reduce balanced cases. The proof is a one-line wrapper that introduces the unit and simplifies using the phi definition together with the balance hypothesis and the subtraction identity.
Claim. Let $L$ be a ledger on a recognition structure $M$. If $L$ satisfies debit$(u)=$credit$(u)$ for every unit $u$, then the associated phi function satisfies phi$(L,u)=0$ for every $u$.
background
The Recognition module opens with the T1 principle that nothing can recognize itself. A RecognitionStructure comprises a set $U$ of units together with a recognition relation $R$. A Ledger on such a structure is a pair of functions assigning integer debit and credit values to each unit in $U$. The phi function on a ledger is the difference debit minus credit, which is the quantity shown to vanish under the balance hypothesis.
proof idea
This is a one-line wrapper. It introduces an arbitrary unit $u$ and then applies simp to the definition of phi, the supplied balance hypothesis at $u$, and the identity $x-x=0$.
why it matters
The lemma is invoked by chainFlux_zero_of_balanced to obtain vanishing flux along any chain when the ledger is balanced. It therefore supplies the elementary conservation step that feeds into flux calculations throughout the Recognition framework and the T1(MP) development.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.