Alphabeta Math
CorollaryStatement: AI-adaptedProof: AI-adaptedprecheck 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.

A regular level set is locally a Ck graph of dimension m−n

Statement

Let f:U⊆Rm→Rn be Ck, k≥1, and let c be a regular value. Near each point, a regular level set is a Ck graph over ker⁡Df(a) of dimension m−n.

More precisely, for a∈f−1(c) put K=ker⁡Df(a) and E=K⊥, so Rm=K⊕E. There are neighbourhoods P⊆K of 0 and Q⊆E of 0 and a Ck map g:P→Q with g(0)=0 and Dg(0)=0 such that, near a, f−1(c)={a+u+g(u):u∈P}. The empty fibre satisfies the regular-value convention vacuously, and when m=n the local graph has zero-dimensional domain and is the isolated point a.

Facts & Assumptions

Given: The stated map, regular value c, and a point a∈f−1(c).

[L1]

Surjectivity of Df(a) persists nearby, and a constant-rank level is locally a coordinate slice (Regular and critical points, regular and critical values, and level sets, Differential rank is lower semicontinuous, A constant-rank level set is locally a coordinate slice).

[L2]

If K is a subspace of the finite-dimensional Euclidean inner-product space Rm, then Rm=K⊕K⊥; rank-nullity gives dim⁡K=m−n, and the inverse function theorem turns an invertible derivative into a local C1 diffeomorphism whose inverse is Ck when the original map is Ck (For a subspace W of a finite-dimensional inner product space, V=W⊕W⊥, Rank-nullity: dim⁡FV=nullity⁡T+rank⁡T, The Euclidean inverse function theorem, A local inverse of a Ck regular map is Ck).

Proof

technique · direct
1.1givenL1L2construct

By [L1], f has constant rank n near a, and its fibre is a Ck coordinate slice. By [L2], put E=K⊥, so Rm=K⊕E and dim⁡K=m−n.

2.1step 1.1L2algebra

The projection of that slice to K along E has derivative equal to the identity at a: its tangent there is K, because differentiating the normal-form slice and undoing the source coordinates gives ker⁡Df(a). By [L2], this projection is a local Ck diffeomorphism.

3.1step 2.1algebra

Inverting the projection writes the slice uniquely as a+u+g(u). Its derivative at 0 takes values both in E and in the tangent K, so Dg(0)=0; the zero-dimensional case is the same statement with P={0}.

4.1step 3.1∎

This gives the asserted graph and dimension at every point of a nonempty regular fibre, while the empty-fibre case is vacuous.

Depends on

Dependency tree · 2 levels

Sources