uniformRingSample
plain-language theorem explainer
uniformRingSample constructs an explicit uniform charged ring sample on n+1 rings with winding m by assigning the constant phase increment −2πm/(8(n+1)) to each of the 8(n+1) positions. Number theorists and physicists working on the Recognition Science cost-covering argument for the Riemann hypothesis cite this when assembling uniform charge meshes. The definition is completed by a direct simplification that confirms the winding sum constraint.
Claim. The uniform ring sample with parameters $n ∈ ℕ$ and $m ∈ ℤ$ is the annular ring sample on $n+1$ rings whose $8(n+1)$ increments are each equal to $-2πm/(8(n+1))$, with prescribed winding number $m$.
background
The AnnularRingSample structure consists of a function assigning real phase increments to each of 8n positions on ring n, together with an integer winding number whose constraint requires the sum of increments to equal −2π times the winding. This definition realizes a uniform version of that structure for use in the explicit carrier package of the Cost-Covering Bridge module. The module provides the second layer of the RS cost-covering architecture for the Riemann hypothesis after the unconditional annular bounds in AnnularCost.lean. Upstream results include the winding operation on ribbons that abstracts net torsion on the eight-tick clock.
proof idea
The definition directly populates the three fields of AnnularRingSample. The increments field is set to the constant function returning −(2 * Real.pi * m) / (8 * (n + 1)). The winding field is set to m. The winding_constraint is discharged by a one-line tactic applying simp with Finset.sum_const and nsmul_eq_mul, followed by field_simp.
why it matters
This supplies the building block for uniformChargeMesh, which is used to show that uniform charge meshes have zero annular excess above the topological floor. It realizes the explicit carrier package in the cost-covering bridge, enabling the conditional theorem that the defect topological floor is covered by the carrier scale only for m = 0. This supports the claim that ζ(s) has no zeros with real part exceeding 1/2, consistent with the Recognition Science derivation of D = 3 and the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.