MinimalLedger
plain-language theorem explainer
MinimalLedger defines a structure on any type X that pairs an integer charge map with the requirement that charges sum to zero over every transaction list. Researchers tracing the meta-principle derivation of double-entry accounting would cite this as the formal ledger carrier. The declaration is a direct structure definition with no proof obligations or computational content.
Claim. A minimal ledger on a carrier set $X$ consists of a charge function $c: X → ℤ$ together with the axiom that the sum of $c(x)$ over every finite list of elements is zero.
background
The Meta-Principle module starts from the statement that empty recognition is impossible and derives the necessity of a ledger to record pairings. This structure supplies the minimal data for conservation: an integer-valued charge on elements of X and the global sum-zero condition on transactions. Upstream structures such as NucleosynthesisTiers.of supply discrete φ-tier densities while CPM2D.Hypothesis and PhiForcingDerived.of provide the constants and J-cost functionals that later instantiate concrete ledgers.
proof idea
The declaration is a direct structure definition that introduces the two fields charge and conserved with no lemmas, tactics, or reduction steps.
why it matters
This structure realizes the first implication in the module chain MP → Ledger → φ. It supplies the formal object on which later results such as self-similarity forcing and the eight-tick octave can act. No downstream uses are recorded, leaving open its integration with the phi-ladder mass formula and the alpha band.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.