tailStrainTimeVariation_of_lipschitz
plain-language theorem explainer
If a map S is Lipschitz continuous with respect to another map Omega that admits a short-window time modulus, then S inherits such a modulus. Fluid dynamicists working on tail controls in the RM2U pipeline would cite this to transfer variation bounds across the Biot-Savart pairing. The proof builds the new modulus by scaling the original one by the Lipschitz constant C and verifies nonnegativity, the zero-limit, and the pointwise inequality by direct multiplication and case split on the sign of C.
Claim. Suppose there exists a modulus function ω such that ω is nonnegative for positive arguments, ω(r) tends to 0 as r tends to 0, and ‖Ω(t) − Ω(s)‖ ≤ ω(r) whenever t and s lie in [−r², 0]. If S is Lipschitz continuous with respect to Ω with some constant C ≥ 0, then there exists a modulus function for S satisfying the same three properties.
background
The module isolates the single hard non-parasitism gate for the RM2U to RM2 pipeline: the tail-flux or boundary term at infinity must vanish for the relevant ℓ=2 coefficient, expressed in Lean as TailFluxVanish. The key auxiliary structure is the tail strain time variation hypothesis, which requires an abstract signal S:ℝ→α to admit a short-window modulus ω controlling ‖S(t)−S(s)‖ on intervals [−r²,0]. This theorem supplies the bridge that transfers the hypothesis from one normed space to another when the second signal is Lipschitz in the first, mirroring the TeX step from tail vorticity L2 time modulus to tail strain time variation once the explicit pairing is packaged as a Lipschitz map.
proof idea
The tactic proof begins with classical and rcases to extract the original modulus μ from the hypothesis on Ω together with the Lipschitz constant C. It then refines the target structure by supplying the scaled modulus r ↦ C·μ(r). Nonnegativity follows by multiplication of nonnegative terms. The limit property splits on whether C is positive: when C>0 the original limit is rescaled by division and multiplication; when C≤0 the product is nonpositive and therefore bounded by any positive ε. The inequality property chains the Lipschitz bound with the original modulus bound via monotonicity of multiplication by C.
why it matters
The declaration closes a transfer step inside the non-parasitism file, allowing the abstract absorption-class impossibility (U-4) to propagate from one signal to its Lipschitz image. It therefore supports the larger claim that the tail-flux boundary term vanishes, which is the only genuinely hard hypothesis kept separate so the rest of the RM2U pipeline remains checkable. In the Recognition Science setting this sits downstream of the forcing chain and the recognition composition law, supplying the concrete control needed to eliminate parasitic absorption below the Berry threshold.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.