log_charge

formal source

  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 :=
 108  next ∈ Feasible current ∧
 109  ∀ c' ∈ Feasible current, total_defect next ≤ total_defect c'
 110
 111/-- **Total defect** is non-negative for any configuration. -/
 112theorem total_defect_nonneg' {N : ℕ} (c : Configuration N) :
 113    0 ≤ total_defect c := total_defect_nonneg c