theorem
proved
zero_defect_iff_unity
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Foundation.InitialCondition on GitHub at line 71.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
-
of -
of -
Configuration -
total_defect -
defect -
defect_nonneg -
defect_one -
defect_zero_iff_one -
of -
Configuration -
of -
of -
total -
total
used by
formal source
68/-- **Theorem (F-005 core)**: The unity configuration is the unique
69 zero-total-defect configuration.
70 Every entry must be 1 for total defect to vanish. -/
71theorem zero_defect_iff_unity {N : ℕ} (_hN : 0 < N) (c : Configuration N) :
72 total_defect c = 0 ↔ ∀ i, c.entries i = 1 := by
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. -/
99theorem unity_is_global_minimum {N : ℕ} (hN : 0 < N) (c : Configuration N) :
100 total_defect (unity_config N hN) ≤ total_defect c := by
101 rw [unity_defect_zero hN]