ringCost_ge_topologicalFloor
plain-language theorem explainer
The ring cost of an annular sample with positive winding is bounded below by the topological floor induced by its total winding number. Researchers decomposing annular costs into minimal topological and excess parts cite this result in the Recognition Science cost-covering bridge. The proof is a one-line wrapper that unfolds the floor definition and applies the Jensen ring bound directly to the sample.
Claim. Let $s$ be an annular ring sample on $n$ rings with winding number $w$. Then the topological floor satisfies topologicalFloor$(n,w) ≤$ ringCost$(s)$, where ringCost$(s)$ sums the φ-costs over the $8n$ phase increments obeying the winding constraint.
background
The Annular J-Cost Framework sets phiCost $u$ := cosh((log φ)·$u$) − 1 = J(φ^u). An AnnularRingSample $n$ is a structure holding $8n$ real increments whose sum equals −(2π $w$) for integer winding $w$. ringCost is defined as the sum of phiCost over those increments. The module establishes Jensen-based coercivity: nonzero winding forces Θ($m^2$ log $N$) cost, with this theorem supplying the exact lower bound named as the topological floor.
proof idea
The proof is a one-line wrapper. It unfolds topologicalFloor and invokes jensen_ring_bound on the hypotheses 0 < $n$ and the sample $s$, with simpa discharging the resulting equality.
why it matters
This supplies the named topological floor used by annularTopologicalFloor_le_annularCost to bound total annular cost from below. It completes the annular topological floor and excess decomposition step in the module, linking to the J-uniqueness and phi-ladder landmarks of the forcing chain. The module doc states that the annular layer is now constructively formalized, with this result advancing the trace-based carrier-budget interface.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.