IdentificationHypothesis
plain-language theorem explainer
IdentificationHypothesis packages an abstract predicate IsSolution on trajectories together with the assertion that the converged Fourier trajectory u from ConvergenceHypothesis satisfies it. Researchers formalizing 2D Navier-Stokes limits cite it to close the identification step after uniform bounds and modewise convergence are in hand. The declaration is a pure structure definition whose only content is the two fields.
Claim. Let $H$ be a UniformBoundsHypothesis and $HC$ a ConvergenceHypothesis over $H$ with limit trajectory $u$. An IdentificationHypothesis consists of a predicate $IsSolution : (ℝ → FourierState2D) → Prop$ such that $IsSolution(u)$ holds.
background
The ContinuumLimit2D module formalizes a Lean-checkable pipeline from finite-dimensional 2D Galerkin approximations to a continuum limit object. FourierState2D is the type of all Fourier coefficient maps Mode2 → VelCoeff. UniformBoundsHypothesis supplies a family of Galerkin trajectories uN together with a uniform bound B such that ‖uN N t‖ ≤ B for all N and t ≥ 0. ConvergenceHypothesis then asserts pointwise modewise convergence of the zero-extended Galerkin coefficients to those of a candidate limit trajectory u.
proof idea
Structure definition. The two fields simply introduce the abstract predicate IsSolution and the assertion isSolution : IsSolution HC.u. A trivial constructor (commented in the file) sets IsSolution := True.
why it matters
The structure supplies the interface for the identification step in milestone M5 of the classical bridge. It is invoked by coeffBound to produce a concrete identification via uniform coefficient bounds, by divFreeCoeffBound to add the divergence-free condition, and by continuum_limit_exists to assert existence of the limit under the identification. It keeps the PDE solution concept abstract so that later milestones can replace the hypothesis with a theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.