uniformChargeMesh_excess_zero
plain-language theorem explainer
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.
Claim. For 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.