Quasi2DToComparisonSolutionHypothesis
plain-language theorem explainer
The E-gate bridge hypothesis asserts that a quasi-2D event on a bounded mild solution with bounded vorticity yields a comparison solution in an eliminable subclass that matches the original data at any fixed time T. Analysts of Navier-Stokes regularity via symmetry methods would cite this structure when closing uniqueness arguments. It is introduced as a bare structure definition that packages the required existential statement for direct pairing with backward-uniqueness hypotheses.
Claim. Let $Sol$ be a type of solutions. Let $IsBoundedMild, HasBoundedVorticity, Quasi2DEvent, EliminableSubclass : Sol → Prop$ and $AgreeAtTime : Sol → Sol → ℝ → Prop$. The hypothesis states: for every $u ∈ Sol$ and $T ∈ ℝ$, if $IsBoundedMild(u)$, $HasBoundedVorticity(u)$ and $Quasi2DEvent(u)$ hold, then there exists $u_2 ∈ Sol$ such that $IsBoundedMild(u_2)$, $HasBoundedVorticity(u_2)$, $EliminableSubclass(u_2)$ and $AgreeAtTime(u_2, u, T)$ all hold.
background
The module isolates the single hard non-parasitism gate for the RM2U → RM2 pipeline. Non-parasitism is translated as the vanishing of the tail-flux (boundary term at infinity) for the relevant ℓ=2 coefficient. The local setting keeps solution objects abstract as a type $Sol$ and encodes only logical shape, so that the rest of the pipeline remains checkable once this gate is discharged. The referenced sibling BackwardUniquenessNSHypothesis encodes that, within the bounded-mild plus bounded-vorticity class, any two solutions agreeing at time T coincide everywhere.
proof idea
This declaration is a structure definition whose single field directly encodes the required existential statement. No lemmas are applied; the structure simply packages the universal quantifier over solutions and times together with the three antecedent predicates and the four consequent predicates.
why it matters
The structure supplies the symmetry-propagation step needed to feed the backward-uniqueness gate and thereby close the non-parasitism hypothesis in the RM2U module. It is explicitly designed to pair with BackwardUniquenessNSHypothesis so that a quasi-2D event produces a comparison mild solution whose final data can be used for uniqueness. In the Recognition Science setting this isolates the only genuinely hard statement, keeping the remainder of the Navier-Stokes translation clean.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.