uniformChargeMesh_excess_zero

formal source

 132  simp [Finset.sum_const, nsmul_eq_mul]
 133
 134/-- The uniform charge mesh has zero annular excess. -/
 135theorem uniformChargeMesh_excess_zero (N : ℕ) (m : ℤ) :
 136    annularExcess (uniformChargeMesh N m) = 0 := by
 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. -/
 147theorem defect_cost_unbounded (sensor : DefectSensor)
 148    (hm : sensor.charge ≠ 0) :
 149    ∀ B : ℝ, ∃ N : ℕ, ∀ (mesh : AnnularMesh N),
 150      (∀ n, (mesh.rings n).winding = sensor.charge) →
 151      B < annularCost mesh := by
 152  intro B
 153  let C : ℝ := Real.pi ^ 2 * kappa / 4 * (sensor.charge : ℝ) ^ 2
 154  have hcharge_ne : (sensor.charge : ℝ) ≠ 0 := by
 155    exact_mod_cast hm
 156  have hC_pos : 0 < C := by
 157    unfold C
 158    have hsq : 0 < (sensor.charge : ℝ) ^ 2 := by
 159      exact sq_pos_iff.mpr hcharge_ne
 160    have hpi2 : 0 < Real.pi ^ 2 := by positivity
 161    have h4 : 0 < (4 : ℝ) := by norm_num
 162    have hconst : 0 < Real.pi ^ 2 * kappa / 4 := by
 163      exact div_pos (mul_pos hpi2 kappa_pos) h4
 164    exact mul_pos hconst hsq
 165  obtain ⟨N0, hN0⟩ :=