annularCost
plain-language theorem explainer
Annular cost aggregates the phi-weighted ring costs across N concentric rings sharing a uniform integer winding charge. Researchers on the RS topological cost-covering bridge cite it when deriving divergence bounds for nonzero-charge defects. The definition is realized by direct summation over the mesh rings, which immediately transfers convexity and nonnegativity from the underlying ringCost.
Claim. Let $N$ be a natural number and let $M$ be an annular mesh of $N$ rings with integer charge $m$. The annular cost is defined by $C(M) := {}_{n=0}^{N-1} r_n$, where $r_n$ denotes the ring cost of the $n$-th ring sample in $M$.
background
The Annular J-Cost Framework supplies the phi-weighted cost function phiCost u := cosh((log phi) u) - 1 = J(phi^u) together with annular sampling machinery for the RS topological cost-covering bridge. AnnularMesh is the structure consisting of N concentric rings, each an AnnularRingSample, a shared integer charge, and the uniform-winding axiom that every ring carries the same winding number m. Upstream results include PhiForcingDerived.of supplying the J-cost definition and PrimitiveDistinction.from reducing the seven axioms to four structural conditions plus three definitional facts.
proof idea
The declaration is a direct definition that sums ringCost over the Fin N rings of the mesh. No lemmas or tactics are applied; the body is the summation expression itself.
why it matters
This definition supplies the central quantity for the annular coercivity theorem, which establishes annularCost mesh >= (pi^2 kappa / 4) m^2 sum_{n=1}^N 1/n for m != 0, and for the excess decomposition annularExcess. It feeds the carrier-budget comparison theorems that separate topological floor from excess cost. The object realizes the Jensen coercivity step in the annular layer, linking directly to the phi-ladder and the eight-tick octave in the T0-T8 forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.