Pipeline-generated

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.

✓ 2 results · all verified · 2 also independently AI-judged

Every result on this page is machine-checked by a proof checker and read in full by a delegated reviewing agent on the owner's instruction; the judge is an additional, independent cross-model AI review of the proofs; all 2 also cleared it.

Nonlinear maps and tangential cone control — Examples and Counterexamples

1 · Prerequisites

2 · Logical flowchart

3 · Definitions, theorems and proofs

None yet.

4 · Examples, counterexamples and false statements

CounterexampleConstruction: AI-generatedVerification: AI-generatedprecheck passjudge pass (gpt-6-luna)verified 2026-10-22 (gpt-6.1-sol)Open item page →

A smooth map can fail the tangential cone condition

Statement refuted

Every infinitely differentiable forward map between real Hilbert spaces satisfies a local tangential cone condition at each point of its domain with some radius $δ > 0$ and some constant $0 \leq η < 1$ .

Statement references

Local tangential cone condition

Christian Clason, Regularization of Inverse Problems, equation (9.6)

Facts & Assumptions

Given: The standard real Hilbert line $X = Y = R$ , the map $F (t) = t^{2}$ , basepoint $x^{†} = 0$ , exact datum $y = 0$ , and a proposed local TCC radius $δ > 0$ with constant $0 \leq η < 1$ .

[F1]

The one-coordinate Euclidean inner product is $⟨ s, t ⟩ = s t$ , with induced Euclidean norm (The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ ).

[F2]

The induced Euclidean length on $R^{1}$ is a norm (Cauchy-Schwarz $∣ ⟨ x, y ⟩ ∣ \leq ∥ x ∥_{2} ∥ y ∥_{2}$ with its equality case, the triangle inequality for $∥ \cdot ∥_{2}$ , the parallelogram law and polarisation).

[F3]

Every Cauchy sequence of real numbers converges (The reals are complete).

[F4]

A real inner-product space complete in its induced norm is a real Hilbert space (Real and complex inner-product spaces and their induced length, Hilbert space).

[F5]

A Fréchet derivative is a bounded linear map whose remainder divided by the increment norm tends to zero (Fréchet derivative between Banach spaces).

[F6]

The local TCC at $0$ would require $∣ F (h) - F (0) - F^{'} (0) h ∣ \leq η ∣ F (h) - F (0) ∣$ whenever $∣ h ∣ \leq δ$ (Local tangential cone condition).

Counterexample

technique · direct

1.1givenF1F2F3F4F5constructalgebra

Identify $R$ with the one-coordinate Euclidean space $R^{1}$ by its sole coordinate; [F1] gives inner product $s t$ and [F2] gives norm $∣ t ∣$ . Every Cauchy sequence for this norm converges by [F3], so [F4] makes $R$ a real Hilbert space. The polynomial $F (t) = t^{2}$ is infinitely differentiable; moreover $∣ F (h) - F (0) - 0 h ∣ / ∣ h ∣ = ∣ h ∣ \to 0$ as $h \to 0$ , so [F5] gives $F^{'} (0) = 0$ .

2.1givenF6choosealgebra∎

Since $δ > 0$ , choose $h = δ / 2$ , which is nonzero and satisfies $∣ h ∣ \leq δ$ . Substitution in [F6] gives $h^{2} \leq η h^{2}$ , hence $1 \leq η$ after division by $h^{2} > 0$ , contradicting $η < 1$ . Therefore no such TCC radius and constant exist.

References

Nonlinear forward-map convention

Local tangential cone condition

Christian Clason, Regularization of Inverse Problems, equation (9.6)

ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passjudge pass (gpt-6-luna)verified 2026-10-22 (gpt-6.1-sol)Open item page →

A smooth map with a local tangential cone neighborhood

Example

Let $X = Y = R$ with their usual real Hilbert structure, let $U = R$ , and define the smooth forward map $F (t) = t + t^{2}$ . At $x^{†} = 1$ the exact datum is $y = F (1) = 2$ . The local tangential cone condition holds at $1$ on the closed ball of radius $δ = 1 / 4$ with constant $η = 1 / 10$ .

Example references

Nonlinear forward maps and exact data

Local tangential cone condition

Fréchet derivative

Christian Clason, Regularization of Inverse Problems, equation (9.6)

Facts & Assumptions

Given: The standard real Hilbert line $X = Y = R$ , $U = R$ , $F (t) = t + t^{2}$ , $x^{†} = 1$ , $y = 2$ , $δ = 1 / 4$ , and $η = 1 / 10$ .

[F1]

The one-coordinate Euclidean inner product is $⟨ s, t ⟩ = s t$ , with induced Euclidean norm (The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ ).

[F2]

[F3]

Every Cauchy sequence of real numbers converges, and a complete real inner-product space is a real Hilbert space (The reals are complete, Real and complex inner-product spaces and their induced length, Hilbert space).

[F4]

The Fréchet derivative is characterized by a remainder that is $o (∥ h ∥)$ (Fréchet derivative between Banach spaces).

[F5]

The local TCC requires $∥ F (x + h) - F (x) - F^{'} (x) h ∥ \leq η ∥ F (x + h) - F (x) ∥$ for every increment in its closed ball (Local tangential cone condition).

Verification

technique · direct

1.1givenF4algebra

For $h \in R$ , $F (1 + h) - F (1) = 3 h + h^{2}$ , so $F (1 + h) - F (1) - 3 h = h^{2}$ . Since $∣ h^{2} ∣ / ∣ h ∣ = ∣ h ∣ \to 0$ , [F4] gives $F^{'} (1) h = 3 h$ ; the polynomial is smooth.

2.1givenF1F2F3F5algebra∎

For $∣ h ∣ \leq 1 / 4$ , the TCC remainder is $∣ h ∣^{2}$ and the data difference has magnitude $∣ 3 h + h^{2} ∣ = ∣ h ∣ ∣ 3 + h ∣$ . If $h \neq 0$ , then $∣ 3 + h ∣ \geq 3 - ∣ h ∣ \geq 11 / 4$ , so $∣ h ∣ / ∣ 3 + h ∣ \leq (1 / 4) / (11 / 4) = 1 / 11 < 1 / 10$ . Thus $∣ h ∣^{2} \leq (1 / 10) ∣ 3 h + h^{2} ∣$ ; for $h = 0$ both sides vanish. Since ${\overline{B}}_{1 / 4} (1) \subset R$ and $F (1) = 2$ , this verifies the stated local TCC neighborhood.

Nonlinear maps and tangential cone control — Examples and Counterexamples

2 · Logical flowchart

3 · Definitions, theorems and proofs

4 · Examples, counterexamples and false statements

A smooth map can fail the tangential cone condition

Statement refuted

Statement references

Facts & Assumptions

Counterexample

References

A smooth map with a local tangential cone neighborhood

Example

Example references

Facts & Assumptions

Verification

Sources