uniformChargeMesh
plain-language theorem explainer
uniformChargeMesh N m builds an AnnularMesh of N rings carrying identical winding charge m on every ring by delegating each ring to uniformRingSample. Researchers formalizing the argument principle sampling step in the Riemann hypothesis proof cite this construction to obtain a constant-charge witness for any sensor. The definition is a direct structure instantiation that sets the charge field to m and discharges the uniformity predicate by reflexivity.
Claim. For $N$ a natural number and $m$ an integer, the uniform charge mesh is the annular mesh of $N$ rings whose $n$-th ring is given by the uniform ring sample at level $n$ with winding $m$, whose total charge equals $m$, and whose winding is identical across all rings.
background
AnnularMesh N is the structure consisting of a ring map from Fin N to AnnularRingSample (n.val + 1), a charge field in Z, and a uniformity predicate requiring that every ring's winding equals the total charge. This sits inside the Cost-Covering Bridge module, whose architecture separates unconditional annular bounds (from AnnularCost.lean) from explicit carrier witnesses and the conditional RH theorem. Upstream, the carrier definitions in CorticalNeuromodulationDevice and PhantomCoupledGWAntennaSensitivity fix the frequency scale at 5 phi Hz, while IntegrationGap.A and Masses.Anchor.A record the active edge count per tick as 1; Modal.Actualization.A supplies the actualization operator that selects minimal J-cost configurations.
proof idea
The definition is a direct structure extension: the rings field is defined by lambda n, uniformRingSample n.val m; the charge field is set to m; the uniform_charge field is discharged by the tactic intro n; rfl, which reduces the winding equality to reflexivity.
why it matters
This supplies the uniform-charge mesh required by argument_principle_trivial, which shows that Axiom 1 of the RH formalization holds definitionally rather than as a second axiom. It is invoked in defect_topological_floor_unbounded to witness the divergence of the topological floor for nonzero charge, and in not_costDivergent_of_charge_zero to establish that zero charge yields bounded excess. The construction therefore closes the sampling side of the argument principle inside the cost-covering argument that forces m = 0 and hence no zeros of zeta with real part exceeding 1/2.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.