Ledger
plain-language theorem explainer
A Ledger packages a list of RecognitionEvents with a predicate ensuring every event appears exactly as often as its reciprocal. Foundation researchers cite the structure when constructing the double-entry layer forced by J-symmetry. The declaration is a plain inductive structure with no proof obligations or computational content.
Claim. A ledger is a pair consisting of a finite list $L$ of recognition events together with a proof that $L$ is balanced: for every event $e$ the multiplicity of $e$ in $L$ equals the multiplicity of its reciprocal event.
background
The LedgerForcing module establishes that J-symmetry on positive ratios forces a double-entry bookkeeping structure. RecognitionEvent is the basic datum: a triple (source, target, ratio) with ratio positive real. balanced_list is the predicate requiring that every event $e$ occurs exactly as often as reciprocal($e$), where reciprocal inverts the ratio and swaps source with target. Upstream cost definitions from ObserverForcing and MultiplicativeRecognizerL4 supply the J-cost on each event, which the ledger structure later aggregates.
proof idea
The declaration is a direct structure definition. It simply bundles the events list with the balanced_list hypothesis as a single type; no lemmas or tactics are applied.
why it matters
The structure supplies the canonical data type for the double-entry constraint that the module derives from J-symmetry and the Recognition Composition Law. It occupies the base of the forcing chain that later results use to recover physical ledgers and cost accounting. No downstream uses are yet recorded, leaving open the question of how concrete physical processes instantiate non-trivial balanced lists.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.