False statementConstruction: Literature-sourcedVerification: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 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.

FALSE: every level set of a smooth map is locally a graph

Statement

Every level set of a smooth Euclidean map is locally a $C^{1}$ graph.

Facts & Assumptions

Given: The smooth map $F (x, y, z) = x^{2} + y^{2} - z^{2}$ .

[L1]

The power rule and derivative algebra give the continuous Jacobian row $(2 x, 2 y, - 2 z)$ , the continuous-partials theorem identifies it with $D F$ , and polynomial coordinate expressions are smooth (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, $C^{k}$ Euclidean maps are closed under componentwise algebra and composition).

[L2]

The regular-level graph theorem assumes surjectivity of the derivative at every point of the fibre (Regular and critical points, regular and critical values, and level sets, A regular level set is locally a $C^{k}$ graph of dimension $m - n$ ).

Refutation

technique · direct

1.1

The zero level is the double cone $x^{2} + y^{2} = z^{2}$ , and [L1] gives $D F (0, 0, 0) = 0$ , so the apex is critical and [L2] does not apply there.

givenL1L2

1.2

The cone contains rays from the apex in the linearly independent directions $(1, 0, 1)$ , $(1, 0, - 1)$ , and $(0, 1, 1)$ . If it were a $C^{1}$ graph near the apex, all these curve velocities would lie in its single two-dimensional tangent plane, which is impossible.

givenalgebra

2.1

Thus this smooth polynomial has a level set that is not locally a $C^{1}$ graph at the apex, refuting the statement.

step 1.1step 1.2∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

41 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, Regular Level Set Theorem and examples (standard reference, not scraped)
L. W. Tu, An Introduction to Manifolds, Section 11.2 (standard reference, not scraped)