trivial
plain-language theorem explainer
The trivial constructor supplies the base identification hypothesis for the 2D Galerkin-to-continuum pipeline by declaring that the limit trajectory satisfies the solution predicate by fiat. Workers formalizing compactness arguments in fluid dynamics would reference it when building the dependency graph for the Navier-Stokes limit. Its construction is a direct structure instantiation with the constant-true predicate and a trivial proof obligation.
Claim. Let $H$ be a uniform bounds hypothesis on a family of Galerkin trajectories $u_N$ and let $HC$ be a convergence hypothesis asserting pointwise convergence to a limit trajectory $u$. Then the trivial identification hypothesis is the structure consisting of the predicate $IsSolution := (v : ℝ → FourierState2D) → Prop$ set to the constant true together with the assertion that $u$ satisfies this predicate.
background
The module ContinuumLimit2D defines a Lean-checkable pipeline from finite-dimensional 2D Galerkin approximations to a continuum Fourier state. UniformBoundsHypothesis packages a family of trajectories $u_N(t)$ together with a uniform bound $B$ such that $‖u_N(t)‖ ≤ B$ for all $N$ and $t ≥ 0$. ConvergenceHypothesis adds a candidate limit $u(t)$ with modewise convergence of the zero-extended coefficients. IdentificationHypothesis then requires that this limit satisfies a chosen solution concept for 2D Navier-Stokes on the torus, kept abstract here.
proof idea
The definition directly constructs the IdentificationHypothesis record by setting the IsSolution field to the constant true function and discharging the isSolution obligation with the built-in trivial tactic.
why it matters
This supplies the minimal placeholder for the identification step in the continuum limit pipeline, allowing the overall structure to be assembled before concrete PDE verification is supplied. It feeds the later replacement of hypotheses with proofs in subsequent milestones. In the Recognition framework it parallels the use of scaffolding definitions to close dependency chains without circularity, here applied to the classical fluid bridge rather than the core forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.