excess_bounded
Any budgeted carrier satisfies a uniform O(R²) bound on annular excess cost above the topological floor, independent of mesh level N. Analysts of the Recognition Science topological cost-covering bridge cite this result to obtain mesh-independent estimates directly from the carrier data. The proof is a one-line wrapper that invokes the carrier's built-in excess witness.
claimLet $C$ be a budgeted carrier. Then there exists $K$ in the reals such that for every natural number $N$, the annular excess of the $N$-level mesh of $C$'s trace satisfies annularExcess$(C$.trace.mesh$(N)) ≤ K · (logDerivBound$(C))^2 · (radius$(C))^2$.
background
The annular J-cost framework defines phiCost u := cosh((log φ)·u) − 1, which equals J(φ^u). Annular sampling uses phase increments on concentric rings; the excess is annularCost minus the sum of topological floors, and the module states that holomorphic nonvanishing implies O(R²) annular cost. A BudgetedCarrier extends a regular carrier by adjoining an AnnularTrace of zero charge together with an explicit uniform bound on the excess above the topological floor.
proof idea
The proof is a one-line wrapper that applies the excess_bound field of the BudgetedCarrier structure via the carrier_budget lemma.
why it matters in Recognition Science
This theorem supplies the uniform O(R²) excess bound required by the annular layer of the Recognition Science framework. It completes the trace-based carrier-budget interface, allowing the topological cost-covering bridge to proceed with mesh-independent estimates. The module documentation notes that the remaining open task is the construction of a concrete trace family for specific analytic carriers.
scope and limits
- Does not compute an explicit numerical value for the constant K.
- Does not construct or verify a specific AnnularTrace for a given holomorphic function.
- Does not extend the bound to carriers with nonzero charge.
- Does not address divergence for nonzero winding numbers.
formal statement (Lean)
648theorem excess_bounded (carrier : BudgetedCarrier) :
649 ∃ K : ℝ, ∀ N : ℕ,
650 annularExcess (carrier.trace.mesh N) ≤
651 K * carrier.logDerivBound ^ 2 * carrier.radius ^ 2 := by
proof body
Term-mode proof.
652 exact carrier_budget carrier
653
654end NumberTheory
655end IndisputableMonolith