ExampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generatedjudge 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 one-dimensional obstacle reaction is supported on the contact set

Example

Assume the Axiom of Choice and Countable Choice (The Axiom of Choice, The Axiom of Countable Choice ( ${A C}_{ω}$ )), inherited from the obstacle example. In A one-dimensional obstacle problem and its contact set, the solution $u$ lies in $H^{2} (- 1, 1)$ with $u^{''} = ψ^{''} = - 1$ on $(- t, t)$ and $u^{''} = 0$ on the noncontact set ${t < ∣ x ∣ < 1}$ . The reaction distribution $Λ (φ) = \int_{- 1}^{1} u^{'} φ^{'} d x = - \int_{- 1}^{1} u^{''} φ d x$ of Obstacle complementarity in distribution form equals $\int_{- 1}^{1} 1_{[- t, t]} φ d x$ : it is represented by the nonnegative density $1_{{u = ψ}}$ , has mass $2 t$ , and has no atom at the free boundary points $\pm t$ because $u^{'}$ is continuous there.

Facts & Assumptions

Given: The obstacle example A one-dimensional obstacle problem and its contact set with $Ω = (- 1, 1)$ , $0 < ε < 1 / 2$ , $t = 1 - \sqrt{1 - 2 ε} \in (0, 1)$ , the obstacle $ψ (x) = ε - x^{2} / 2$ , the solution $u (x) = ψ (x)$ for $∣ x ∣ \leq t$ and $u (x) = t (1 - ∣ x ∣)$ for $t \leq ∣ x ∣ \leq 1$ , and the reaction $Λ (φ) = a (u, φ) = \int_{- 1}^{1} u^{'} φ^{'} d x$ on test functions (Distribution, Test function space d of an open set, Distributional derivative).

[F1]

A one-dimensional obstacle problem and its contact set: $u$ is the unique obstacle solution on $K = {v \in H_{0}^{1} (- 1, 1) : v \geq ψ}$ ; it is $C^{1}$ on $[- 1, 1]$ with $u^{'} (x) = t$ for $x \in (- 1, - t)$ , $u^{'} (x) = - x$ for $x \in (- t, t)$ , $u^{'} (x) = - t$ for $x \in (t, 1)$ , and its slopes match the obstacle at $\pm t$ ; the contact set is ${u = ψ} = [- t, t]$ .

[F2]

Classical derivatives agree with weak derivatives, Integer-order Sobolev spaces and their norms: the classical derivative of a $C^{1}$ function is its weak derivative, and $H^{2} (- 1, 1)$ consists of the classes in $L^{2}$ with first and second weak derivatives in $L^{2}$ .

[F3]

Integration by parts for absolutely continuous functions: for absolutely continuous $F, G$ on $[- 1, 1]$ , $\int_{- 1}^{1} F G^{'} = - \int_{- 1}^{1} F^{'} G + F (1) G (1) - F (- 1) G (- 1)$ .

[F4]

Obstacle complementarity in distribution form: the reaction of the solution is the distribution $Λ (φ) = a (u, φ) - \int_{Ω} f φ$ on $C_{c}^{\infty} (- 1, 1)$ , here with $f = 0$ .

[F5]

Every at most countable subset of $R^{n}$ is Lebesgue null; in particular $λ_{1} (Q) = 0$ , A nonnegative integral over a null set vanishes: countable subsets of $R$ are Lebesgue-null and the integral of a nonnegative measurable function over a null set vanishes; for $φ \in C_{c}^{\infty} (- 1, 1)$ the pairing against the density $1_{[- t, t]}$ is $\int_{{- t, t}} 1_{[- t, t]} φ d x = 0$ .

[F6]

The space $L^{p} (μ)$ as the quotient by null functions: $1_{[- t, t]}$ is an $L^{\infty}$ , hence $L^{2}$ , class determined up to null sets, and the pairing $\int 1_{[- t, t]} φ d x$ depends only on this class.

Verification

technique · direct

Given: The explicit solution $u$ and the reaction functional $Λ$ above.

1.1givenF1F2F3

By [F1] the derivative $u^{'}$ equals $t$ on $(- 1, - t)$ , $- x$ on $(- t, t)$ and $- t$ on $(t, 1)$ ; it is continuous and piecewise affine on $[- 1, 1]$ with matching one-sided values, hence Lipschitz and absolutely continuous, and its a.e. derivative is $u^{''} = 0$ on $(- 1, - t) \cup (t, 1)$ and $u^{''} = - 1$ on $(- t, t)$ . For each compactly supported smooth test $φ$ , [F3] gives $\int u^{'} φ^{'} = - \int u^{''} φ$ , proving that this a.e. derivative is the weak derivative of $u^{'}$ . Since $u^{''} \in L^{\infty} (- 1, 1) \subseteq L^{2} (- 1, 1)$ , [F2] gives $u \in H^{2} (- 1, 1)$ with weak second derivative $u^{''}$ ; in particular $u^{''} = ψ^{''} = - 1$ on the contact interval and $u^{''} = 0$ on the noncontact set.

2.1step 1.1F3F4

For every $φ \in C_{c}^{\infty} (- 1, 1)$ integration by parts [F3] applied to the absolutely continuous $u^{'}$ and the smooth compactly supported $φ$ gives $Λ (φ) = \int_{- 1}^{1} u^{'} φ^{'} d x = - \int_{- 1}^{1} u^{''} φ d x$ , the endpoint terms vanishing because $φ$ is compactly supported; by step 1.1 the right-hand side equals $\int_{- t}^{t} φ d x = \int_{- 1}^{1} 1_{[- t, t]} φ d x$ . Hence the reaction is represented by the density $1_{[- t, t]}$ on all test functions.

3.1step 2.1F5F6

The density $1_{[- t, t]}$ is nonnegative and lies in $L^{\infty} (- 1, 1) \subseteq L^{2} (- 1, 1)$ [F6]; its total mass is $\int_{- 1}^{1} 1_{[- t, t]} d x = 2 t$ . Since the free boundary points $\pm t$ form a Lebesgue-null set, the pairing against $1_{[- t, t]}$ assigns them value zero, so the reaction has no atom at $\pm t$ ; concretely $\int_{{- t, t}} 1_{[- t, t]} φ d x = 0$ for every test function by [F5].

4.1step 1.1step 2.1step 3.1∎

Steps 1.1, 2.1 and 3.1 prove all the asserted properties: $u \in H^{2} (- 1, 1)$ with $u^{''} = - 1$ on $(- t, t)$ and $u^{''} = 0$ on the noncontact set, the reaction $Λ (φ) = \int u^{'} φ^{'} = - \int u^{''} φ$ is represented by the nonnegative density $1_{{u = ψ}} = 1_{[- t, t]}$ , its mass is $2 t$ , and it gives the Lebesgue-null set ${- t, t}$ the value $0$ , because the continuous derivative $u^{'}$ produces no boundary contribution at the free boundary points in the integration by parts.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

61 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

John Andersson, The Obstacle Problem, KTH lecture notes, 16 December 2015 (complete 52-page notes) (standard reference, not scraped)