Ledger
Ledger defines a carrier type with optional state and tick bookkeeping fields for Recognition Science specifications. Modules handling observable payloads cite it to project canonical states without added structure. The declaration is a direct structure with defaults for the optional components, drawing on the fundamental tick from Constants.
claimA structure consisting of a carrier type $C$, an optional state $s : Option(C)$, and an optional tick map $t : Option(C → ℕ)$.
background
In RecogSpec.Core, Ledger supplies a minimal carrier augmented with bookkeeping so that downstream projections remain canonical. It imports the tick definition from Constants, where tick is the fundamental RS time quantum τ₀ = 1, and the sibling Bridge structure is declared immediately afterward over Ledger. The module also imports ObservablePayloads, preparing for dimensionless and absolute pack constructions.
proof idea
Direct structure definition that introduces the three fields with default values for state and tick. No lemmas or tactics are invoked.
why it matters in Recognition Science
Ledger supplies the base carrier for the RecogSpec module and enables the Bridge structure that follows. It aligns with RS-native units by referencing the tick quantum, consistent with the eight-tick octave in the forcing chain. No downstream uses appear in the head, leaving its role as foundational scaffolding.
scope and limits
- Does not specify any concrete carrier type or its properties.
- Does not enforce relations between state and tick fields.
- Does not connect to J-uniqueness, phi-ladder, or mass formulas.
- Does not address spatial dimensions or Berry thresholds.
formal statement (Lean)
11structure Ledger where
12 Carrier : Type
13 state : Option Carrier := none
proof body
Definition body.
14 tick : Option (Carrier → ℕ) := none
15
16/-- Bridge over a ledger. -/