total_defect

formal source

  42  entries_pos : ∀ i, 0 < entries i
  43
  44/-- Total defect of a configuration: sum of individual J-costs. -/
  45noncomputable def total_defect {N : ℕ} (c : Configuration N) : ℝ :=
  46  ∑ i : Fin N, LawOfExistence.defect (c.entries i)
  47
  48/-- Total defect is non-negative (each term is non-negative). -/
  49theorem total_defect_nonneg {N : ℕ} (c : Configuration N) : 0 ≤ total_defect c := by
  50  apply Finset.sum_nonneg
  51  intro i _
  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