topologicalFloor
plain-language theorem explainer
The topological floor supplies the exact Jensen lower bound on the phi-cost incurred by charge m on a ring discretized into 8n phase samples. Workers on the annular cost-covering bridge cite it when separating ring costs into a minimum floor plus explicit excess. The definition is a direct one-line scaling of phiCost at the uniform winding increment by the factor 8n.
Claim. For integer charge $m$ on a ring with $n$ samples the topological floor is $8n$ times the phi-cost of the uniform increment: $8n · (cosh((log φ) · (-2π m / (8n))) - 1)$.
background
In the Annular J-Cost Framework the phi-cost is defined by phiCost u := cosh((log φ)·u) − 1, which equals J(φ^u) via the hyperbolic representation of the J-function. The topological floor is the minimum cost for fixed charge m on a ring with 8n samples, obtained by evaluating phiCost at the uniform winding step. This object lives in NumberTheory.AnnularCost and forms part of the RS topological cost-covering bridge that combines phiCost coercivity with the simplicial Laplacian identification.
proof idea
One-line definition that multiplies the ring-size factor (8 * n : ℝ) by phiCost evaluated at the uniform increment -(2 * Real.pi * m) / (8 * n). No lemmas are invoked inside the body; the expression directly encodes the Jensen lower bound.
why it matters
This definition supplies the exact Jensen lower bound that feeds annularTopologicalFloor, ringCost_ge_topologicalFloor, and the excess decomposition theorems. It fills the minimum-cost slot in the annular sampling machinery for the RS topological cost-covering bridge. The 8n factor reflects the eight-tick octave discretization used throughout the annular layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.