TailVorticityL2TimeModulusHypothesis
plain-language theorem explainer
The declaration sets up an abstract hypothesis interface asserting that tail vorticity Ω : ℝ → β obeys a short-window L2 time-modulus condition in any normed additive commutative group β. Navier-Stokes workers on the RM2U closure cite it to control boundary terms at infinity for the ℓ=2 coefficient. It is realized as a direct one-line alias to the strain time-variation hypothesis, keeping the ambient space abstract until L2 instantiation.
Claim. Let β be a normed additive commutative group and Ω : ℝ → β. The hypothesis states that Ω satisfies the tail strain time variation condition, i.e., it possesses a short-window time-modulus on the truncated tail vorticity.
background
The RM2U.NonParasitism module isolates non-parasitism as the single hard gate for the RM2U to RM2 pipeline. Non-parasitism means the tail-flux or boundary term at infinity vanishes for the relevant ℓ=2 coefficient, expressed in Lean as TailFluxVanish. This abbrev supplies the supporting time-modulus hypothesis on tail vorticity while leaving β abstract for later specialization to L2-type tail spaces. Upstream the CPM2D bridge packs models into structures that track discrete defect mass and energy gaps above structured baselines in Galerkin2D settings.
proof idea
This is a one-line wrapper that directly aliases to TailStrainTimeVariationHypothesis β Ω. The attached comment records that the alias mirrors the TeX bridge once the Biot-Savart map is packaged as a Lipschitz operator on the chosen normed space.
why it matters
The interface closes the non-parasitism gate so the remainder of the RM2U pipeline stays checkable. It matches the TeX hypothesis hyp:tail_vorticity_L2_time_modulus and supports vanishing of the ℓ=2 boundary term. It touches the open question of discharging the hypothesis by concrete L2 estimates on the tail vorticity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.