Reading Points and Galerkin Limits

A — Abstract

We study the specification structure of the Galerkin construction formalized by Wang for global Leray–Hopf weak solutions of the two-dimensional Navier–Stokes equations. The construction begins with Galerkin systems, where transport cancellation yields an exact energy identity, and proceeds through uniform estimates, space–time compactness, and convergence to a weakly continuous velocity path satisfying the energy inequality at every time. We call each specified time \(t\) a reading point: a point where the established weakly continuous representative and its admissible energy bound can be read directly, while the approximating sequence remains part of the construction that establishes them. The passage from exact Galerkin identities to an inherited limiting inequality provides a concrete example of specification leading construction. We formulate this ordering as a specification grammar: leading constraints organize engineering objects and measurable states; leading specifications constrain admissible generalizations; and admissible generalizations trail leading specifications.

B — Introduction: A Reading Point and Its Construction

Consider the normalized, unforced incompressible Navier–Stokes system on a bounded open domain \(\Omega\subset\mathbb R^2\),

Wang formalizes in Lean 4 the Galerkin construction of a global Leray–Hopf weak solution for every initial datum in the corresponding solenoidal \(L^2\) velocity space. The resulting solution has a weakly continuous representative

satisfies the weak equation on every specified horizon, and obeys the energy inequality at every time.

For every integer \(N\geq0\) and \(t\in[0,N]\),

We call the specified \(t\) a reading point. Once the representative \(u_c\) has been established, its velocity value and admissible energy bound can be read directly at \(t\). The Galerkin approximations remain part of the construction establishing that reading.

At each Galerkin level, the corresponding energy relation is exact. For the interval \(I=[a,b]\), where \(a\) is the initial time, the schematic form is

At the limiting reading point,

Weak lower semicontinuity carries the exact approximating balance into the admissible limiting bound.

In proof order, the construction produces the objects satisfying that specification. Our contribution is an interpretation of this ordering in Wang’s kernel-checked construction.

C — Leading Specification: The Weak Solution

Choose an auxiliary rectangle \(Q\) satisfying

Let \(D_\sigma(\Omega)\) denote the compactly supported \(C^1\) divergence-free fields in \(\Omega\), extended by zero to \(Q\). Wang defines \(H_\Omega\) as their closure in \(L^2(Q;\mathbb R^2)\) and \(V_\Omega\) as the closure of their velocity–gradient graphs. The coordinate maps are

For every \(u_0\in H_\Omega\), Wang constructs \(u_c\) as in (2) and, for every integer \(N\geq0\),

with

For every \(y\in H_\Omega\),

is continuous.

For \(t\in[0,N]\), define

and

For every \(\varphi\in V_\Omega\) and scalar time test \(\eta\in C^1([0,N])\) satisfying \(\eta(N)=0\),

In our terminology, the initial value, weak continuity, almost-everywhere compatibility, weak equation, and every-time energy inequality form the leading specification. They state what an admissible construction must establish.

D — Galerkin Construction

The Galerkin construction on a specified interval is carried out on

using the rectangular spaces \(V_Q\) and \(H_Q\). The compact, injective, dense embedding

provides spectral coordinates through the compact positive operator

There are orthonormal bases \((e_i)\) of \(V_Q\) and \((f_i)\) of \(H_Q\), together with singular values \(\sigma_i>0\), satisfying

Nested mode sets \(K_m\) define

The associated orthogonal projections satisfy

and

Wang constructs exact lifts

and test projections \(Q_m:V_Q\to H_m\). To keep the rectangle \(Q\) distinct from the projection notation below, write \(\Pi_m:=Q_m\), with

These spectral objects connect the \(H_Q\)-coordinates used by the coefficient ODE with the \(V_Q\)-coordinates carrying gradient control.

The convection form satisfies the skew identity

hence

Write \(A_Q(v,w):=\langle G_Qv,G_Qw\rangle_{L^2(Q)}\) for the diffusion form. Riesz representation converts diffusion, convection, and forcing on each \(H_m\) into a coefficient ODE. We write its vector field as \(\mathcal V\), keeping \(R_t\) below for time restriction:

Wang’s Galerkin ODE theorem gives the exact energy identity

For the unforced construction \(F=0\),

Skew cancellation therefore yields both an exact balance and the uniform control required to continue the coefficient solution across the full interval. The Ladyzhenskaya estimate additionally supplies the uniform dual-space derivative control used in compactness.

E — Compactness and the Reading Point

The uniform bounds prepare the passage to the limit. Each fixed-mode projection has a uniform \(1/2\)-Hölder modulus in time. Arzelà–Ascoli on each Galerkin space \(H_m\) therefore supplies uniform convergence along a subsequence, while the operator-norm spectral-tail estimate controls the high-mode remainder.

The resulting spectral compactness argument yields

and, along a common refinement of the extracted subsequences,

with

The gradient coordinate also converges weakly:

in

Wang then uses uniform convergence of every fixed-mode projection to construct

such that, for every \(t\in I\),

For every \(y\in H_Q\),

is continuous, while

and

The initial Galerkin values are orthogonal projections of \(u_0\), and

Thus the Bochner limit supplies the almost-everywhere class, and the fixed-mode construction lifts that class to a weakly continuous representative specified at every \(t\).

supplies the reading points.

The Ladyzhenskaya map \(R_Q:V_Q\to L^4(Q;\mathbb R^2)\) and the interpolation bound

applied to \(w=u_{V,k}-u_V\) upgrade the strong \(L^2(I;H_Q)\) convergence to strong \(L^2(I;L^4(Q))\) convergence, which passes the convection term. The common refined subsequence therefore supports the nonlinear limit, the weakly continuous representative, and the energy argument.

F — Exact Identity to Limit Inequality

Fix a reading point

Let \(R_t\) denote restriction of a time-dependent gradient to \([a,t]\). Define

in the Hilbert direct sum

Its squared norm is

Let \(U_m:I\to H_m\) denote the coefficient solution. Along the selected indices \(m_k\), set

The initial coefficient data and diffusion form satisfy

These identities connect the coefficient ODE directly to the velocity–gradient pair used in the limiting energy argument.

For the unforced system, the exact Galerkin identity gives

Orthogonal projection gives

Meanwhile,

where

The first coordinate converges by the pointwise weak construction of \(u_c\). The second follows from weak gradient convergence and boundedness of \(R_t\). Weak lower semicontinuity gives

Using the projection bound (51), we obtain

The choice of \(t\) was arbitrary, so (55) holds at every time.

The equality records the exact Galerkin balance. The inequality is Wang’s inherited energy inequality: the admissible property carried to the limiting reading point. Classical two-dimensional regularity theory can strengthen the energy relation further; that strengthening lies outside Wang’s formalized statement and outside the specification used here.

For \(\Omega\), zero extension makes \(V_\Omega\) and \(H_\Omega\) closed subspaces of \(V_Q\) and \(H_Q\). Restricting \(J_Q\) gives a compact, injective, dense map \(J_\Omega:V_\Omega\to H_\Omega\). The Ladyzhenskaya bound and skew cancellation transfer through the zero extensions. The spectral construction is then applied to \(J_\Omega\), producing \(\Omega\)-adapted Galerkin spaces, lifts, and projections.

For each integer horizon \([0,N]\), Galerkin ODE uniqueness makes the Galerkin paths consistent under restriction. A diagonal extraction over the integer horizons produces one subsequence converging strongly on every horizon; weak compactness refines it in the energy spaces, and a further diagonal extraction makes every fixed spectral projection converge uniformly on every \([0,N]\). Self-adjointness of the projections and \(P_jy\to y\) identify the weakly continuous representatives pointwise on overlaps. One global path follows:

Its restriction to every \([0,N]\) carries the weak equation and every-time energy inequality.

G — Specification Grammar

The Galerkin argument now displays two compatible orders.

The construction order records how the result is established:

The specification order records what an admissible construction must establish:

Here \(\mathcal S\) contains the initial value, weak continuity, compatibility of the velocity and energy representatives, weak equation, and every-time energy inequality.

A specification is leading where it constrains what counts as an admissible construction or generalization. “Leading” therefore specifies an ordering of constraints rather than a chronology of proof steps.

The construction introduces engineering objects including

These objects mediate between the leading constraints and the limiting quantities established by the proof.

At a reading point, the relevant measurable state is

with

If \(\mathcal C'\) denotes a proposed generalization, its admissibility relative to the specification \(\mathcal S\) can be written schematically as

The criterion concerns preservation of specification. Alternative Galerkin or approximation constructions can qualify where they establish the specified properties.

Wang’s forced rectangle theorem supplies a concrete generalized specification. For admissible forcing \(F\), the every-time energy requirement becomes

The spectral machinery is retained while the construction gains forcing-work control and the Poincaré absorption used for continuation. Thus a generalized \(\mathcal S_F\) constrains the additional engineering step required for its admissible construction.

The first line specifies admissibility. The second establishes it.

H — Discussion: Specification Leads Construction

Wang’s formalization exposes a detailed construction: graph spaces, compact spectral coordinates, projections, Galerkin coefficient ODEs, transport cancellation, exact energy identities, uniform estimates, space–time compactness, nonlinear convergence, a weakly continuous representative, and weak lower semicontinuity. The theorem presents the result through a smaller collection of properties of the established weakly continuous representative.

The reading point identifies one such state:

The approximating sequence establishes \(u_c\); the established representative supplies \(u_c(t)\) at every specified \(t\). The common refined subsequence supports the strong velocity limit, weak energy-space limit, weakly continuous representative, nonlinear passage, and energy inequality.

Here the transition from \(=\) to \(\leq\) is carried by weak convergence and weak lower semicontinuity. The resulting inherited energy inequality remains the every-time bound specified for the Leray–Hopf solution.

The global construction adds another lift. Integer-horizon representatives agree pointwise on overlaps, so a specified \(t\geq0\) can be read through any integer horizon containing it. Wang thereby obtains

The restriction of this path to every integer horizon retains the initial value, weak continuity, weak equation, and every-time energy inequality.

The specification grammar extracted from this example is

together with

For this paper, the grammar is an interpretation of the mathematical structure exposed by Wang’s formalization. Other approximation arguments can be read through their own leading constraints, engineering objects, measurable states, and limiting operations.