153theorem verification_equivalence {N : ℕ} (config : LedgerConfig N) : 154 (∀ i : Fin N, config.ratios i = 1) ↔ totalJCost config = 0 := by
proof body
Tactic-mode proof.
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 -/ 169 170/-- The physics complexity structure: core claim. -/
used by (1)
From the project-wide theorem graph. These declarations reference this one in their body.