feasible_nonempty

formal source

  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 _ }
 121
 122/-- The constant configuration has log-charge `N * μ`. -/
 123private theorem constant_config_log_charge {N : ℕ} (μ : ℝ) :
 124    log_charge (constant_config μ : Configuration N) = (N : ℝ) * μ := by
 125  unfold log_charge constant_config
 126  simp only [Real.log_exp]
 127  rw [Finset.sum_const, Finset.card_univ, Fintype.card_fin, nsmul_eq_mul]
 128