annularExcess
plain-language theorem explainer
The annularExcess definition subtracts the topological floor from the summed ring costs for a given annular mesh. Researchers on the Recognition Science cost-covering arguments cite this decomposition when establishing non-negativity or bounding carrier excess independent of mesh size. The definition is a direct one-line subtraction of the precomputed floor from the annularCost summation.
Claim. For an annular mesh with $N$ rings and integer charge $m$, the excess cost is defined as the total annular cost minus the topological floor: annularCost(mesh) - annularTopologicalFloor($N$, $m$).
background
The Annular J-Cost Framework defines phiCost(u) as cosh((log φ)·u) − 1, equivalently J(φ^u). An AnnularMesh is a structure of N concentric rings whose windings are uniform and equal to the total charge m. The total annular cost sums the individual ring costs, each derived from the J-cost function on the phase increments. This machinery supports Jensen coercivity: nonzero winding forces Θ(m² log N) cost growth. The excess isolates the variable part above the minimal floor enforced by the charge.
proof idea
This is a one-line wrapper that subtracts annularTopologicalFloor N mesh.charge from the annularCost summation over the rings.
why it matters
This definition supplies the excess term used by annularExcess_nonneg to prove non-negativity and by carrier_budget to bound excess by K · (logDerivBound)² · radius² for zero-charge BudgetedCarrier traces. It completes the decomposition step in the RS topological cost-covering bridge, separating the forced topological floor from the controllable excess for holomorphic carriers. It touches the remaining open construction of a concrete trace family for the analytic carrier with matching excess bound.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.