ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck 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.

Fixing the spatially constant pressure mode

Example

Assume Countable Choice. On a nonempty bounded connected open set $D \subset R^{d}$ , adding any spatial constant $c (t)$ to a pressure does not change the weak momentum equation with zero-boundary velocity tests. The condition $p (t) \in L_{0}^{2} (D)$ fixes that freedom uniquely.

Facts & Assumptions

Given: Countable Choice, a nonempty bounded connected open $D \subset R^{d}$ , $p (t) \in L^{2} (D)$ , $v \in H_{0}^{1} (D)^{d}$ , and a scalar $c (t)$ .

[F1]

Under Countable Choice, zero-boundary divergence belongs to $L^{2} (D)$ and has zero spatial integral on every bounded open $D$ . (The Axiom of Countable Choice ( ${A C}_{ω}$ ), Zero mean of the divergence of a zero-boundary field)

[F2]

Holder makes $p \in L^{2} (D)$ integrable and the pairing $\tilde{b} (v, p) : = - \int_{D} p div v$ finite for every $p \in L^{2} (D)$ . This explicitly extends the mean-zero pressure pairing; on the Lipschitz domains in dimensions two and three of Stokes velocity and pressure spaces and weak forms, it agrees with $b$ when $p \in L_{0}^{2} (D)$ . (Holder's inequality for integrals, including the endpoint cases)

Verification

1.1F1F2givenalgebra

The pressure term changes by $\tilde{b} (v, p + c (t)) - \tilde{b} (v, p) = - c (t) \int_{D} div v = 0$ by [F1]. Therefore the weak equation cannot distinguish pressures differing by a function constant in space.

2.1F2step 1.1givenalgebra∎

Put $\overset{ˉ}{p} = ∣ D ∣^{- 1} \int_{D} p$ . Then $p - \overset{ˉ}{p}$ has zero mean. If both $p + c_{1} (t)$ and $p + c_{2} (t)$ have zero mean, integration over $D$ gives $∣ D ∣ (c_{1} - c_{2}) = 0$ ; because $∣ D ∣ > 0$ , $c_{1} = c_{2}$ .

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

23 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

Jean-Luc Guermond, MATH 661 Fall 2025, Chapter 53: Stokes equations (standard reference, not scraped)