L
plain-language theorem explainer
This definition constructs the constant ledger on the base recognition structure M, assigning debit and credit value 1 to every carrier element. Researchers deriving quadratic actions or applying Noether theorems to translation-invariant functionals cite it as the unit case for graded ledgers. The definition is a direct structure constructor with no computation or lemmas.
Claim. Let $M$ be the recognition structure with carrier $U$ and recognition relation $R$. Define the ledger $L$ on $M$ by setting the debit map and credit map to the constant function with value $1$ on every element of $U$.
background
The Recognition module opens with T1, the statement that nothing can recognize itself. A Ledger on a recognition structure $M$ consists of two maps from the carrier $U$ to the integers, called debit and credit. The sibling definition M supplies the concrete recognition structure whose carrier is the type $U$ and whose recognition map is recog. Upstream Cycle3 supplies a contrasting three-cycle structure together with its zero ledger, which carries an explicit conservation instance.
proof idea
One-line wrapper that directly constructs the Ledger structure by supplying the two constant-1 functions.
why it matters
L supplies the unit ledger that appears in the construction of Cycle and GradedLedger in LedgerAlgebra and is invoked by standardLagrangian, kineticAction, standardEL, and standardHamiltonian in the Action modules. It therefore participates in the passage from the Recognition Composition Law to the Euler-Lagrange equation and the Noether-derived momentum conservation theorem. Within the forcing chain it instantiates the minimal non-zero ledger compatible with the eight-tick octave and the emergence of three spatial dimensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.