pith. machine review for the scientific record. sign in
structure definition def or abbrev high

LedgerState

show as:
view Lean formalization →

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.

claimA 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 in Recognition Science

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.

scope and limits

formal statement (Lean)

  77structure LedgerState (N : ℕ) where
  78  config : Configuration N
  79  tick : ℕ
  80
  81/-- Total log-ratio of a configuration: the conserved quantity.
  82    This is the "charge" of the ledger — preserved under evolution. -/

used by (40)

From the project-wide theorem graph. These declarations reference this one in their body.

… and 10 more

depends on (17)

Lean names referenced from this declaration's body.