U4InjectionPaymentPackageHypothesis
plain-language theorem explainer
The declaration packages three conditions on a payments structure P and an injection rate function into one hypothesis for the U-4 payment upper bound. A researcher closing the RM2U non-parasitism gate in the Navier-Stokes pipeline would cite it to invoke the combined vanishing and control assumptions at once. It is realized as a structure definition that simply collects the vanishing injection hypothesis with the two payment-control structures.
Claim. Let $P$ be a payments structure whose components are nonnegative functions $payXi, payRho : ℝ → ℝ$. Let $injRate : ℝ → ℝ$. The package hypothesis holds precisely when $injRate$ vanishes at small scales, there exist $C ≥ 0$ and an error function $e$ with $e(r) → 0$ as $r → 0$ such that $payXi(r) ≤ C · injRate(2r) + e(r)$ for all small $r > 0$, and the same bound holds with $payRho$ in place of $payXi$.
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 relevant ℓ=2 coefficient. Payments is the abstract structure carrying the normalized cylinder integrals: $payXi(r)$ records the weighted $L^2$ norm of ∇ξ over the cylinder of radius r, while $payRho(r)$ records the corresponding term for the density gradient inside the transition layer {1-2η < ρ < 1-η}. U4VanishingInjectionRateHypothesis is the alias requiring that the normalized positive injection term tends to zero at small scales; the two control structures each assert the existence of a uniform constant C together with an error term that is nonnegative and tends to zero, so that the respective payment is bounded by C times the rescaled injection rate plus the error.
proof idea
This is a structure definition whose three fields are exactly the three component hypotheses: the vanishing injection rate, the PayXi control structure, and the PayRho control structure. No tactics or lemmas are applied; the declaration serves only as a packaging device that downstream code can pattern-match on a single identifier.
why it matters
It supplies the single bundled input to the theorem u4PaymentUpperBound_of_u4Package, which immediately yields the U4PaymentUpperBoundHypothesis. The construction corresponds to the TeX blocker hyp:U4_injection_payment_package and keeps the remainder of the RM2U → RM2 pipeline free of hidden hypotheses. It therefore isolates the only genuinely hard non-parasitism statement while the rest of the closure remains checkable.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.