AnnularMesh
An annular mesh of N concentric rings packages a family of ring samples each carrying identical integer winding m together with the uniform charge constraint. Researchers on the RS topological cost-covering bridge cite this structure when deriving Jensen coercivity bounds of order m² log N. The declaration is a pure structure definition that assembles the rings, charge, and uniformity predicate with no lemmas or computation.
claimAn annular mesh of $N$ concentric rings consists of a family of samples $r_n$ ($n=0,…,N-1$), where each $r_n$ is an annular ring sample on ring $n+1$ with $8n$ phase increments summing to $-2π m$, an integer charge $m$, and the predicate that every ring has winding number exactly $m$.
background
The module sets up the annular J-cost framework in which phiCost u is defined as cosh((log φ)·u)−1, equivalently J(φ^u). AnnularRingSample(n) is the structure holding 8n real increments whose sum equals −2π times the winding integer. Upstream cost is the J-cost derived from multiplicative recognizers and from recognition events; winding extracts net torsion from eight-tick clock words.
proof idea
The declaration is a structure definition. It introduces the rings field as a dependent function from Fin N into AnnularRingSample, the charge field as an integer, and the uniform_charge field as the predicate that every ring sample carries exactly that charge. No tactics or lemmas are invoked.
why it matters in Recognition Science
AnnularMesh is the central input type for annularCost (the sum of ring costs), annularExcess, and the coercivity theorem annular_coercivity that establishes Θ(m² log N) divergence for nonzero charge. It realizes the annular sampling layer of the Recognition Science framework, supporting the topological cost-covering bridge, Jensen ring bounds, and the trace-based carrier-budget interface. The remaining open question is the concrete construction of an AnnularTrace family for a holomorphic carrier.
scope and limits
- Does not prescribe concrete values for the phase increments beyond the winding sum constraint.
- Does not define or compute the associated J-cost; that occurs in ringCost and annularCost.
- Does not impose positivity or boundedness conditions on the charge.
- Does not address the transition to continuous carriers or the argument principle.
formal statement (Lean)
309structure AnnularMesh (N : ℕ) where
310 rings : (n : Fin N) → AnnularRingSample (n.val + 1)
311 charge : ℤ
312 uniform_charge : ∀ n, (rings n).winding = charge
313
314/-- Total annular cost over N rings. -/
used by (21)
-
annular_coercivity -
annularCost -
annularExcess -
annularExcess_nonneg -
annularTopologicalFloor_le_annularCost -
AnnularTrace -
argument_principle_honest -
argument_principle_trivial -
carrier_cost_eq_excess_of_zero_charge -
defect_cost_unbounded -
defect_topological_floor_unbounded -
uniformChargeMesh -
canonicalDefectSampledFamily_charge -
defectAnnularMesh -
DefectSampledFamily -
argument_principle_sampling -
SampledMesh -
SampledMesh -
annularCost_nonneg -
CostDivergent -
not_costDivergent_of_charge_zero