Alphabeta Math
PropositionStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-31
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.

The tangent space of a regular level set is the kernel

Statement

Let F:M→N be smooth, let q be a regular value, and let p∈F−1(q). Then

Tp(F−1(q))=ker⁡dFp.

Facts & Assumptions

Given: A smooth map F:M→N, a regular value q, and a point p∈F−1(q).

[F1]

A regular value has only submersion points in its fibre (Regular and critical points and values).

[L1]

The fibre F−1(q) is an embedded submanifold (A regular level set is an embedded submanifold).

[L2]

Near a submersion point, suitable coordinates put F into the form (u,v)↦u (Local normal form for submersions).

[L3]

Chart maps are diffeomorphisms onto open Euclidean sets (Chart maps are diffeomorphisms onto Euclidean open sets).

[L4]

Differentials satisfy the chain rule (The chain rule for differentials of smooth maps).

Proof

technique · direct
1.1F1L1L2given

Because q is a regular value and p∈F−1(q), [F1] makes F a submersion at p. Write m:=dim⁡M, n:=dim⁡N, and ℓ:=m−n. By [L2], choose local coordinates near p and q in which the representative of F is (u,v)↦u on Rn×Rℓ, with p and q sent to the origins. Then the fibre F−1(q) is represented by the slice {0}×Rℓ. By [L1], this is the embedded-submanifold structure on the fibre near p, so its tangent vectors are exactly the vectors of the form (0,w).

2.1L3L4step 1.1

Let π(u,v)=u be the coordinate projection. Step 1.1 makes ψ∘F∘φ−1=π near the distinguished point. By [L3], the differentials dφp and dψq are isomorphisms, and [L4] gives dψq∘dFp∘d(φ−1)φ(p)=dπφ(p). Because dπφ(p) has kernel {0}×Rℓ, one gets ker⁡dFp=dφp−1({0}×Rℓ). Step 1.1 identifies the same subspace with Tp(F−1(q)), so Tp(F−1(q))=ker⁡dFp.

3.1step 1.1step 2.1∎

Therefore the intrinsic tangent space of the regular level set equals ker⁡dFp.

Depends on

Used by

Dependency tree · two levels

17 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