TailStrainTimeVariationHypothesis
plain-language theorem explainer
The time-variation modulus hypothesis for the tail strain signal asserts existence of a modulus function that bounds the variation of an abstract map S over backward time intervals of length r squared. Fluid analysts deriving tail estimates inside the RM2U non-parasitism closure cite this structure as the abstract carrier for the tail-strain time-variation condition. The declaration is a pure structure definition carrying no proof obligations.
Claim. Let $S:ℝ→α$ map into a normed additive commutative group $α$. The hypothesis asserts existence of $ω:ℝ→ℝ$ such that $ω(r)≥0$ for $r>0$, $ω(r)→0$ as $r→0^+$, and $‖S(t)−S(s)‖≤ω(r)$ whenever $r>0$ and $t,s∈[−r²,0]$.
background
In the RM2U.NonParasitism module the non-parasitism condition is isolated as the single hard gate: the tail-flux boundary term at infinity vanishes for the relevant ℓ=2 coefficient. The present structure supplies the short-time continuity control required for the tail strain signal at the origin. Upstream, the CPM2D Hypothesis bundle packages the Galerkin-state projection-defect and energy controls that underwrite the fluid closure.
proof idea
The declaration is a pure structure definition that packages three properties (non-negativity, vanishing at zero, and the uniform bound on short intervals) into a single Prop. No lemmas are invoked and no tactics appear.
why it matters
This structure supplies the abstract carrier for the tail-strain time-variation hypothesis and is invoked by the bridge theorem tailStrainTimeVariation_of_lipschitz that transfers the modulus from the vorticity field under a Lipschitz assumption. It supports the clean separation of the RM2U to RM2 pipeline by keeping the non-parasitism gate as a single interface. The definition mirrors the corresponding TeX hypothesis and leaves the concrete Biot-Savart instantiation open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.