U4BandBudgetControlledByInjectionRateHypothesis
plain-language theorem explainer
The structure encodes the hypothesis that a scale-critical band budget function is bounded above by a fixed multiple of the injection rate evaluated at doubled radius, plus an error term that vanishes as the radius approaches zero from above. A researcher closing the RM2U system for the Navier-Stokes equations would cite it to reduce the PayRho control gate to the positive injection hypothesis. The definition is realized directly as an existential statement over the constant C and the dominating error function satisfying the ε-δ condition.
Claim. Let $bandBudget, injRate : (0,∞) → ℝ$. The hypothesis holds if there exists $C ≥ 0$ and $err : (0,∞) → ℝ$ together with a dominating function $e : (0,∞) → ℝ$ such that $e(r) ≥ 0$ for all $r > 0$, $e(r) → 0$ as $r → 0^+$, $err(r) ≤ e(r)$ for all $r > 0$, and $bandBudget(r) ≤ C · injRate(2r) + err(r)$ for all $r > 0$.
background
In the RM2U.NonParasitism module the single hard gate is isolated as the hypothesis that the tail-flux boundary term at infinity vanishes for the ℓ=2 coefficient. The band budget is the scale-critical term extracted from the band-payment inequality on the payments structure; the injection rate is the normalized positive source term. This hypothesis abstracts the remaining analytic control step that reduces the budget term to the injection rate plus an o(1) error near the origin.
proof idea
This is a structure definition that directly encodes the hypothesis via an existential quantifier over C and the error function. No tactics or lemmas are applied; the declaration serves as a pure interface specification for the downstream bookkeeping argument.
why it matters
The hypothesis supplies the missing control step that feeds the theorem u4PayRhoControlledByInjectionRate_of_bandBudget, which then isolates all PDE content to the two hypotheses in the non-parasitism module. It corresponds to the U-4 band-budget reduction in the manuscript and keeps the remainder of the RM2U-to-RM2 pipeline algebraic. The construction touches the open question of discharging the non-parasitism hypothesis by an explicit tail-flux estimate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.