`LedgerState`

definition

show as: view math explainer →

module: IndisputableMonolith.Foundation.VariationalDynamics
domain: Foundation
line: 77 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Foundation.VariationalDynamics on GitHub at line 77.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

  74/-! ## Ledger State with Conservation Law -/
  75
  76/-- A ledger state: N entries with positive real ratios, indexed by tick. -/
  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. -/
  83noncomputable def log_charge {N : ℕ} (c : Configuration N) : ℝ :=
  84  ∑ i : Fin N, Real.log (c.entries i)
  85
  86/-- The feasible set: configurations reachable in one tick.
  87    A configuration c' is feasible from c if:
  88    1. All entries remain positive
  89    2. Total log-charge is conserved -/
  90def Feasible {N : ℕ} (c : Configuration N) : Set (Configuration N) :=
  91  { c' : Configuration N | log_charge c' = log_charge c }
  92
  93/-- The current configuration is always feasible (reflexivity). -/
  94theorem self_feasible {N : ℕ} (c : Configuration N) :
  95    c ∈ Feasible c := rfl
  96
  97/-- The feasible set is nonempty (contains the current state). -/
  98theorem feasible_nonempty {N : ℕ} (c : Configuration N) :
  99    Set.Nonempty (Feasible c) := ⟨c, self_feasible c⟩
 100
 101/-! ## The Variational Update Rule -/
 102
 103/-- **Definition (Update Rule)**: The next state is the configuration
 104    that minimizes total defect subject to conservation of log-charge.
 105
 106    This is the "equation of motion" for the ledger. -/
 107def IsVariationalSuccessor {N : ℕ} (current next : Configuration N) : Prop :=

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.