uniformRingSample_cost_eq_topologicalFloor
plain-language theorem explainer
Uniform ring samples with constant phase increments achieve exactly the minimum J-cost dictated by the topological floor for any integer winding. Analysts constructing explicit carriers in the Recognition Science cost-covering proof of the Riemann hypothesis would invoke this saturation result. The proof is a one-line wrapper that unfolds the definitions of ring cost, topological floor, and the uniform sample, then simplifies the constant sum via Finset.sum_const and nsmul_eq_mul.
Claim. For natural number $n$ and integer $m$, the J-cost of the uniform charged ring sample (identical increments summing to winding $m$) equals the topological floor for charge $m$ on $n+1$ units. With $k = n+1$ and $delta = -2 pi m / (8k)$, this is the equality $8k cdot phi-cost(delta) = 8k cdot phi-cost(delta)$, where the left side is the sum of $8k$ identical phi-cost terms.
background
The Cost-Covering Bridge module packages an explicit carrier for the Riemann hypothesis after unconditional annular bounds are established in AnnularCost. The uniform ring sample sets every angular increment to the same phase step so the total winding equals $m$ exactly. Ring cost is the sum of phi-costs (J-costs) over those increments; the topological floor is the Jensen lower bound $8n cdot phi-cost(-2 pi m / (8n))$, the minimum cost for given charge $m$ on ring parameter $n$ (quoted from its doc-comment as the exact Jensen lower bound written as a named topological floor). Upstream, the uniform distribution from Shannon entropy supplies the equal-increment idea, while the has class from AsteroidOreSpectroscopy is imported but not used here.
proof idea
This is a term-mode proof. It unfolds ringCost, topologicalFloor, and uniformRingSample to expose the sum over identical increments and the explicit delta. The simp tactic then applies Finset.sum_const to replace the sum by cardinality times the common value, together with nsmul_eq_mul to align the scalar multiplication, yielding exact equality with the floor expression.
why it matters
This supplies the saturation property used directly in the downstream theorem uniformChargeMesh_excess_zero, which states that the uniform charge mesh has zero annular excess. In the module architecture it realizes the explicit carrier package: the carrier trace has annular excess O(R^2) independent of mesh refinement, so any zero of zeta with Re(s) > 1/2 would force the defect topological floor to diverge as m^2 log N, exceeding the budget and forcing m=0. It connects to the J-uniqueness (T5) and eight-tick octave (T7) that underlie the annular discretization in the Recognition Science forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.