U4PayXiControlledByInjectionRateHypothesis
plain-language theorem explainer
This structure encodes the hypothesis that the normalized PayXi cylinder payment is bounded above by a constant times the positive injection rate evaluated at doubled radius, plus a vanishing error term. Researchers assembling the RM2U closure for the Navier-Stokes equations cite it when packaging the U-4 controls. The definition is a direct structural encoding of the existential bound together with the o(1) modulus condition on the error.
Claim. Let $P$ be a payment structure whose payXi function is non-negative. Let injRate be a real-valued function on the positive reals. The hypothesis asserts that there exist a constant $Cgeq 0$ and an error function err such that there is an auxiliary non-negative function $e$ with $e(r)to 0$ as $r to 0^+$, err$(r)leq e(r)$ for all $r>0$, and payXi$(r)leq Ccdot$ injRate$(2r)+$err$(r)$ for all $r>0$.
background
The RM2U.NonParasitism module isolates the single hard non-parasitism statement as a hypothesis so that the remainder of the RM2U to RM2 pipeline stays checkable. Non-parasitism is the vanishing of the tail-flux boundary term at infinity for the relevant ell=2 coefficient. The Payments structure abstracts the normalized cylinder payments: payXi$(r)$ corresponds to the integral expression $(1/r^2) iint_{Q_r} rho^{3/2} |nabla xi|^2$, kept at the spec layer as an uninterpreted non-negative function from the reals to the reals.
proof idea
This is a definition rather than a theorem. It directly encodes the required bound by existentially quantifying over the constant $C$ and the error function err, then imposing the smallness condition on err via an auxiliary function $e$ that is non-negative and tends to zero at the origin.
why it matters
The declaration supplies the PayXi-control component of the downstream U4InjectionPaymentPackageHypothesis, which bundles vanishing injection rate with controls on both PayXi and PayRho. It fills the spec-layer version of the TeX blocker hyp:U4_injection_payment_package once injRate is instantiated by the normalized positive injection. In the Recognition framework it supports the non-parasitism gate required for the Navier-Stokes closure, ensuring boundary terms vanish without parasitic contributions; it touches the open question of discharging the hypothesis via explicit tail-flux vanishing.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.