annular_coercivity
plain-language theorem explainer
Annular coercivity supplies a lower bound on total annular cost that grows as charge squared times the partial harmonic sum. Researchers building cost-covering contradictions in Recognition Science cite it to show that nonzero winding forces cost to diverge with mesh refinement. The proof applies the per-ring coercivity bound to each component of the mesh and sums the resulting inequalities via the definition of annularCost.
Claim. Let $N$ be a positive integer and let $M$ be an annular mesh of $N$ concentric rings carrying nonzero integer charge $m$. Then $ (π² κ / 4) m² ∑_{k=1}^N 1/k ≤ $ total annular cost of $M$, where $κ$ is the conductivity parameter taken from the φ-ladder.
background
In the annular J-cost framework an AnnularMesh of $N$ rings is a structure whose rings field assigns to each index an AnnularRingSample whose winding number equals the mesh charge $m$ for every ring. annularCost is the sum of the individual ring costs, each obtained from the phiCost function (equal to $J(φ^u)$) via the multiplicative-recognizer cost construction. kappa is defined as $φ^k$ for a suitable rung $k$ drawn from the phi-ladder in the Materials module.
proof idea
The tactic proof first establishes a pointwise lower bound for each ring by calling ring_coercivity after rewriting the uniform_charge hypothesis into the ring. It then rewrites the target left-hand side as a Finset sum using mul_sum, applies sum_le_sum to replace each term by the corresponding ringCost, and finishes by reflexivity on the definition of annularCost.
why it matters
The bound is the direct input to defect_cost_unbounded, which uses divergence of the harmonic sum to obtain a contradiction from any nonzero-charge defect. It completes the Jensen coercivity step inside the annular layer of the Recognition Science cost-covering bridge, linking the magnitude-of-mismatch forces structure and the observer-forcing cost definition to the topological floor.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.