ExampleConstruction: AI-generatedVerification: AI-generatedprecheck pass

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

The two-dimensional Taylor–Green vortex on the flat torus

Example

This is a periodic-boundary example, not a no-slip example. On the torus obtained by identifying opposite sides of $(0, 2 π)^{2}$ , let $A (t) = e^{- 2 ν t}$ and define $u (x, y, t) = A (t) (\sin x \cos y, - \cos x \sin y), p (x, y, t) = \frac{A (t)^{2}}{4} (\cos 2 x + \cos 2 y) .$ The pressure is periodic and has zero mean on the fundamental square.

\begin{center} \begin{tikzpicture}[scale=0.85] \draw[thick] (0,0) rectangle (4,2.6); \node at (2,1.3) {fundamental square}; \node[blue] at (2,2.82) { $y = 0 \sim 2 π$ }; \node[blue] at (2,-0.22) { $y = 0 \sim 2 π$ }; \node[red,rotate=90] at (-0.28,1.3) { $x = 0 \sim 2 π$ }; \node[red,rotate=90] at (4.28,1.3) { $x = 0 \sim 2 π$ }; \end{tikzpicture} \end{center}

The rectangle is only a fundamental-domain picture: each pair of equally labelled opposite edges is identified point-for-point, so fields and derivatives must be periodic across the seams. The picture records the topology; the verification below is analytic.

Facts & Assumptions

Given: $ν > 0$ , the periodic square with opposite-edge identification, and the displayed smooth fields.

[F2]

Derivatives of sine and cosine and the double-angle identity are the usual real calculus identities. (The derivatives of sine and cosine are cosine and minus sine, Double-angle and quadratic power-reduction identities)

[F3]

Sine and cosine have period $2 π$ . (The zero sets of sine and cosine and the least positive common period 2 pi)

[F4]

$A^{'} (t) = - 2 ν A (t)$ , and the second fundamental theorem evaluates the integral of the continuous function $\cos (2 x)$ using its differentiable primitive $\frac{1}{2} \sin (2 x)$ . (The exponential function is smooth and $(\exp)^{'} = \exp$ , The derivatives of sine and cosine are cosine and minus sine, The second fundamental theorem: if $G$ is differentiable on $[a, b]$ with $G^{'} = f$ and $f$ is integrable, then $\int_{a}^{b} f = G (b) - G (a)$ )

Verification

1.1F2F3F4givenalgebra

By [F2]–[F3], the fields and all their derivatives are periodic across opposite edges. Differentiating gives $div u = A (\cos x \cos y - \cos x \cos y) = 0$ and $Δ u = - 2 u$ . Since $A^{'} = - 2 ν A$ by [F4], one has $\partial_{t} u = ν Δ u$ .

2.1F2F3F4step 1.1algebra∎

The derivatives are $\partial_{x} u_{1} = A \cos x \cos y$ , $\partial_{y} u_{1} = - A \sin x \sin y$ , $\partial_{x} u_{2} = A \sin x \sin y$ , and $\partial_{y} u_{2} = - A \cos x \cos y$ . Direct multiplication gives $(u \cdot \nabla) u = \frac{A^{2}}{2} (\sin 2 x, \sin 2 y), \nabla p = - \frac{A^{2}}{2} (\sin 2 x, \sin 2 y) .$ Thus $\partial_{t} u + (u \cdot \nabla) u + \nabla p - ν Δ u = 0$ . By [F4], $\int_{0}^{2 π} \cos (2 x) d x = \frac{1}{2} (\sin 4 π - \sin 0) = 0$ , and the identical calculation gives $\int_{0}^{2 π} \cos (2 y) d y = 0$ ; hence $p$ has zero mean at every time. At $x = 0$ and $y = π / 3$ , $u_{2} = - A \sin (π / 3) \neq 0$ , so this periodic solution does not satisfy homogeneous no-slip data on the square boundary.

Remarks

The skew form in The skew convective form for incompressible flow is defined for zero-boundary fields on bounded Lipschitz domains. This periodic example is verified directly from its classical strong equation; it does not identify these fields with the no-slip test space.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

35 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.