LedgerState
plain-language theorem explainer
LedgerState pairs a configuration of N positive real ratios with a discrete tick index to track the conserved log-ratio charge. Researchers modeling variational ledger evolution cite this to enforce the update rule state(t+1) equals the global J-cost minimizer over feasible successors. The declaration is a bare structure definition carrying no proof obligations or computational content.
Claim. A ledger state for $N$ entries consists of a configuration $c$ of $N$ positive real ratios together with a tick index $t$.
background
The VariationalDynamics module supplies the missing update rule for the Recognition Science ledger: state(t+1) is the argmin of total defect over the feasible set that preserves the sum of log-ratios. Configuration N, imported from InitialCondition, is the structure whose entries field maps Fin N to positive reals with the positivity predicate. The tick field is the fundamental RS time quantum, one octave of which equals eight ticks.
proof idea
This is a structure definition with no proof body. It directly introduces the two fields config and tick without any lemmas or tactics.
why it matters
LedgerState is the central carrier for the conservation law that makes the constrained J-cost minimization well-defined. Downstream it is used to construct the diagonal Hamiltonian in HamiltonianEmergence and to prove ledger_identity together with non-negativity of total information cost in the Information modules. It therefore closes the gap between the energy landscape (LawOfExistence, Determinism) and the actual dynamics required by the F-008 update principle.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.