TheoremStatement: Literature-sourcedProof: 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.

Differential rank is lower semicontinuous

Statement

Let $f : U \subseteq R^{m} \to R^{n}$ be $C^{1}$ on an open set. For every natural $r$ , the locus $U_{\geq r} : = {x \in U : rank D f (x) \geq r}$ is open. Thus $x \mapsto rank D f (x)$ is lower semicontinuous. In particular the submersion locus, the immersion locus, and every locus on which the derivative has the largest possible rank are open.

Facts & Assumptions

Given: A $C^{1}$ map $f : U \subseteq R^{m} \to R^{n}$ and a natural number $r$ .

[L1]

For $1 \leq r \leq \min {m, n}$ , a matrix has rank at least $r$ exactly when it has a nonzero $r$ -rowed minor (A matrix has rank at least $r$ exactly when it has a nonzero $r$ -rowed minor, The rank of a derivative and constant-rank Euclidean maps, The Jacobian matrix of partial derivatives and the gradient in the scalar-valued case).

[L2]

Each fixed-size determinant is a polynomial in the matrix entries, while the first partial derivatives of a $C^{1}$ map are continuous; sums, products, and composites of continuous Euclidean maps are continuous, and the empty set and whole metric space are open (For every fixed finite size at least one, the determinant of a real square matrix is a polynomial in its matrix entries, $C^{k}$ Euclidean maps and diffeomorphisms, $C^{k}$ Euclidean maps are closed under componentwise algebra and composition, The metric topology: a set is open when every one of its points has a ball around it inside the set; closed means open complement).

Proof

technique · direct

1.1givenL2

If $r = 0$ , then $U_{\geq r} = U$ ; if $r > \min {m, n}$ , then $U_{\geq r} = \emptyset$ . Both sets are open.

1.2givenL1choose

Assume $1 \leq r \leq \min {m, n}$ and fix $a \in U_{\geq r}$ . By [L1], one $r$ -rowed minor $M (a)$ of $J f (a)$ is nonzero.

2.1step 1.2L1L2

By [L2], the same minor $M (x)$ is a continuous scalar function of $x$ . Its nonzero locus contains an open neighbourhood $V$ of $a$ , and [L1] gives $V \subseteq U_{\geq r}$ .

3.1step 1.1step 2.1∎

Every point of $U_{\geq r}$ therefore has an open neighbourhood inside it, and the two exceptional cases were settled in step 1.1. Hence $U_{\geq r}$ is open for every $r$ , proving all stated consequences.

Differential rank is lower semicontinuous

Statement

Facts & Assumptions

Proof

Depends on

Dependency tree · 2 levels

Sources