balanced_config_zero_cost

formal source

 135
 136/-- **THEOREM IC-005.10**: The balanced configuration (all ratios = 1) has zero total cost.
 137    This is the ground state of the ledger — trivially verifiable. -/
 138theorem balanced_config_zero_cost (N : ℕ) :
 139    totalJCost (N := N) { ratios := fun _ => 1, ratios_pos := fun _ => one_pos } = 0 := by
 140  unfold totalJCost
 141  simp [Cost.Jcost_unit0]
 142
 143/-- Helper: A sum of non-negative reals equals 0 iff each term is 0. -/
 144private lemma sum_nonneg_zero_iff {N : ℕ} (f : Fin N → ℝ)
 145    (hnn : ∀ i, 0 ≤ f i) :
 146    ∑ i : Fin N, f i = 0 ↔ ∀ i : Fin N, f i = 0 := by
 147  rw [Finset.sum_eq_zero_iff_of_nonneg (fun i _ => hnn i)]
 148  simp [Finset.mem_univ]
 149
 150/-- **THEOREM IC-005.11**: A configuration is balanced iff its total J-cost is zero.
 151    This means balance verification is equivalent to a single sum = 0 check,
 152    which is O(N) in the number of ledger entries. -/
 153theorem verification_equivalence {N : ℕ} (config : LedgerConfig N) :
 154    (∀ i : Fin N, config.ratios i = 1) ↔ totalJCost config = 0 := by
 155  unfold totalJCost
 156  rw [sum_nonneg_zero_iff _ (fun i => Cost.Jcost_nonneg (config.ratios_pos i))]
 157  constructor
 158  · intro h i
 159    rw [h i]; exact Cost.Jcost_unit0
 160  · intro h i
 161    have hi := h i
 162    rw [Cost.Jcost_eq_sq (config.ratios_pos i).ne'] at hi
 163    have hden : 2 * config.ratios i ≠ 0 := ne_of_gt (by linarith [config.ratios_pos i])
 164    have hsq : (config.ratios i - 1)^2 = 0 := by
 165      rwa [div_eq_zero_iff, or_iff_left hden] at hi
 166    nlinarith [sq_nonneg (config.ratios i - 1)]
 167
 168/-! ## IV. Complexity Classes for RS Physics -/