uniformChargeMesh_excess_zero
The theorem shows that the uniform charge mesh yields zero annular excess for any mesh size N and charge m. Researchers on the Recognition Science cost-covering proof of the Riemann hypothesis cite it to confirm the zero-excess carrier trace. The proof is a term reduction that unfolds the excess definition and reduces the sum via congruence to a sibling equality on ring samples.
claimFor every natural number $N$ and integer $m$, the annular excess of the uniform charge mesh with $N$ points and charge $m$ equals zero.
background
This result belongs to the CostCoveringBridge module, which supplies the explicit carrier package and conditional theorems for the RS cost-covering architecture after the budget interface is realized. Annular excess is defined as the difference between annular cost and the topological floor; the uniform charge mesh is the explicit construction whose excess vanishes. Upstream lemmas supply the defect functional (equal to J for positive arguments) and cost maps induced by multiplicative recognizers and observer forcing, all calibrated inside the phi-ladder with J-uniqueness from the forcing chain.
proof idea
The term proof unfolds annularExcess, annularCost and annularTopologicalFloor, rewrites the difference to zero, applies Finset.sum_congr, and reduces each summand by the sibling equality uniformRingSample_cost_eq_topologicalFloor.
why it matters in Recognition Science
It feeds defect_topological_floor_unbounded (unbounded floor for nonzero charge), eulerBudgetedCarrier (zero-charge trace with zero excess) and not_costDivergent_of_charge_zero. The lemma supplies the zero-excess witness required by the cost-covering bridge, consistent with T5 J-uniqueness, T7 eight-tick octave and the requirement that defect floors stay covered by finite carrier scale. It closes the zero-charge case in the contradiction argument for zeros with Re(s) > 1/2.
scope and limits
- Does not establish zero excess for non-uniform meshes.
- Does not bound the topological floor for nonzero charge.
- Does not derive the Riemann hypothesis.
- Does not treat complex-valued charges.
formal statement (Lean)
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. -/