Ledger
plain-language theorem explainer
Ledger equips a RecognitionStructure M with integer-valued debit and credit maps on its carrier U. Workers on recognition lattices or conserved quantities in the T1-T8 chain would cite the structure when introducing balance tracking. The declaration is a direct record definition followed by a one-line carrier projection that returns M.U.
Claim. Let $M$ be a recognition structure with carrier $U$. A ledger on $M$ consists of maps debit, credit : $U → ℤ$. The carrier of any such ledger is the underlying type $U$.
background
RecognitionStructure is the minimal pair (U : Type, R : U → U → Prop) that encodes a recognition relation on a universe. The local module instantiates M via the RS-native U (gauge τ₀ = 1 tick, ℓ₀ = 1 voxel, c = 1) and a structural-equality recognition predicate. The module heading records T1 (MP): Nothing cannot recognize itself, supplying the immediate theoretical setting for any ledger construction.
proof idea
The structure is introduced by direct record declaration with the two integer maps. The Carrier projection is a one-line wrapper that simply returns M.U.
why it matters
The definition supplies the primitive integer accounting layer required before any defectDist or J-cost balance can be stated inside the recognition monolith. It sits immediately after the RecognitionStructure stub and before any use of the Recognition Composition Law or phi-ladder mass formulas. No downstream theorems are recorded, indicating it functions as an open interface for later conservation statements.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.