C2VanishingInjectionHypothesis
plain-language theorem explainer
The C2 vanishing positive injection hypothesis asserts that a scale-dependent positive injection function injPos(r) is dominated by a nonnegative function α(r) that approaches zero as r approaches zero from above. Researchers formalizing the Recognition Science translation of Navier-Stokes regularity cite this structure as the scale-invariant form of the C2 stretching hypothesis. It is introduced directly as a Prop structure with no computational content or proof obligations.
Claim. A function $injPos : (0,∞) → ℝ$ satisfies the C2 vanishing injection hypothesis if there exists $α : (0,∞) → ℝ$ such that $α(r) ≥ 0$ for all $r > 0$, $α(r) → 0$ as $r → 0^+$, and $injPos(r) ≤ α(r)$ for all $r > 0$.
background
The RM2U.NonParasitism module isolates the single hard non-parasitism statement as a hypothesis, which in the PDE translation is the vanishing of the tail-flux or boundary term at infinity for the ℓ=2 coefficient. The C2VanishingInjectionHypothesis supplies the scale-modulus control on the positive stretching injection injPos r on cylinders, mirroring the TeX Hypothesis hyp:C2_vanishing_injection in scale-invariant form (navier-dec-12-rewrite.tex, Eq. eq:C2-stretch-hyp). Upstream results provide the RS-native units U (τ₀ = 1 tick, ℓ₀ = 1 voxel, c = 1) and foundational one elements from integers and rationals derived from logic.
proof idea
This declaration is a pure definition of a Prop-valued structure; it encodes the existence of the dominating function α with nonnegativity, vanishing limit, and domination properties and carries no proof steps or lemma applications.
why it matters
This hypothesis is the foundational gate for non-parasitism in the RM2U pipeline. It directly defines the alias U4VanishingInjectionRateHypothesis and feeds the theorems c2VanishingInjection_comp_two (scale invariance under doubling) and u4PaymentUpperBound_of_injection (vanishing payments from vanishing injection). It corresponds to the manuscript's C2 stretching hypothesis and supports the Recognition Science derivation of Navier-Stokes regularity via the unified forcing chain and energy identity control.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.