Ledger
plain-language theorem explainer
The Ledger structure equips any recognition structure with two integer-valued maps on its units, one for debits and one for credits. Chain modelers would cite it when formalizing accounting or flux tracking inside recognition cycles. The declaration is introduced by a direct structure definition with no added axioms or lemmas.
Claim. Let $M$ be a recognition structure with underlying type $U$. A ledger on $M$ consists of two functions $d,c:U→ℤ$, where $d$ records debits and $c$ records credits.
background
The module supplies a minimal RecognitionStructure consisting of a type $U$ together with a binary relation $R$ on $U$, serving as a stub for standalone compilation. Upstream results include the RS-native units definition that fixes the gauge with one tick as the time unit and one voxel as the length unit, enforcing $c=1$. The Recognition module provides a concrete instance whose $U$ is the unit type and whose relation holds by structural equality.
proof idea
The declaration is a direct structure definition that packages the two maps without invoking lemmas or tactics.
why it matters
This definition supplies the basic accounting data for the chain module and stands ready for conservation statements such as Conserves among the sibling declarations. It forms part of the minimal scaffolding that precedes imposition of atomicity and continuity axioms in the chain. No downstream uses are recorded, leaving open how it will integrate with the eight-tick octave or the recognition composition law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.