Feasible

formal source

  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
 114
 115/-! ## Uniform candidate and Jensen helpers -/
 116
 117/-- Constant-entry configuration with value `exp μ` in every slot. -/
 118private noncomputable def constant_config {N : ℕ} (μ : ℝ) : Configuration N :=
 119  { entries := fun _ => Real.exp μ
 120    entries_pos := fun _ => Real.exp_pos _ }