CounterexampleConstruction: 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.

Critical traces fail compactness under boundary dilation

Statement refuted

Refuted claim. The Sobolev trace is compact at its critical boundary exponent: for a bounded $C^{1}$ domain $Ω \subset R^{n}$ the trace map $T : W^{1, p} (Ω) \to L^{q_{\partial}} (\partial Ω)$ , $1 < p < n$ , $n \geq 2$ , and $q_{\partial} = \frac{p (n - 1)}{n - p}$ , would send every bounded sequence to a sequence with a strongly convergent subsequence.

The witness is a boundary bubble: one fixed smooth boundary profile dilated by the factor $j$ , with the bulk amplitude scaled so that the $W^{1, p}$ norm stays bounded and the critical trace norm stays fixed while the support shrinks to a single boundary point.

Facts & Assumptions

Given: the Axiom of Choice; $n \geq 2$ ; $1 < p < n$ ; $q_{\partial} = \frac{p (n - 1)}{n - p}$ ; a bounded $C^{1}$ domain $Ω \subset R^{n}$ with the following explicit flat boundary patch. Start with $B (e_{n}, 1)$ , whose lower boundary near $0$ is $t = h (y) = 1 - \sqrt{1 - ∣ y ∣^{2}}$ . Choose $a \in C_{c}^{\infty} (R^{n - 1})$ equal to $h$ near $0$ , using an interior cutoff. The global smooth diffeomorphism $F (y, t) = (y, t - a (y))$ has inverse $(y, t) \mapsto (y, t + a (y))$ and determinant $1$ . Set $Ω = F (B (e_{n}, 1))$ . It is bounded with smooth boundary and locally $Ω = {x_{n} > 0}$ , $\partial Ω = {x_{n} = 0}$ ; and a nonzero $ψ \in C_{c}^{\infty} (R^{n})$ supported in a sufficiently small ball inside that patch, with boundary restriction $g (x^{'}) : = ψ (x^{'}, 0)$ not identically $0$ . Write $R_{+}^{n} : = {y \in R^{n} : y_{n} > 0}$ . For large $j$ put $u_{j} (x) : = j^{(n - p) / p} ψ (j x)$ .

[F1]

The trace operator. $T : W^{1, p} (Ω) \to L^{p} (\partial Ω)$ is bounded and $T u = u ∣_{\partial Ω}$ for every $u$ continuous on $\overline{Ω}$ and in $W^{1, p} (Ω)$ . (The $L^{p}$ trace operator on a bounded $C^{1}$ domain)

[F2]

Surface measure on the flat patch. On the patch ${x_{n} = 0} \cap {small ∣ x^{'} ∣}$ the surface measure of Surface integration on compact C1 hypersurfaces is $(n - 1)$ -dimensional Lebesgue measure; $ψ$ compactly supported in the patch gives a compactly supported, smooth boundary restriction $g$ . (Surface integration on compact C1 hypersurfaces, A Euclidean bump for a compact set inside an open set)

[F3]

Scaling. For measurable nonnegative $h$ and $j > 0$ , $\int h (j z) j^{m} d z = \int h$ on $R^{m}$ for each $m$ . (A linear map $T$ of $R^{n}$ sends Lebesgue measurable sets to Lebesgue measurable sets, with $λ_{n} (T [E]) = ∣ \det T ∣ λ_{n} (E)$ when $T$ is invertible and $T [E]$ Lebesgue null when it is not)

[F4]

Almost-everywhere subsequences. Every $L^{q}$ -convergent sequence, $1 \leq q < \infty$ , has a subsequence converging almost everywhere to a representative of its limit. (Assuming Countable Choice, $L^{p}$ -convergent sequences have almost-everywhere convergent subsequences)

[F5]

Class norms. $L^{q}$ norms are computed on almost-everywhere classes and are continuous under strong convergence; $W^{1, p}$ carries the norm of Integer-order Sobolev spaces and their norms. (The space $L^{p} (μ)$ as the quotient by null functions, Integer-order Sobolev spaces and their norms)

Counterexample

technique · direct

1.1F3F5given

For all sufficiently large $j$ , the support of $ψ (j \cdot)$ on $Ω$ lies inside the flat patch, where $Ω$ is the upper half-space; the restriction of the ambient smooth function is therefore smooth up to the boundary and belongs to $W^{1, p} (Ω)$ . By [F3] and the change of variables over that half-space, $∥ u_{j} ∥_{L^{p} (Ω)} = j^{(n - p) / p} j^{- n / p} ∥ ψ ∥_{L^{p} (R_{+}^{n})} = j^{- 1} ∥ ψ ∥_{L^{p} (R_{+}^{n})}$ and $∥ D u_{j} ∥_{L^{p} (Ω)} = j^{(n - p) / p} j^{1 - n / p} ∥ D ψ ∥_{L^{p} (R_{+}^{n})} = ∥ D ψ ∥_{L^{p} (R_{+}^{n})}$ , so $\sup_{j} ∥ u_{j} ∥_{W^{1, p} (Ω)} < \infty$ (discarding the finitely many initial indices if needed).

1.2F1F2F3given

By [F1] and [F2], $T u_{j}$ is the restriction of $u_{j}$ to $\partial Ω$ , which equals $j^{(n - p) / p} g (j x^{'})$ on the flat patch and $0$ elsewhere. By [F2] and [F3] with $m = n - 1$ , $∥ T u_{j} ∥_{L^{q_{\partial}} (\partial Ω)}^{q_{\partial}} = j^{(n - p) q_{\partial} / p} j^{- (n - 1)} ∥ g ∥_{L^{q_{\partial}}}^{q_{\partial}} = ∥ g ∥_{L^{q_{\partial}}}^{q_{\partial}} > 0$ , because $\frac{(n - p) q_{\partial}}{p} = n - 1$ ; and $T u_{j} (x^{'}) \to 0$ for every $x^{'} \neq 0$ on the patch, since $g$ is compactly supported, while off the patch $T u_{j} = 0$ for all large $j$ .

2.1F1F4F5step 1.1step 1.2∎

Suppose a subsequence of $(T u_{j})$ converged strongly in $L^{q_{\partial}} (\partial Ω)$ to some $v$ . Then $∥ v ∥_{L^{q_{\partial}}} = ∥ g ∥_{L^{q_{\partial}}} > 0$ by continuity of the norm [F5], while by [F4] a further subsequence converges almost everywhere to a representative of $v$ ; since the traces converge to $0$ at every boundary point except the single point $0$ , which has surface measure zero, that representative vanishes almost everywhere, so $∥ v ∥ = 0$ by [F5], a contradiction. Hence the bounded $W^{1, p}$ -sequence $(u_{j})$ has no subsequence whose traces converge strongly at the critical boundary exponent, and the refuted compactness claim is false. The Axiom of Choice is inherited through the trace interface [F1].

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

71 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

Richard S. Laugesen, Linear Analysis and Partial Differential Equations, full graduate notes (standard reference, not scraped)
Juha Kinnunen, Sobolev Spaces, complete 168-page 2026 notes (standard reference, not scraped)