135theorem uniformChargeMesh_excess_zero (N : ℕ) (m : ℤ) : 136 annularExcess (uniformChargeMesh N m) = 0 := by
proof body
Term-mode proof.
137 unfold annularExcess annularCost annularTopologicalFloor 138 rw [sub_eq_zero] 139 apply Finset.sum_congr rfl 140 intro n _ 141 simpa [uniformChargeMesh] using uniformRingSample_cost_eq_topologicalFloor n.val m 142 143/-- A zero of ζ in the critical strip with Re > 1/2 would create 144 a defect with unbounded annular cost, violating cost-covering. 145 146 This is the key contradiction lemma. -/
used by (3)
From the project-wide theorem graph. These declarations reference this one in their body.