annularExcess_nonneg
plain-language theorem explainer
The excess cost above the topological floor for any annular mesh is nonnegative. Researchers formalizing the annular J-cost decomposition cite this to close the sign property before coercivity estimates. The proof is a one-line wrapper that unfolds the excess definition and applies linear arithmetic to the floor-cost inequality.
Claim. For every natural number $N$ and every annular mesh of $N$ rings, the excess cost above the topological floor is nonnegative.
background
The module sets up the annular J-cost framework for the RS topological cost-covering bridge. An annular mesh of $N$ rings carries a uniform integer charge across concentric ring samples, with total annular cost defined as the sum of individual ring costs. The excess is the difference between this total cost and the topological floor for the given charge.
proof idea
Unfolds the excess definition then applies linarith directly to the upstream inequality that the topological floor is at most the total annular cost.
why it matters
This result secures the nonnegativity of the excess term in the annular cost decomposition, a prerequisite for separating floor and excess contributions in Jensen-based coercivity arguments. It belongs to the sequence of annular properties that include the topological floor bound and ring-level inequalities, supporting the overall cost-covering bridge in the Recognition Science framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.