annularTopologicalFloor
plain-language theorem explainer
This definition sums the per-ring topological floors to obtain the minimum J-cost for an annular mesh with N rings and fixed integer charge m. Researchers on the RS cost-covering bridge cite it when decomposing total annular cost into floor plus excess for coercivity and budget arguments. The implementation is a direct finite sum over the Fin N index set of the per-ring topologicalFloor values.
Claim. The annular topological floor for $N$ rings and charge $m$ is $∑_{n=1}^N (8n) · ϕCost(−(2π m)/(8n))$, where ϕCost$(u) := cosh((log ϕ) u) − 1$ equals the J-cost of the scaled phase.
background
In the Annular J-Cost Framework the function ϕCost u is defined as cosh((log ϕ) u) − 1, which equals J(ϕ^u) and measures the base cost of phase increments on concentric rings. The upstream topologicalFloor n m is then (8n) times ϕCost of the argument −(2π m)/(8n), supplying the exact Jensen lower bound for the cost on ring n with winding m. annularTopologicalFloor aggregates these floors over the first N rings to give the baseline cost for the full annular configuration with charge m.
proof idea
The definition is a one-line wrapper that sums topologicalFloor (n.val + 1) m over n in Fin N. No lemmas or reductions are applied; the body is the explicit finite sum.
why it matters
It supplies the floor term inside annularExcess and supports the theorems annularTopologicalFloor_nonneg, annularTopologicalFloor_le_annularCost, and annularTopologicalFloor_one_pos_of_charge_ne_zero. These feed the budget transfer theorem carrier_defect_budget_contradiction, which shows that nonzero charge forces the floor above any fixed budget for large N. The declaration completes the annular decomposition layer of the RS topological cost-covering bridge, linking to the phi-ladder and J-uniqueness. The remaining open question is the construction of a concrete trace family for the analytic carrier.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.