annularTopologicalFloor_nonneg
plain-language theorem explainer
The annular topological floor, the sum of per-ring topological floors over N concentric rings for integer charge m, is nonnegative. Researchers establishing annular cost bounds and defect excess controls in the Recognition Science J-cost framework cite this result. The proof unfolds the sum definition then invokes Finset.sum_nonneg together with the already-established per-ring topologicalFloor_nonneg.
Claim. For every natural number $N$ and integer $m$, $0 ≤ ∑_{k=1}^N topologicalFloor(k,m)$, where topologicalFloor$(n,m)$ is the base nonnegative cost on the $n$-th ring.
background
The Annular J-Cost Framework defines phiCost $u$ as cosh((log φ)·$u$) − 1, which equals J(φ^u). AnnularTopologicalFloor aggregates the topological floor over N rings as ∑_{n:Fin N} topologicalFloor (n.val + 1) m. The module supplies the RS topological cost-covering bridge, including Jensen coercivity for nonzero winding and holomorphic carrier budgets.
proof idea
Unfold annularTopologicalFloor to the finite sum. Apply Finset.sum_nonneg. For the generic term, invoke topologicalFloor_nonneg (n.val + 1) m, which itself rests on phiCost_nonneg and positivity of the scaling factor.
why it matters
Feeds directly into annularCost_nonneg (which obtains total annular cost nonnegativity by le_trans with this floor) and realizedDefectAnnularExcessBounded_of_costBounded (which converts a uniform cost bound into an excess bound precisely because the floor is nonnegative). Completes the nonnegativity step in the annular layer of the J-cost framework, supporting the carrier-budget interface and excess decomposition.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.