U4VanishingInjectionRateHypothesis
plain-language theorem explainer
The declaration aliases the C2 vanishing injection hypothesis to serve as the U4 rate-strengthened gate on the normalized positive injection rate injPos(r) in the Navier-Stokes non-parasitism module. Fluid dynamicists applying the RM2U pipeline would cite it when bundling injection controls into payment upper bounds. The proof is a direct one-line alias that inherits the exists-alpha domination structure from the C2 hypothesis.
Claim. Let injPos : ℝ → ℝ represent the normalized positive injection rate. The hypothesis asserts that injPos(r) vanishes at small scales: there exists α : ℝ → ℝ with α(r) ≥ 0 for r > 0, α(r) → 0 as r → 0, and injPos(r) ≤ α(r) for all r > 0. In practice injPos(r) is instantiated as (1/r²) ∬_{Q_r} ρ^{3/2} σ₊.
background
The RM2U.NonParasitism module isolates non-parasitism as the single hard hypothesis that the tail-flux boundary term at infinity vanishes for the ℓ=2 coefficient, keeping the RM2U to RM2 pipeline clean and checkable. C2VanishingInjectionHypothesis supplies the scale-modulus for the positive stretching injection: it requires an α ≥ 0 that tends to zero at the origin and dominates injPos on cylinders, mirroring the TeX form hyp:C2_vanishing_injection in scale-invariant shape. Upstream results include the scale function defined by phi^k from cosmology and the is structures from empirical programs and simplicial ledgers that encode collision-free and algebraic-tautology properties.
proof idea
This is a one-line wrapper alias that directly expands to C2VanishingInjectionHypothesis injPos and therefore inherits the exists-α structure with non-negativity, vanishing limit, and pointwise domination.
why it matters
It supplies the injection-rate component of U4InjectionPaymentPackageHypothesis and feeds the payment-upper-bound theorems u4PaymentUpperBound_of_injection and u4PaymentUpperBound_of_u4Package. The alias advances the RS-aligned non-parasitism gate for Navier-Stokes regularity while leaving the concrete PDE discharge as an open question once the ρ and σ objects exist in Lean.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.