topologicalFloor_nonneg
plain-language theorem explainer
Nonnegativity of the minimum cost for charge m on ring size n follows from the definition as a scaled phi-cost. Researchers establishing annular lower bounds in Recognition Science cite this to justify summed topological costs. The term-mode proof unfolds the floor expression and applies multiplication nonnegativity together with the known nonnegativity of phiCost.
Claim. For every natural number $n$ and integer $m$, the quantity $8n$ times phi-cost of $-(2$π$m)/(8n)$ is nonnegative, where phi-cost$(u) = $cosh$((log$ φ$)u) - 1$.
background
In the annular J-cost framework the phi-cost function is defined by phiCost$(u) := $cosh$((log$ φ$) · u) − 1$, which equals the J-cost of φ^u. The topological floor for ring size n and charge m is the explicit Jensen lower bound 8n · phiCost$(-(2$π$m)/(8n))$. The module develops phi-weighted costs and annular sampling to support the RS topological cost-covering bridge, including coercivity for nonzero winding and the carrier-budget interface for holomorphic nonvanishing.
proof idea
The proof unfolds the topological floor definition to a product of 8n and phiCost at the scaled argument. It then applies the multiplication nonnegativity lemma, invoking positivity of the natural-number factor together with the upstream result that phiCost is nonnegative at every real argument.
why it matters
This theorem supplies the per-ring nonnegativity step required by the annular topological floor nonnegativity result, which sums floors over rings to obtain a global lower bound. It completes one piece of the annular-layer formalization in the module, supporting the trace-based carrier budget. The step aligns with the phi-ladder and eight-tick octave structure in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.