u4PaymentUpperBound_of_paymentControl
plain-language theorem explainer
The theorem shows that if normalized cylinder payments are majorized by a vanishing injection rate plus a vanishing error, then the payments themselves admit a vanishing upper bound at small scales. Analysts closing the non-parasitism gate in the RM2U Navier-Stokes pipeline would cite it to convert a control interface into the required payment decay. The argument is a one-line wrapper that destructures the control hypothesis and feeds the extracted constants into the rate-vanishing lemma.
Claim. Let $P$ be a payments structure with non-negative functions payXi and payRho. Let injRate satisfy the vanishing injection hypothesis. If there exist $C ≥ 0$ and an error function err such that payXi(r) + payRho(r) ≤ C · injRate(r) + err(r) for all sufficiently small r > 0 with err(r) → 0 as r → 0, then there exists a function β(r) → 0 such that payXi(r) + payRho(r) ≤ β(r) for all sufficiently small r > 0.
background
Payments is an abstract structure of two non-negative real-valued functions on positive reals that represent normalized gradient integrals over cylinders Q_r. U4VanishingInjectionRateHypothesis is the C2-style condition that the positive injection injRate vanishes at small scales. U4PaymentsControlledByInjectionRateHypothesis supplies the interface asserting that the sum of the two payment functions is bounded by C times injRate plus an error that tends to zero at small scales. U4PaymentUpperBoundHypothesis is the target statement that the same sum is bounded by a function that itself tends to zero at small scales. The module RM2U.NonParasitism isolates the tail-flux vanishing condition at infinity for the ℓ=2 coefficient as the single hard hypothesis needed to keep the RM2U to RM2 pipeline checkable.
proof idea
The proof runs in classical mode. It destructures the exists_bound field of the control hypothesis to obtain the constant C, the error function err, and the bounding inequality. It then applies the lemma u4PaymentUpperBound_of_u4InjectionRate to the payments structure, the injection rate, the vanishing hypothesis, the error data, and the extracted bound triple.
why it matters
The result supplies one direction of the bookkeeping that converts a rate-control interface into the payment upper bound required for tail-flux vanishing. It therefore supports the module's design goal of isolating the single hard non-parasitism statement while keeping the remainder of the RM2U closure purely algebraic. The declaration sits downstream of the Payments structure and the two rate hypotheses but has no recorded users yet; it does not engage the Recognition Science forcing chain or the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.