theorem
proved
tactic proof
zero_defect_iff_unity
show as:
view Lean formalization →
formal statement (Lean)
71theorem zero_defect_iff_unity {N : ℕ} (_hN : 0 < N) (c : Configuration N) :
72 total_defect c = 0 ↔ ∀ i, c.entries i = 1 := by
proof body
Tactic-mode proof.
73 constructor
74 · intro h_zero
75 have h_terms : ∀ i, LawOfExistence.defect (c.entries i) = 0 := by
76 by_contra h_not
77 push_neg at h_not
78 obtain ⟨j, hj⟩ := h_not
79 have hj_pos : 0 < LawOfExistence.defect (c.entries j) := by
80 have h_nn := LawOfExistence.defect_nonneg (c.entries_pos j)
81 exact lt_of_le_of_ne h_nn (Ne.symm hj)
82 have h_sum_pos : 0 < total_defect c := by
83 calc 0 < LawOfExistence.defect (c.entries j) := hj_pos
84 _ ≤ ∑ i : Fin N, LawOfExistence.defect (c.entries i) := by
85 apply Finset.single_le_sum (f := fun i => LawOfExistence.defect (c.entries i))
86 (fun i _ => LawOfExistence.defect_nonneg (c.entries_pos i))
87 (Finset.mem_univ j)
88 linarith
89 intro i
90 exact (LawOfExistence.defect_zero_iff_one (c.entries_pos i)).mp (h_terms i)
91 · intro h_all_one
92 simp only [total_defect]
93 apply Finset.sum_eq_zero
94 intro i _
95 rw [h_all_one i]
96 exact LawOfExistence.defect_one
97
98/-- **Theorem**: The unity configuration achieves the global minimum of total defect. -/