carrierBudgetScale_nonneg
plain-language theorem explainer
Nonnegativity of the carrier budget scale holds for any budgeted carrier equipped with a nonnegative constant and zero-charge trace. Researchers formalizing mesh-independent annular excess bounds in Recognition Science cite this to keep cost estimates nonnegative. The proof is a term-mode one-liner that unfolds the scale and applies multiplication nonnegativity to the budget constant, squared log-derivative bound, and squared radius.
Claim. For any regular carrier with an explicit zero-charge annular trace and nonnegative budget constant $C$, the scale factor $C M^2 R^2$ satisfies $0 ≤ C M^2 R^2$, where $M$ is the logarithmic derivative bound and $R$ the radius.
background
The Annular J-Cost Framework defines phiCost u := cosh((log φ)·u) − 1 = J(φ^u). It equips AnnularSample with phase increments on concentric rings and invokes Jensen coercivity to force Θ(m² log N) cost on nonzero winding. Carrier budget states that holomorphic nonvanishing implies O(R²) annular cost. The module certifies phiCost properties, ring bounds, annular coercivity, and the trace-based carrier-budget interface; what remains conditional is a concrete trace family for the analytic carrier. BudgetedCarrier extends RegularCarrier by adding a zero-charge trace, a nonnegative budgetConstant, and the excess_bound ∀ N, annularExcess (trace.mesh N) ≤ budgetConstant · logDerivBound² · radius².
proof idea
Term-mode proof unfolds carrierBudgetScale then applies mul_nonneg to the product of (mul_nonneg budgetConstant_nonneg (sq_nonneg logDerivBound)) and (sq_nonneg radius).
why it matters
The result supplies the nonnegative scale in the carrier budget theorem that bounds annular excess by C · M² · R² independent of mesh refinement N. It is invoked by the Euler instantiation theorem that equates sampled floor coverage with zero charge. Within the framework it closes the annular topological floor and excess decomposition, consistent with the phi-ladder, J-uniqueness, and eight-tick octave from the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.