annularTopologicalFloor_one_pos_of_charge_ne_zero
plain-language theorem explainer
The one-ring annular topological floor is strictly positive for any nonzero integer charge m. Workers on the RS annular J-cost framework cite this to anchor the base case of the excess cost decomposition. The proof is a one-line wrapper that unfolds the annular definition and applies the upstream topological floor positivity lemma at unit radius.
Claim. For nonzero integer charge $m$, the one-ring annular topological floor satisfies $0 <$ annularTopologicalFloor$(1,m)$.
background
The Annular J-Cost Framework equips the Recognition Science cost function with concentric-ring sampling. phiCost u is defined as J(phi^u) = cosh((log phi) u) - 1. AnnularSample records phase increments across rings, and the topological floor extracts the minimal cost forced by winding number m. annularTopologicalFloor(1,m) is the single-ring instance of this floor. The result rests on the upstream lemma topologicalFloor_pos_of_charge_ne_zero, which supplies the same positivity statement for the general topological floor.
proof idea
The proof is a one-line wrapper. It applies simpa to unfold the definition of annularTopologicalFloor and invokes topologicalFloor_pos_of_charge_ne_zero, supplying the radius hypothesis 0 < 1 via norm_num together with the given hm : m ≠ 0.
why it matters
This theorem supplies the base case for the annular topological floor inside the excess bound section of the Annular J-Cost Framework. It supports the decomposition annularCost(F) minus sum of floors equals O(R²) for holomorphic carriers. In the broader Recognition Science setting it reinforces Jensen coercivity for nonzero winding and feeds the carrier-budget interface. No downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.