defect_cost_unbounded
Nonzero charge on a defect sensor forces annular cost of uniform-charge meshes to exceed any real bound B. Researchers deriving the Riemann hypothesis from cost-covering would cite this to contradict a zero of zeta with real part above one half. The proof scales the divergent harmonic series against a positive constant C built from pi squared, kappa and charge squared, then invokes annular coercivity to obtain the strict inequality.
claimLet $S$ be a defect sensor with nonzero integer charge $m$. Then for every real number $B$ there exists a natural number $N$ such that for every annular mesh of size $N$ whose rings all have winding number $m$, the annular cost of the mesh exceeds $B$.
background
The CostCoveringBridge module packages the RS cost-covering architecture that links defect sensors to annular costs after the budget interface is realized. A DefectSensor is a structure recording an integer charge (the multiplicity of a zero of zeta, hence the order of the pole of zeta inverse), a realPart in (1/2,1), and the predicate that the point lies inside the critical strip. AnnularMesh N discretizes the plane into N concentric rings; annularCost sums the contributions of each ring's winding number together with geometric factors involving kappa. The module builds on unconditional annular bounds from AnnularCost, including the coercivity lower bound and the fact that the harmonic series diverges.
proof idea
The proof constructs the positive constant C equal to pi squared times kappa over 4 times charge squared. It invokes the at-top divergence of the harmonic series to obtain N0 such that the partial sum up to N0+1 exceeds B/C plus 1. For the mesh at level N0+1 with uniform winding equal to the sensor charge, it confirms the mesh charge matches and is nonzero, then applies the annular coercivity inequality to replace the scaled harmonic sum by annularCost, yielding B less than annularCost.
why it matters in Recognition Science
This supplies the core unconditional divergence statement that nonzero charge produces unbounded annular cost. It is repackaged as CostDivergent in UnifiedRH and directly feeds defect_topological_floor_unbounded together with the realized-family results in DefectSampledTrace. The lemma closes the contradiction step in the RS cost-covering argument for the Riemann hypothesis: a zero with real part exceeding one half would generate a topological floor that diverges as m squared log N, outrunning any finite carrier budget.
scope and limits
- Does not establish bounded cost when the sensor charge is zero.
- Does not supply explicit divergence rates or numerical constants.
- Applies only to meshes with uniform winding equal to the sensor charge.
- Relies on positivity of kappa and divergence of the harmonic series.
- Does not address existence or location of zeros; assumes the sensor data.
formal statement (Lean)
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
proof body
Tactic-mode proof.
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⟩ :=
166 ((Filter.tendsto_atTop.1 harmonic_sum_diverges) (B / C + 1)).exists_forall_of_atTop
167 refine ⟨N0 + 1, ?_⟩
168 intro mesh hmesh
169 have hsum_gt : B / C < ∑ n : Fin (N0 + 1), (1 : ℝ) / ((n : ℝ) + 1) := by
170 have hge := hN0 (N0 + 1) (Nat.le_succ _)
171 linarith
172 have hscaled : B < C * ∑ n : Fin (N0 + 1), (1 : ℝ) / ((n : ℝ) + 1) := by
173 have hmul := mul_lt_mul_of_pos_left hsum_gt hC_pos
174 have hleft : C * (B / C) = B := by
175 field_simp [hC_pos.ne']
176 calc
177 B = C * (B / C) := hleft.symm
178 _ < C * ∑ n : Fin (N0 + 1), (1 : ℝ) / ((n : ℝ) + 1) := hmul
179 have hcharge_eq : mesh.charge = sensor.charge := by
180 have h0 := hmesh ⟨0, by positivity⟩
181 rw [mesh.uniform_charge ⟨0, by positivity⟩] at h0
182 exact h0
183 have hmesh_nonzero : mesh.charge ≠ 0 := by
184 rw [hcharge_eq]
185 exact hm
186 have hcoerc :
187 C * ∑ n : Fin (N0 + 1), (1 : ℝ) / ((n : ℝ) + 1) ≤ annularCost mesh := by
188 unfold C
189 rw [← hcharge_eq]
190 simpa [mul_assoc, mul_left_comm, mul_comm] using
191 (annular_coercivity (N := N0 + 1) (by positivity) mesh hmesh_nonzero)
192 exact lt_of_lt_of_le hscaled hcoerc
193
194/-- The defect topological floor is unbounded for nonzero charge. -/