chainFlux_zero_of_loop
plain-language theorem explainer
A closed chain in the recognition structure carries zero net flux under any conserving ledger. Researchers modeling conservation laws or cycle closures in the Recognition framework cite this when handling loops on the phi-ladder. The proof is a direct one-line application of the Conserves.conserve axiom to the supplied head-last equality.
Claim. Let $L$ be a ledger on recognition structure $M$ that satisfies conservation. For any chain $ch$ with head equal to last, the flux of $L$ along $ch$ is zero, where flux equals the difference of the phi evaluation at last minus the phi evaluation at head.
background
A recognition structure supplies a universe $U$ together with a recognition relation $R$. A chain is a finite sequence of elements from $U$ such that each consecutive pair satisfies $R$. The ledger $L$ equips each element of $U$ with integer debit and credit values. Chain flux is defined as the difference of the phi map evaluated at the chain's last element minus its head element. The Conserves class asserts that every closed chain (head equal to last) has zero flux. The local module context is the T1 principle that nothing can recognize itself.
proof idea
The proof is a one-line wrapper that applies the conserve field of the Conserves instance directly to the given chain and the head-last equality hypothesis.
why it matters
This lemma supplies the basic conservation fact for closed paths that feeds into atomicity arguments in the upstream Chain module. It supports the T1 (MP) setting by ensuring flux vanishes on loops, consistent with the self-similar fixed point and eight-tick octave in the forcing chain. No downstream uses are recorded, leaving its role as a foundational conservation primitive.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.