262theorem variational_step_exists {N : ℕ} (hN : 0 < N) 263 (c : Configuration N) : 264 ∃ next : Configuration N, IsVariationalSuccessor c next := by
proof body
Term-mode proof.
265 let μ := log_charge c / N 266 use (constant_config μ : Configuration N) 267 constructor 268 · show log_charge (constant_config μ : Configuration N) = log_charge c 269 rw [constant_config_log_charge] 270 unfold μ 271 exact mul_div_cancel₀ _ (Nat.cast_ne_zero.mpr (Nat.pos_iff_ne_zero.mp hN)) 272 · intro c' _hc' 273 rw [constant_config_total_defect] 274 have hbound := total_defect_lower_bound hN c' 275 rw [_hc'] at hbound 276 unfold μ 277 exact hbound 278 279/-! ## Uniqueness of the Variational Step -/ 280 281/-- **Theorem (Variational Step Uniqueness)**: 282 If two configurations both minimize total defect over the feasible set, 283 they are identical. 284 285 Proof uses strict convexity of J: if c₁ ≠ c₂ both minimize total J-cost, 286 their midpoint (adjusted to satisfy the constraint) would have strictly 287 lower cost, contradicting minimality. 288 289 This is the core determinism result: the next state is UNIQUE. -/
used by (1)
From the project-wide theorem graph. These declarations reference this one in their body.