variational_step_unique

formal source

 287    lower cost, contradicting minimality.
 288
 289    This is the core determinism result: the next state is UNIQUE. -/
 290theorem variational_step_unique {N : ℕ} (hN : 0 < N)
 291    (c : Configuration N)
 292    (next₁ next₂ : Configuration N)
 293    (h₁ : IsVariationalSuccessor c next₁)
 294    (h₂ : IsVariationalSuccessor c next₂) :
 295    next₁.entries = next₂.entries := by
 296  have h_uniform : IsVariationalSuccessor c (constant_config (log_charge c / N) : Configuration N) := by
 297    constructor
 298    · show log_charge (constant_config (log_charge c / N) : Configuration N) = log_charge c
 299      rw [constant_config_log_charge]
 300      exact mul_div_cancel₀ _ (Nat.cast_ne_zero.mpr (Nat.pos_iff_ne_zero.mp hN))
 301    · intro c' hc'
 302      rw [constant_config_total_defect]
 303      have hbound := total_defect_lower_bound hN c'
 304      rw [hc'] at hbound
 305      exact hbound
 306  have h1_eq_min : total_defect next₁ = (N : ℝ) * Jlog (log_charge c / N) := by
 307    have h1le := h₁.2 (constant_config (log_charge c / N) : Configuration N) h_uniform.1
 308    have h1ge := h_uniform.2 next₁ h₁.1
 309    rw [constant_config_total_defect] at h1le h1ge
 310    exact le_antisymm h1le h1ge
 311  have h2_eq_min : total_defect next₂ = (N : ℝ) * Jlog (log_charge c / N) := by
 312    have h2le := h₂.2 (constant_config (log_charge c / N) : Configuration N) h_uniform.1
 313    have h2ge := h_uniform.2 next₂ h₂.1
 314    rw [constant_config_total_defect] at h2le h2ge
 315    exact le_antisymm h2le h2ge
 316  have h1_const :
 317      next₁.entries = (constant_config (log_charge next₁ / N) : Configuration N).entries := by
 318    apply eq_constant_config_of_defect_eq hN next₁
 319    rw [← h₁.1] at h1_eq_min
 320    exact h1_eq_min