divFree_of_forall
plain-language theorem explainer
Under uniform bounds on Galerkin trajectories and modewise convergence to a limit Fourier trajectory u, the divergence-free condition on each approximant implies the same condition on u. Researchers formalizing 2D incompressible flow limits or Navier-Stokes regularity would cite this to close the identification of the continuum object. The argument is a direct specialization of the fixed-time continuity lemma for the divergence map.
Claim. Let $H$ be a uniform bound hypothesis on the family of Galerkin trajectories $u_N$. Let $HC$ be the convergence hypothesis supplying a limit trajectory $u$. If the Fourier divergence constraint holds for every zero-extended approximant at all $N$, $t$, and modes $k$, then the limit satisfies the divergence-free trajectory condition: for all $t$ and $k$, the divergence constraint on the coefficient $u(t)_k$ vanishes.
background
The ContinuumLimit2D module packages the passage from finite Galerkin approximations to a continuum Fourier state as explicit hypotheses rather than axioms. UniformBoundsHypothesis encodes a family of Galerkin states $u_N$ together with a uniform norm bound $B$ that holds for all $N$ and all $t ≥ 0$. ConvergenceHypothesis supplies a candidate limit $u : ℝ → FourierState2D$ together with pointwise mode-by-mode convergence of the zero-extended coefficients. The auxiliary definition divConstraint extracts the Fourier-side divergence of a velocity coefficient as the linear combination $k_1 v_0 + k_2 v_1$. IsDivergenceFreeTraj then requires this quantity to be identically zero along the entire trajectory.
proof idea
The proof is a one-line wrapper. It introduces the variables $t$ and $k$, then invokes the upstream lemma divConstraint_eq_zero_of_forall after specializing the universal hypothesis to the fixed $t$ and $k$ via the lambda expression fun N => hDF N t k.
why it matters
This result supplies the time-dependent divergence-free property required by the downstream theorem rs_implies_global_regularity_2d_divFreeCoeffBound in Regularity2D. That theorem assembles uniform bounds, convergence, and the present passage to obtain a global regularity statement for the 2D limit without a separate identification hypothesis. Within the Recognition Science pipeline it completes one concrete step of the continuum-limit construction for 2D fluids, consistent with the overall forcing chain that forces D = 3 and the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.