c2VanishingInjection_comp_two
plain-language theorem explainer
If a positive injection function injPos satisfies the C2 vanishing hypothesis then the rescaled map r maps to injPos(2r) satisfies the identical hypothesis. Analysts deriving scale-invariant bounds for Navier-Stokes regularity cite this when shifting estimates between cylinders of radius r and 2r. The proof extracts the original modulus alpha, defines the new witness as alpha composed with doubling, and verifies the three defining properties by elementary rescaling and nlinarith.
Claim. Let $injPos : (0,∞) → ℝ$. Suppose there exists a modulus $α : (0,∞) → ℝ$ such that $α(r) ≥ 0$ for all $r > 0$, $α(r) → 0$ as $r → 0^+$, and $injPos(r) ≤ α(r)$ for all $r > 0$. Then the rescaled function $r ↦ injPos(2r)$ admits a modulus $α'(r) := α(2r)$ satisfying the same three properties.
background
The C2VanishingInjectionHypothesis is a structure that packages a scale-invariant positive injection injPos together with a dominating modulus alpha that is nonnegative, vanishes at the origin, and bounds injPos from above. This mirrors the TeX hypothesis on vanishing stretching injection in its scale-invariant form. The surrounding module isolates the single hard non-parasitism gate for the RM2U pipeline, where non-parasitism is expressed as vanishing tail flux at infinity for the ell=2 coefficient. Upstream results supply only generic algebraic and empirical-program scaffolding; the local content is carried by the hypothesis structure itself.
proof idea
The tactic proof opens with classical, extracts the witness alpha via rcases on the exists_alpha field, and refines a new hypothesis record whose alpha is the original composed with doubling. Non-negativity at r is obtained by applying the original at 2r together with nlinarith to confirm 2r > 0. The vanishing limit rescales the original r0 by division by 2 and reuses the bound after nlinarith adjustment. The domination inequality is transferred verbatim by simpa after the same positivity check.
why it matters
The lemma supplies the only scale-doubling bookkeeping required to align with the TeX convention of working on Q_{2r} cylinders inside the non-parasitism estimates. It is invoked directly by the downstream theorem u4PaymentUpperBound_of_u4Package, which converts a vanishing positive injection into an upper bound on the U4 payment term. Within the Recognition Science framework this closes the scale-consistency step that lets the injection control the boundary term for the ell=2 coefficient without introducing new hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.