U4PaymentsControlledByInjectionRateHypothesis
plain-language theorem explainer
U4PaymentsControlledByInjectionRateHypothesis encodes that normalized cylinder payments payXi(r) and payRho(r) satisfy payXi(r) + payRho(r) ≤ C · injRate(r) + err(r) for r > 0, where err is dominated by a modulus e(r) that tends to zero as r → 0+. A PDE analyst closing the RM2U non-parasitism gate would cite this interface to convert a vanishing injection rate into the U4 payment upper bound. The declaration is a pure structure definition with no proof body.
Claim. Let $P$ be a payments structure with nonnegative components $pay_ξ(r)$ and $pay_ρ(r)$. The hypothesis asserts that there exist $C ≥ 0$ and an error function $err$ such that $pay_ξ(r) + pay_ρ(r) ≤ C · injRate(r) + err(r)$ for all $r > 0$, where $err(r) ≤ e(r)$ for a modulus $e$ satisfying $0 ≤ e(r)$ and, for every $ε > 0$, there exists $r_0 > 0$ such that $e(r) ≤ ε$ whenever $0 < r ≤ r_0$.
background
Payments is an abstract structure holding the normalized cylinder integrals payXi(r) and payRho(r), which in the underlying PDE represent averaged energy densities involving gradients of the velocity and density fields over cylinders of radius r. The module RM2U.NonParasitism isolates the non-parasitism condition as the single hard hypothesis that the tail flux vanishes at infinity for the ell=2 mode. Upstream, the normalized function from RunningMaxNormalization ensures quantities are scaled to unit bound, while RS-native units fix c=1 and other constants to 1.
proof idea
As a structure definition this declaration has no proof body and directly encodes the existential statement on the bound and error modulus.
why it matters
This hypothesis is the input to the theorem u4PaymentUpperBound_of_paymentControl, which concludes the U4PaymentUpperBoundHypothesis when combined with a vanishing injection rate. It fills the spec layer for the U-4 control in the Navier-Stokes RM2U non-parasitism gate, allowing the pipeline to proceed from injection vanishing to payment decay without deriving the bound from the PDE. In the Recognition Science framework it supports the transition from T8 dimensional constraints to the analytic closure needed for the mass ladder and alpha band consistency.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.