Conserves
plain-language theorem explainer
Conserves packages the zero-flux condition on closed chains for any ledger L. Chain-based models of conservation in recognition structures cite it to enforce loop balance. The class definition encodes the universal quantification over chains with matching endpoints directly.
Claim. A ledger $L$ on recognition structure $M$ conserves if for every chain $ch$, head$(ch)=$last$(ch)$ implies chainFlux$(L,ch)=0$.
background
Chain is a structure over RecognitionStructure $M$ with length $n$, sequence $f:$ Fin$(n+1)→ U$, and consecutive units linked by relation $R$. Head and last extract the endpoints. Ledger equips each unit with debit and credit maps to integers. chainFlux computes phi$(L,$last$)$ minus phi$(L,$head$)$, where phi aggregates ledger entries. The module supplies minimal stubs for standalone compilation of these structures. Upstream, tick fixes the base time quantum at 1 in RS-native units.
proof idea
The declaration is a class definition that directly introduces the Prop with the conserve field. No lemmas or tactics are applied; the property is asserted by the class construction itself.
why it matters
It supplies the conservation hypothesis for T3_continuity and chainFlux_zero_of_loop, which extract zero flux on loops. The same class appears in the Recognition module and supports concrete instances in Cycle3 and SimpleLedger. It underpins atomicity by guaranteeing flux cancellation on closed chains, consistent with unique postings per tick.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.