LedgerState
plain-language theorem explainer
LedgerState pairs a Configuration of N positive real ratios with a tick index to represent a discrete state of the recognition ledger. Workers on variational dynamics or thermodynamic bounds cite it when tracking the conserved total log-ratio under J-symmetric evolution. The declaration is a plain record type with no attached computation or proof obligations.
Claim. A ledger state for $N$ entries is a pair $(c, t)$ where $c$ is a configuration of $N$ positive real ratios (i.e., $c :$ Configuration $N$) and $t$ is a natural number indexing the current tick.
background
The module VariationalDynamics supplies the missing update rule for the Recognition Science ledger: state$(t+1)$ is the global argmin of TotalDefect over the feasible set reachable in one tick while preserving the total log-ratio. Configuration, imported from InitialCondition, is the structure whose entries field maps Fin $N$ to positive reals; its total defect is the sum of individual J-costs. The tick constant is the fundamental RS time quantum (one octave equals eight ticks). The conservation law follows from J-symmetry: J$(x)$ = J$(1/x)$ implies that the sum of log-ratios is invariant.
proof idea
The declaration is a structure definition that introduces the record type with exactly two fields: config of type Configuration $N$ and tick of type ℕ. No lemmas or tactics are invoked; the object is introduced by direct record construction.
why it matters
LedgerState supplies the state space for diagonalHamiltonian in HamiltonianEmergence and for ledger_identity plus totalInfoCost in InformationIsLedger. It encodes the conserved charge that appears in the module's update principle and in the eight-tick dissipation limit. The structure therefore closes the gap between LawOfExistence (J-uniqueness) and the explicit dynamics required by F-008.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.