Conserves
plain-language theorem explainer
The Conserves class encodes that a ledger L on recognition structure M has zero net flux on any closed chain. Ledger modelers and chain continuity proofs cite it to enforce atomicity of recognition postings. The declaration is a direct class definition packaging the universal quantification over loops into a Prop field for typeclass use.
Claim. A ledger $L$ on structure $M$ conserves when, for every chain $ch$, if the head equals the last element then the flux of $L$ on $ch$ is zero, where flux is defined as the difference in the recognition potential between the last and head elements.
background
A RecognitionStructure $M$ consists of a carrier set $U$ together with a binary recognition relation $R$. A Ledger $L$ on $M$ supplies integer-valued debit and credit maps on $U$. A Chain on $M$ is a finite sequence of elements of $U$ linked by successive applications of $R$, with head and last extracting the initial and terminal elements. The chainFlux operation subtracts the potential at the head from the potential at the last element. The module opens under the T1 (MP) heading that nothing recognizes itself, while the upstream Chain module already records the same Conserves class under the label T2 (Atomicity).
proof idea
The declaration is a class definition whose single field is the stated universal quantification. It functions as a one-line wrapper that packages the conservation statement for downstream typeclass resolution.
why it matters
This supplies the conservation axiom that T3_continuity in the Chain module invokes directly via Conserves.conserve. It also discharges the hypothesis in chainFlux_zero_of_loop and supplies the instance used by Cycle3.L and SimpleLedger. Within the framework it realizes the T2 atomicity step of the forcing chain, guaranteeing zero net flux on closed loops and thereby supporting the later derivation of the eight-tick octave and three spatial dimensions. It leaves open how the property interacts with the J-uniqueness fixed point of T5.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.