Ledger
plain-language theorem explainer
Ledger supplies a carrier type with optional state and tick bookkeeping fields for canonical projections in Recognition Science specifications. Workers on observable payloads or bridges reference this structure to avoid extra data layers. The declaration is a plain structure with default none values for the optional components.
Claim. A ledger consists of a carrier type $C$ together with an optional element of $C$ and an optional map $C → ℕ$ (the tick function), both defaulting to none.
background
The upstream tick definition supplies the fundamental RS time quantum τ₀ = 1, with one octave equal to 8 ticks. The sibling Bridge structure is defined directly over a Ledger instance. The module sits inside RecogSpec and imports ObservablePayloads, establishing a setting where ledgers carry minimal bookkeeping so that downstream projections remain canonical without added structure.
proof idea
This is a structure definition with default values; no lemmas or tactics are applied.
why it matters
Ledger supplies the base carrier for the Bridge structure that follows in the same module. It anchors the optional tick field to the fundamental time quantum from Constants, supporting the eight-tick octave in the T7 step of the forcing chain. No downstream uses are recorded in the supplied graph.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.