L
plain-language theorem explainer
The definition supplies a concrete ledger L on the main recognition structure M whose debit and credit maps are both the constant function 1. Workers deriving conservation laws or quadratic limits from the Recognition Composition Law cite this as the base ledger instance. The construction is a direct record literal with no auxiliary lemmas or computation.
Claim. Let $M$ be the recognition structure with carrier set $U$ and recognition relation $R$. The ledger $L$ on $M$ is the structure whose debit map sends every element of $U$ to $1$ and whose credit map sends every element of $U$ to $1$.
background
Module Recognition opens with the statement of T1 (MP): Nothing cannot recognize itself. A Ledger on a RecognitionStructure consists of two maps, debit and credit, each from the carrier $M.U$ to the integers; these maps record the accounting of recognitions. The auxiliary definition M instantiates the structure with carrier $U$ and relation recog. An upstream sibling in Cycle3 supplies an analogous ledger on the 3-cycle whose debit and credit are both zero and which carries a Conserves instance.
proof idea
The declaration is a one-line structure literal that directly populates the Ledger record with the two constant functions.
why it matters
This ledger is the base object referenced by the graded Cycle construction in LedgerAlgebra and by the standardLagrangian, kineticAction and standardEL definitions in QuadraticLimit; those objects in turn feed the Noether theorem that extracts momentum conservation from space-translation invariance. It therefore supplies the concrete accounting layer required by the Recognition Composition Law and by the T0-T8 forcing chain that derives $D=3$ and the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.