L
plain-language theorem explainer
L defines the zero ledger on the three-cycle recognition structure M. Workers on conservation laws and graded ledgers cite it as the trivial base case that satisfies the Conserves predicate by construction. The definition is a direct assignment of zero debit and credit maps, with the accompanying instance discharged by a single simplification of chainFlux once phi is identically zero.
Claim. Let $M$ be the recognition structure on the set of three elements with successor relation forming a directed cycle. The ledger $L$ on $M$ is the map sending every vertex to debit value zero and credit value zero. This $L$ satisfies the conservation property that the flux of any closed chain is zero.
background
The module Recognition.Cycle3 builds a minimal cyclic example inside the Recognition framework. M is the recognition structure whose underlying set is Fin 3 and whose relation R is the successor map modulo 3, producing a single 3-cycle. A Ledger on such an M consists of debit and credit functions from the vertex set to integers. chainFlux of a ledger along a chain is defined as phi at the last vertex minus phi at the head. The Conserves class requires that every closed chain (head equal to last) has chainFlux exactly zero; its doc-comment explicitly links this to T2 atomicity.
proof idea
The definition directly constructs L by setting both debit and credit to the constant-zero function on the vertex set of M. The Conserves instance is obtained by a one-line wrapper: introduce an arbitrary closed chain, then apply simp on the definitions of chainFlux and phi together with the closed-chain hypothesis.
why it matters
L supplies the base case for the Cycle and GradedLedger structures in LedgerAlgebra and is invoked by standardLagrangian, standardHamiltonian, kineticAction and the Noether theorem establishing momentum conservation from space-translation invariance. It therefore anchors the passage from the recognition ledger to the quadratic limit of the J-action. The construction directly instantiates the T2 atomicity step of the forcing chain and supplies the zero-flux starting point for all subsequent conservation statements.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.