ExampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6.1-sol)

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 harmonic affine extension minimises the Dirichlet energy

Example

Example. Assume the Axiom of Choice (The Axiom of Choice). Let $Ω \subseteq R^{n}$ , $n \geq 2$ , be a bounded $C^{1}$ domain and let $a (x) = c_{0} + ℓ (x)$ be affine on $\overline{Ω}$ , so that $Δ a = 0$ and $D a = ℓ$ is constant. Then $a$ is the unique minimiser of the Dirichlet energy $I (v) = \frac{1}{2} \int_{Ω} ∣ D v ∣^{2} d x$ on the affine trace class $K_{a} = {v \in H^{1} (Ω) : T v = T a}$ (The $L^{p}$ trace operator on a bounded $C^{1}$ domain): for every $v \in K_{a}$ , $v - a \in H_{0}^{1} (Ω)$ and $I (v) = I (a) + \frac{1}{2} \int_{Ω} ∣ D (v - a) ∣^{2} d x \geq I (a),$ with equality if and only if $D (v - a) = 0$ almost everywhere, and then $v = a$ almost everywhere by the Poincare inequality on $H_{0}^{1} (Ω)$ (The Poincare inequality for zero-boundary Sobolev closures on domains bounded in one direction).

Facts & Assumptions

Given: The Axiom of Choice; a bounded $C^{1}$ domain $Ω \subseteq R^{n}$ , an affine function $a (x) = c_{0} + ℓ (x)$ on $\overline{Ω}$ (so $D a = ℓ$ is a constant field and $Δ a = 0$ ), the Dirichlet energy $I (v) = \frac{1}{2} \int_{Ω} ∣ D v ∣^{2} d x$ , and the affine trace class $K_{a} = {v \in H^{1} (Ω) : T v = T a}$ .

[F1]

$K_{a}$ is nonempty, convex and weakly closed, and $v - a \in H_{0}^{1} (Ω)$ for every $v \in K_{a}$ by the kernel description $\ker T = H_{0}^{1} (Ω)$ (The kernel of the trace is the closure of the test functions, The $L^{p}$ trace operator on a bounded $C^{1}$ domain).

[F2]

Poincare's inequality on $H_{0}^{1} (Ω)$ : if $D η = 0$ almost everywhere for $η \in H_{0}^{1} (Ω)$ , then $η = 0$ (The Poincare inequality for zero-boundary Sobolev closures on domains bounded in one direction).

[F3]

Under the Axiom of Choice, the ultrafilter lemma, Dependent Choice and Hahn--Banach, the Dirichlet principle also identifies an affine-class minimiser with the unique weak solution (The Dirichlet principle for the Poisson equation). In the zero-forcing case here, $a$ is weakly harmonic with trace $T a$ , since $D a = ℓ$ is constant and $\int_{Ω} D a \cdot D φ = ℓ \cdot \int_{Ω} D φ = 0$ for every $φ \in H_{0}^{1} (Ω)$ (The notation $H^{k}$ and the reserved zero-boundary symbol).

Verification

technique · direct completion of the square

1.1F1algebra

Orthogonality of the cross term. For $v \in K_{a}$ one has $η : = v - a \in H_{0}^{1} (Ω)$ by [F1], and $D a = ℓ$ is a constant field, so $\int_{Ω} D a \cdot D η d x = ℓ \cdot \int_{Ω} D η d x = 0$ : each component of $D η$ has vanishing integral, because $η$ is the $H^{1}$ -limit of functions in $C_{c}^{\infty} (Ω)$ and for those the integral of each partial derivative vanishes by integration by parts against the smooth constant field (Divergence on a bounded C1 Euclidean domain). Passage to the $H^{1}$ limit is valid since $∣ \int D_{i} (η - η_{m}) ∣ \leq ∣ Ω ∣^{1 / 2} ∥ D_{i} (η - η_{m}) ∥_{2} \to 0$ by Holder (Holder's inequality for integrals, including the endpoint cases).

2.1step 1.1algebra

The energy identity. Expanding the square, $∣ D v ∣^{2} = ∣ D a + D η ∣^{2} = ∣ D a ∣^{2} + 2 D a \cdot D η + ∣ D η ∣^{2}$ , and integrating with step 1.1 gives $I (v) = I (a) + \frac{1}{2} \int_{Ω} ∣ D η ∣^{2} d x \geq I (a)$ .

3.1F2step 2.1

Equality case. Equality holds exactly when $D η = 0$ almost everywhere, which by [F2] forces $η = 0$ , that is $v = a$ almost everywhere.

4.1F3step 2.1step 3.1∎

$a$ is the minimiser. By steps 2.1 and 3.1 every $v \in K_{a}$ satisfies $I (v) \geq I (a)$ with equality only for $v = a$ ; since $a \in K_{a}$ , it is the unique minimiser of $I$ on $K_{a}$ . This direct completion-of-the-square argument proves the example's claim. Under the additional choice hypotheses stated in [F3], the general Dirichlet principle also identifies this minimiser with the weak solution; the weak harmonicity of $a$ was checked in [F3].

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

70 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

Gerald Teschl, Partial Differential Equations: From Classical to Modern (2026 author manuscript; complete 392-page archived text) (standard reference, not scraped)
Riccardo Cristoferi, Calculus of Variations: Lecture Notes, Carnegie Mellon University 2016 (complete 133-page notes) (standard reference, not scraped)