unity_config

formal source

  52  exact LawOfExistence.defect_nonneg (c.entries_pos i)
  53
  54/-- The zero-defect configuration: all entries equal to 1. -/
  55def unity_config (N : ℕ) (_hN : 0 < N) : Configuration N :=
  56  { entries := fun _ => 1
  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))