ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24

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.

A Euclidean sphere is a regular level set with tangent hyperplanes

Example

For $R > 0$ , the sphere $S_{R}^{m - 1} = {x \in R^{m} : ∥ x ∥_{2} = R}$ is the regular level $F^{- 1} (R^{2})$ of $F (x) = ∥ x ∥_{2}^{2}$ . At $x \in S_{R}^{m - 1}$ , $T_{x} S_{R}^{m - 1} = x^{⊥} = {h : ⟨ x, h ⟩ = 0} .$

Facts & Assumptions

Given: A radius $R > 0$ and $F (x) = ⟨ x, x ⟩$ on $R^{m}$ , with $m \geq 1$ .

[L1]

The Euclidean norm satisfies $∥ x ∥_{2}^{2} = ⟨ x, x ⟩$ (The $p$ -norms $∥ x ∥_{p}$ for rational $p \geq 1$ , and $∥ x ∥_{\infty}$ , The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ ). The power rule and one-variable derivative algebra give the continuous Jacobian row $J F (x) = 2 x^{T}$ , and continuous partial derivatives imply $D F (x) h = 2 ⟨ x, h ⟩$ (For a natural $n \geq 1$ the function $x \mapsto x^{n}$ is differentiable everywhere with derivative $ι (n) x^{n - 1}$ ; for $n = 0$ it is the constant $1$ , with derivative $0$ ; for a natural $n \geq 1$ the function $x \mapsto x^{- n}$ is differentiable at every $x \neq 0$ with derivative $- ι (n) x^{- n - 1}$ ; consequently every polynomial function is differentiable at every real, with the derivative computed term by term, Sums, scalar multiples, products and quotients: $(f + g)^{'} (c) = f^{'} (c) + g^{'} (c)$ , $(α f)^{'} (c) = α f^{'} (c)$ , $(f g)^{'} (c) = f^{'} (c) g (c) + f (c) g^{'} (c)$ , and $(f / g)^{'} (c) = (f^{'} (c) g (c) - f (c) g^{'} (c)) / g (c)^{2}$ when $g (c) \neq 0$ , The Jacobian matrix of partial derivatives and the gradient in the scalar-valued case, If all partial derivatives exist on a neighbourhood and are continuous at a point, then the map is totally differentiable there with Jacobian derivative).

[L2]

A regular level is locally a graph, its tangent space is the derivative kernel, and its tangent vectors are exactly its curve velocities (A regular level set is locally a $C^{k}$ graph of dimension $m - n$ , The tangent space to a regular level set, Tangent vectors to a regular level set are exactly its curve velocities).

Verification

technique · direct

1.1givenL1

By [L1], $F^{- 1} (R^{2}) = S_{R}^{m - 1}$ and $D F (x) h = 2 ⟨ x, h ⟩$ .

2.1step 1.1algebra

If $x$ lies on the sphere, then $x \neq 0$ and $D F (x) x = 2 R^{2} \neq 0$ , so $D F (x) : R^{m} \to R$ is surjective.

3.1step 2.1L2

Thus $R^{2}$ is a regular value. By [L2], the sphere is locally a graph and $T_{x} S_{R}^{m - 1} = \ker D F (x) = x^{⊥}$ , with the same set realized by curve velocities.

4.1step 1.1∎

Negative levels are empty and hence regular by the vacuous convention; the zero level is ${0}$ and is critical because $D F (0) = 0$ . Neither boundary case is included in the positive-radius claim.

Depends on

Used by

Lagrange multipliers locate the extrema of a linear functional on a sphere Example

Dependency tree · two levels

60 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

J. M. Lee, Introduction to Smooth Manifolds, sphere example after the Regular Level Set Theorem (standard reference, not scraped)
L. W. Tu, An Introduction to Manifolds, Section 11.2 (standard reference, not scraped)