unity_defect_zero

formal source

  57    entries_pos := fun _ => by norm_num }
  58
  59/-- The unity configuration has zero total defect. -/
  60theorem unity_defect_zero {N : ℕ} (hN : 0 < N) :
  61    total_defect (unity_config N hN) = 0 := by
  62  unfold total_defect unity_config
  63  simp only [LawOfExistence.defect_at_one]
  64  exact Finset.sum_const_zero
  65
  66/-! ## The Initial Condition is Forced -/
  67
  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)