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 natural Neumann condition from a free endpoint in one dimension

Example

Example. Assume Countable Choice (The Axiom of Countable Choice ( ${A C}_{ω}$ )) and let $a < b$ . On $C^{2} ([a, b])$ consider $I (u) = \int_{a}^{b} f (x, u (x), u^{'} (x)) d x$ with $f \in C^{2}$ , no boundary conditions, and let $u$ be a free-endpoint local minimiser in the $C^{2}$ norm. Retaining the boundary term produced by integration by parts gives, in addition to the Euler-Lagrange equation $f_{s} - \frac{d}{d x} f_{ξ} = 0$ (The classical Euler-Lagrange equation under regularity), the two natural boundary conditions $f_{ξ} (a, u (a), u^{'} (a)) = 0, f_{ξ} (b, u (b), u^{'} (b)) = 0,$ which are precisely the one-dimensional case of The natural boundary condition for free boundary variations. For $f (x, s, ξ) = \frac{1}{2} ξ^{2} - g (x) s$ they read $u^{''} = - g$ on $(a, b)$ with $u^{'} (a) = u^{'} (b) = 0$ .

Facts & Assumptions

Given: Countable Choice and $a < b$ ; a function $f \in C^{2} ([a, b] \times R \times R)$ , the functional $I (u) = \int_{a}^{b} f (x, u (x), u^{'} (x)) d x$ on $C^{2} ([a, b])$ with no boundary conditions, and a free-endpoint local minimiser $u$ : $I (u) \leq I (v)$ for all $v \in C^{2} ([a, b])$ with $∥ v - u ∥_{C^{2}}$ small.

[F1]

The endpoint conditions are the one-dimensional analogue of The natural boundary condition for free boundary variations, whose stated domain and Sobolev hypotheses do not cover this example. They will be proved directly below; the outward signs are $- 1$ at $a$ and $+ 1$ at $b$ .

[F2]

The interior equation has the form in The classical Euler-Lagrange equation under regularity, but is derived directly in step 2.1 because no global Sobolev growth bound is imposed here.

[F3]

Continuous partials make the integrand totally differentiable (If all partial derivatives exist on a neighbourhood and are continuous at a point, then the map is totally differentiable there with Jacobian derivative), and the chain rule (The chain rule for total derivatives: $D (g \circ f) (a) = D g (f (a)) \circ D f (a)$ ) computes its derivative along $(u + t ϕ, u^{'} + t ϕ^{'})$ as $f_{s} ϕ + f_{ξ} ϕ^{'}$ . First variation: for every $ϕ \in C^{\infty} ([a, b])$ the function $Φ (ε) : = I (u + ε ϕ)$ has an interior local minimum at $ε = 0$ and, by the mean value theorem applied to the $C^{2}$ integrand, $Φ^{'} (0) = \int_{a}^{b} (f_{s} (x, u, u^{'}) ϕ + f_{ξ} (x, u, u^{'}) ϕ^{'}) d x = 0$ (Fermat's interior extremum theorem: if $f$ has a local extremum at a point $c$ interior to its domain and is differentiable at $c$ , then $f^{'} (c) = 0$ , The mean value theorem, as the case $g (x) = x$ of Cauchy's: for $f$ continuous on $[a, b]$ with $a < b$ and differentiable on $(a, b)$ there is $c \in (a, b)$ with $f (b) - f (a) = f^{'} (c) (b - a)$ ).

[F4]

Integration by parts and the fundamental lemma: for $u \in C^{2}$ , $g \in C^{1}$ one has $\int_{a}^{b} (g ϕ^{'} + g^{'} ϕ) d x = [g ϕ]_{a}^{b}$ for every $ϕ \in C^{\infty} ([a, b])$ by Integration by parts for continuous factors with Riemann-integrable extensions of their interior derivatives; the continuous integrands have equal Riemann and Lebesgue integrals by A bounded Riemann integrable function on a closed bounded interval is Lebesgue measurable and has the same integral. A continuous function orthogonal to all compactly supported test functions vanishes (The fundamental lemma of the calculus of variations).

[F5]

Composites of $C^{k}$ Euclidean maps are $C^{k}$ , so $x \mapsto f_{ξ} (x, u (x), u^{'} (x))$ is $C^{1}$ when $f \in C^{2}$ and $u \in C^{2}$ ( $C^{k}$ Euclidean maps are closed under componentwise algebra and composition, $C^{k}$ maps and multi-index derivative notation in Euclidean space).

Verification

technique · direct, testing the first variation with compactly supported and with endpoint-supported variations

1.1F3given

The first-variation identity. Let $ϕ \in C^{\infty} ([a, b])$ . Since no boundary conditions are imposed, $u + ε ϕ$ lies in the admissible class for every $ε$ and for $∣ ε ∣$ small it is close to $u$ in the $C^{2}$ norm, so $Φ (ε) = I (u + ε ϕ)$ has an interior local minimum at $0$ ; the mean value theorem expresses the integrand difference quotient as $f_{s} (x, u + θ ε ϕ, u^{'} + θ ε ϕ^{'}) ϕ + f_{ξ} (x, u + θ ε ϕ, u^{'} + θ ε ϕ^{'}) ϕ^{'}$ for some $0 < θ < 1$ . Heine--Cantor (Heine-Cantor: a continuous map from a compact metric space to any metric space is uniformly continuous) makes the partials uniformly continuous on a compact set containing these arguments, this quotient therefore converges uniformly to its value at $ε = 0$ , and its integral is $Φ^{'} (0)$ . Fermat's theorem in [F3] then gives $\int_{a}^{b} (f_{s} (x, u, u^{'}) ϕ + f_{ξ} (x, u, u^{'}) ϕ^{'}) d x = 0$ .

2.1F2F4F5step 1.1

The interior equation. Taking $ϕ \in C_{c}^{\infty} ((a, b))$ in step 1.1 and integrating by parts, using that $x \mapsto f_{ξ} (x, u (x), u^{'} (x))$ is $C^{1}$ by [F5] and has derivative $\frac{d}{d x} f_{ξ} (x, u, u^{'})$ , gives $\int_{a}^{b} (f_{s} (x, u, u^{'}) - \frac{d}{d x} f_{ξ} (x, u, u^{'})) ϕ d x = 0$ for every compactly supported $ϕ$ ; the integrand is continuous, so [F4] gives $f_{s} - \frac{d}{d x} f_{ξ} = 0$ on $(a, b)$ , the classical Euler-Lagrange equation.

3.1F4step 1.1step 2.1

The boundary identity. Let now $ϕ \in C^{\infty} ([a, b])$ be arbitrary. Writing $g : = f_{ξ} (x, u, u^{'})$ and using the interior equation of step 2.1, step 1.1 becomes $0 = \int_{a}^{b} (\frac{d}{d x} g ϕ + g ϕ^{'}) d x = [g ϕ]_{a}^{b} = g (b) ϕ (b) - g (a) ϕ (a)$ by [F4], that is $f_{ξ} (b, u (b), u^{'} (b)) ϕ (b) - f_{ξ} (a, u (a), u^{'} (a)) ϕ (a) = 0$ for every $ϕ \in C^{\infty} ([a, b])$ .

4.1F1step 2.1step 3.1∎

Both natural conditions, and the instance. Choosing in step 3.1 $ϕ (x) = (b - x) / (b - a)$ gives $f_{ξ} (a, u (a), u^{'} (a)) = 0$ , and $ϕ (x) = (x - a) / (b - a)$ gives $f_{ξ} (b, u (b), u^{'} (b)) = 0$ ; these are the one-dimensional natural boundary conditions, the general form of [F1]. For $f (x, s, ξ) = \frac{1}{2} ξ^{2} - g (x) s$ one has $f_{ξ} = ξ$ and $f_{s} = - g (x)$ , so the interior equation of step 2.1 reads $u^{''} = - g$ on $(a, b)$ and the natural conditions read $u^{'} (a) = u^{'} (b) = 0$ .

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

91 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

Riccardo Cristoferi, Calculus of Variations: Lecture Notes, Carnegie Mellon University 2016 (complete 133-page notes) (standard reference, not scraped)
Sung-Jin Oh, Lecture Notes for Math 222A, UC Berkeley, 19 March 2024 (complete 179-page author PDF) (standard reference, not scraped)