annularTopologicalFloor_zero
plain-language theorem explainer
Zero winding number forces the annular topological floor to vanish for every mesh size N. Researchers comparing carrier budgets to excess costs or bounding defect traces in Recognition Science cite this identity to simplify zero-charge arguments. The proof is a term-mode reduction that unfolds the sum definition and applies the zero topological floor property termwise.
Claim. For every natural number $N$, the sum of topological floor contributions over an annular mesh of size $N$ equals zero when the total winding (charge) is zero.
background
The annular J-cost framework defines the topological floor as the base cost contribution arising from winding numbers on concentric rings, with the annular version aggregating these contributions over a finite mesh. The zero-charge case supplies the base identity needed to equate total annular cost with excess cost. The module sets up phi-weighted costs via phiCost u = J(phi^u) together with Jensen-based coercivity that forces quadratic growth for nonzero winding.
proof idea
The proof unfolds the annular topological floor definition to reveal a Finset sum. It applies the general lemma that a finite sum vanishes when every summand is zero. Each summand is then reduced to zero by simplification with the topological floor property at zero winding.
why it matters
This identity is invoked directly in the carrier budget comparison to obtain annularCost = annularExcess when charge is zero, and it underpins the equivalence between bounded excess and bounded total cost for zero-charge defect families. It also supports the non-divergence theorem for zero charge and the equivalence of floor coverage to zero charge. The result closes the zero-winding case in the annular cost-covering bridge, consistent with the RS requirement that zero winding incurs no topological cost.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.