pith. machine review for the scientific record. sign in
def definition def or abbrev high

annularExcess

show as:
view Lean formalization →

annularExcess defines the difference between total annular cost and the topological floor for a mesh of N concentric rings. Carrier-budget and charge-zero arguments in the Recognition Science cost-covering bridge cite this decomposition directly. The definition is a one-line subtraction of the precomputed floor from the summed ring costs.

claimFor an annular mesh of $N$ concentric rings with integer winding number $m$, the excess cost equals the total annular cost minus the topological floor value determined by $N$ and $m$.

background

The Annular J-Cost Framework supplies the phi-weighted cost function and annular sampling machinery for the RS topological cost-covering bridge. An AnnularMesh is a structure consisting of $N$ rings together with a single integer charge $m$ such that every ring carries exactly winding number $m$. annularCost sums the individual ring costs; annularTopologicalFloor returns the minimal cost enforced by that charge on the $N$-ring mesh.

proof idea

One-line wrapper that subtracts annularTopologicalFloor N mesh.charge from annularCost mesh.

why it matters in Recognition Science

The definition supplies the excess term required by annularExcess_nonneg, carrier_budget, and excess_bounded. It completes the annular topological floor and excess decomposition listed in the module documentation. The construction supports the transition from Jensen coercivity on rings to mesh-independent budget bounds for zero-charge carriers.

scope and limits

formal statement (Lean)

 468noncomputable def annularExcess {N : ℕ} (mesh : AnnularMesh N) : ℝ :=

proof body

Definition body.

 469  annularCost mesh - annularTopologicalFloor N mesh.charge
 470
 471/-- Annular coercivity: for charge m ≠ 0, total annular cost diverges
 472    as Θ(m² log N). Specifically:
 473    annularCost ≥ (π²κ/4) · m² · ∑_{n=1}^{N} 1/n. -/

used by (19)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (9)

Lean names referenced from this declaration's body.