topologicalFloor_zero
plain-language theorem explainer
Zero winding number yields identically zero topological floor on every ring in the annular J-cost model. Researchers deriving coercivity bounds or excess decompositions in Recognition Science annular sampling would invoke this to clear the m=0 case before applying Jensen lower bounds. The proof is a one-line wrapper that unfolds the topologicalFloor definition and simplifies directly via the phiCost zero property.
Claim. For every natural number $n$, the topological floor of zero winding on ring $n$ vanishes: topologicalFloor$(n,0)=0$, where topologicalFloor$(n,m)=8n·phiCost(-2πm/(8n))$ and phiCost$(u)=cosh((log φ)·u)-1$.
background
The Annular J-Cost Framework defines phiCost u as cosh((log φ)·u)−1, equivalently J(φ^u), the Recognition Science cost function on phase increments. AnnularSample machinery samples phase increments on concentric rings, with the topological floor supplying the exact Jensen lower bound on minimum cost for integer charge m on ring n. The definition topologicalFloor(n,m) := (8n)·phiCost(−2πm/(8n)) encodes the scaled cost of the minimal winding configuration on that ring. Upstream, phiCost_zero establishes phiCost(0)=0 by direct simplification with Real.cosh_zero, providing the algebraic base case for all zero-winding statements.
proof idea
One-line wrapper that unfolds the topologicalFloor definition and applies simp with the phiCost_zero lemma, reducing the expression 8n·phiCost(0) immediately to zero.
why it matters
This result closes the zero-winding case inside the annular topological floor and excess decomposition layer of the RS cost-covering bridge. It is invoked directly by the downstream annularTopologicalFloor_zero theorem, which extends the vanishing statement to the full mesh sum over rings. The step aligns with the module's certification of Jensen ring bounds and harmonic divergence, supporting the carrier-budget interface where holomorphic nonvanishing implies O(R²) annular cost.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.