totalJCost

formal source

 122  ratios_pos : ∀ i, ratios i > 0
 123
 124/-- Total J-cost of a ledger configuration. -/
 125noncomputable def totalJCost {N : ℕ} (config : LedgerConfig N) : ℝ :=
 126  ∑ i : Fin N, Jcost (config.ratios i)
 127
 128/-- **THEOREM IC-005.9**: Total J-cost is non-negative. -/
 129theorem total_jcost_nonneg {N : ℕ} (config : LedgerConfig N) :
 130    totalJCost config ≥ 0 := by
 131  unfold totalJCost
 132  apply Finset.sum_nonneg
 133  intro i _
 134  exact Cost.Jcost_nonneg (config.ratios_pos i)
 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