U4PayRhoControlledByInjectionRateHypothesis
plain-language theorem explainer
U4PayRhoControlledByInjectionRateHypothesis encodes the control of normalized PayRho cylinder payment by a constant multiple of the positive injection rate evaluated at doubled radius plus a vanishing error term. Fluid dynamicists closing RS-aligned Navier-Stokes bounds from band budgets cite this spec-layer statement to isolate the missing analytic step in the PayRho gate. The declaration is a direct structure definition matching the TeX hypothesis with an explicit o(1) modulus.
Claim. Let $P$ be a payment structure with nonnegative payRho. The hypothesis holds if there exist $Cgeq 0$ and error function err such that payRho$(r)leq Ccdot$ injRate$(2r)+$err$(r)$ for all $r>0$, where err is bounded by a nonnegative $e$ with $e(r)to 0$ as $r to 0$.
background
In the RM2U.NonParasitism module non-parasitism is the vanishing of the tail-flux boundary term at infinity for the ell=2 coefficient. Payments is the abstract structure carrying the normalized cylinder integrals payXi(r) and payRho(r), both nonnegative, matching the TeX expressions (1/r^2) double-integral over Q_r of rho^{3/2}|nabla xi|^2 and the rho-gradient term over the annular region 1-2eta<rho<1-eta.
proof idea
This declaration is a structure definition with no proof body. It directly encodes the exists-bound condition on C, err, and the o(1) modulus e as specified in the doc-comment.
why it matters
This definition supplies the PayRho control leg of U4InjectionPaymentPackageHypothesis, which bundles vanishing injection, PayXi control, and PayRho control to close the U-4 upper bound. It fills the spec-layer version of the TeX hypothesis hyp:U4_band_budget_controlled_by_injection_rate. In the Recognition framework it supports the non-parasitism gate required for the Navier-Stokes existence pipeline, linking to the eight-tick octave and D=3 via RS-native units.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.