DefinitionDefinition: Literature-sourcedProof: Not applicablejudge 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.

Regular and critical points, regular and critical values, and level sets

Let $m, n \geq 1$ , let $U \subseteq R^{m}$ be open, and let $f : U \to R^{n}$ be $C^{1}$ .

A point $a \in U$ is a regular point of $f$ when $f$ is a submersion at $a$ , and a critical point otherwise (Submersions and immersions between Euclidean open sets).
A value $c \in R^{n}$ is a regular value when every $a \in f^{- 1} ({c})$ is a regular point. A value that is not regular is a critical value. In particular every value outside $f [U]$ is regular by vacuous truth.
The level set or fibre over $c$ is $f^{- 1} (c) : = {x \in U : f (x) = c}$ .

Regularity is a condition on the derivative at points of the fibre, not a claim that the fibre is nonempty.

Depends on