pith. machine review for the scientific record. sign in
theorem proved term proof

unity_is_optimal

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 246theorem unity_is_optimal {N : ℕ} (hN : 0 < N) (c : Configuration N)
 247    (h_zero_charge : log_charge c = 0) :
 248    IsVariationalSuccessor c (unity_config N hN) := by

proof body

Term-mode proof.

 249  constructor
 250  · show log_charge (unity_config N hN) = log_charge c
 251    rw [unity_log_charge_zero hN, h_zero_charge]
 252  · intro c' _
 253    rw [unity_defect_zero hN]
 254    exact total_defect_nonneg c'
 255
 256/-- **Theorem (Variational Step Existence)**:
 257    A total-defect minimizer always exists in the feasible set.
 258
 259    The proof constructs the minimizer explicitly: it is the configuration
 260    where every entry equals exp(log_charge(c) / N), distributing the
 261    conserved charge equally. This is the AM-GM-optimal configuration. -/

depends on (19)

Lean names referenced from this declaration's body.