ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passjudge pass (gpt-6-luna)

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.

Zero-forcing discrete energy budget

Example

Take $f = 0$ and any initial weak-kernel velocity $u_{h}^{0} \in Z_{h}$ . Every backward Euler MINI solution satisfies $\frac{1}{2} ∥ u_{h}^{m} ∥_{2}^{2} + \frac{1}{2} \sum_{n = 1}^{m} ∥ u_{h}^{n} - u_{h}^{n - 1} ∥_{2}^{2} + ν \sum_{n = 1}^{m} τ_{n} ∥ \nabla u_{h}^{n} ∥_{2}^{2} \leq \frac{1}{2} ∥ u_{h}^{0} ∥_{2}^{2} .$

Facts & Assumptions

Given: A MINI mesh, a finite positive time partition, $f = 0$ , $u_{h}^{0} \in Z_{h}$ , and a scheme solution.

[F1]

The work-form energy inequality holds for every discrete solution. (Backward Euler MINI step existence and discrete energy bound)

Verification

1.1F1givenalgebra

Substitute $f_{h}^{n} = 0$ in the work-form inequality of [F1]. Its right side is exactly $\frac{1}{2} ∥ u_{h}^{0} ∥_{2}^{2}$ , while the jump and viscosity sums are nonnegative.

2.1step 1.1algebra∎

The inequality therefore bounds the kinetic energy at each node by its initial value and accounts separately for the nonnegative time-jump and viscous-dissipation terms. It is uniform in $h$ and in all positive step sizes; it does not assert strict decay when the velocity is stationary.

Depends on

Used by

A conditional three-dimensional computation with no uniqueness claim Example

Dependency tree · two levels

20 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.

Sources

Xiaoming He, Finite Element Methods, Chapter 9: unsteady Navier–Stokes equations (standard reference, not scraped)