LemmaStatement: AI-adaptedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-13

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.

Choice-free smooth inverse function theorem in Euclidean space

Statement

In ZF, let $n \geq 1$ , let $U \subseteq R^{n}$ be open, let $f : U \to R^{n}$ be smooth, and let $a \in U$ . If $D f (a)$ is invertible, then there are open neighbourhoods $a \in V \subseteq U$ and $f (a) \in W$ such that $f ∣_{V} : V \to W$ is a diffeomorphism. Writing $g = (f ∣_{V})^{- 1}$ , $D g (y) = D f (g (y))^{- 1} (y \in W) .$ No choice axiom is used.

Facts & Assumptions

Given: The positive dimension, open set, smooth map, point, and invertible derivative in the Statement. Put $b = f (a)$ , $A = D f (a)$ , and $B = A^{- 1}$ .

[F1]

Newton maps are uniform contractions near a point with invertible derivative supplies $R > 0$ , $0 \leq q < 1$ , and $C > 0$ such that $\overline{B} (a, R) \subseteq U$ , each $T_{y} (x) = x + B (y - f (x))$ is $q$ -Lipschitz there, every $D f (x)$ there is invertible, $∥ B v ∥_{2} \leq C ∥ v ∥_{2}$ , and $∥ D f (x)^{- 1} v ∥_{2} \leq C (1 - q)^{- 1} ∥ v ∥_{2}$ .

[F2]

$R$ and $R^{n}$ for $n \geq 1$ with the Euclidean metric are complete, componentwise from the Cauchy criterion in $R$ makes $R^{n}$ complete, and A contraction of a nonempty complete metric space into itself has exactly one fixed point, the limit of the iterates from any starting point gives the unique fixed point of a specified self-contraction of a nonempty complete metric space by its recursively specified iterates.

[F3]

Total differentiability is the linear expansion with $o (∥ h ∥_{2})$ remainder, and it implies continuity (The total (Fréchet) derivative $D f (a)$ as the linear first-order approximation with $o (∥ h ∥_{2})$ remainder, Total differentiability gives a local $O (∥ h ∥_{2})$ increment bound and therefore continuity).

[F4]

Smooth Euclidean maps and diffeomorphisms have the meaning in $C^{k}$ Euclidean maps and diffeomorphisms. Finite componentwise algebra and composition preserve $C^{r}$ regularity, and inversion of a matrix-valued $C^{r}$ map preserves that regularity on the invertible locus ( $C^{k}$ Euclidean maps are closed under componentwise algebra and composition, Matrix inversion preserves $C^{k}$ regularity where the determinant is nonzero).

[F5]

Invertibility and a local $C^{1}$ inverse have the meanings in Invertible Euclidean linear maps and Continuously differentiable maps, local inverses, and local diffeomorphisms; derivatives obey the chain rule (The chain rule for total derivatives: $D (g \circ f) (a) = D g (f (a)) \circ D f (a)$ ).

Proof

technique · contraction

1.1

Take $R, q, C$ from [F1] and choose the explicit positive number $δ = (1 - q) R / (2 C)$ . Put $W = B (b, δ)$ . For $y \in W$ and $x \in \overline{B} (a, R)$ , $∥ T_{y} (x) - a ∥_{2} \leq ∥ T_{y} (x) - T_{y} (a) ∥_{2} + ∥ B (y - b) ∥_{2} \leq q R + C δ = (1 + q) R / 2 < R .$ Thus $T_{y}$ maps the closed ball strictly into its open interior.

F1algebra

1.2

The closed ball is complete without choice. Indeed, a Cauchy sequence $(x_{k})$ in it is Cauchy in $R^{n}$ , so [F2] gives its unique limit $x$ . The triangle inequality yields $∥ x - a ∥_{2} \leq ∥ x - x_{k} ∥_{2} + R$ for every $k$ ; if $∥ x - a ∥_{2} > R$ , choosing $k$ with $∥ x - x_{k} ∥_{2} < ∥ x - a ∥_{2} - R$ is a contradiction. Hence $x$ remains in the ball. The ball is nonempty because it contains $a$ .

2.1

For each fixed $y \in W$ , [F1], step 1.1, step 1.2, and [F2] give a unique fixed point $g (y) \in \overline{B} (a, R)$ . This defines a function without a choice axiom: $g (y)$ is the unique object satisfying the displayed fixed-point property. Its equation is $B (y - f (g (y))) = 0$ , hence $f (g (y)) = y$ because $B$ is injective; step 1.1 puts $g (y)$ in $B (a, R)$ .

F1F2F5step 1.1step 1.2

3.1

If $x, z \in \overline{B} (a, R)$ and $f (x) = f (z) = y$ , then $T_{y} (x) = x$ and $T_{y} (z) = z$ , so [F1] gives $∥ x - z ∥_{2} \leq q ∥ x - z ∥_{2}$ and therefore $x = z$ . Define $V = B (a, R) \cap f^{- 1} [W]$ . By [F3], $V$ is open; it contains $a$ , lies in $U$ , and step 2.1 together with injectivity shows that $f ∣_{V} : V \to W$ is bijective with inverse $g$ .

F1F3step 2.1

3.2

For $y, z \in W$ , the fixed-point equations and [F1] give $∥ g (y) - g (z) ∥_{2} \leq q ∥ g (y) - g (z) ∥_{2} + C ∥ y - z ∥_{2},$ so $∥ g (y) - g (z) ∥_{2} \leq C (1 - q)^{- 1} ∥ y - z ∥_{2}$ . Thus $g$ is Lipschitz and continuous.

F1step 2.1algebra

4.1

Fix $y \in W$ , put $x = g (y)$ and $L = D f (x)$ . For small $h$ with $y + h \in W$ , put $k = g (y + h) - x$ . Step 3.2 gives $∥ k ∥_{2} = O (∥ h ∥_{2})$ , while [F3] and $f (g (y + h)) - f (g (y)) = h$ give $h = L k + r (k)$ with $∥ r (k) ∥_{2} = o (∥ k ∥_{2})$ . The inverse bound in [F1] therefore gives $k = L^{- 1} h - L^{- 1} r (k) = L^{- 1} h + o (∥ h ∥_{2})$ , including the case $k = 0$ . Hence $D g (y) = D f (g (y))^{- 1}$ . The chain rule in [F5] also gives $D f (g (y)) D g (y) = I$ from $f \circ g = {id}_{W}$ , consistently with this formula.

F1F3F5step 2.1step 3.2

5.1

The map $g$ is $C^{1}$ : it is continuous by step 3.2, $D f \circ g$ is continuous, and [F4] makes its inverse matrix $D g$ continuous. Inductively, suppose $g$ is $C^{r}$ for some $r \geq 1$ . Because $f$ is smooth, the matrix entries of $D f$ are $C^{r}$ ; [F4] makes $D f \circ g$ and then $(D f \circ g)^{- 1} = D g$ of class $C^{r}$ . Thus the first partial derivatives of $g$ are $C^{r}$ , so [F4] makes $g$ of class $C^{r + 1}$ . Induction proves $g$ is smooth, and [F4] and step 3.1 make $f ∣_{V}$ a diffeomorphism.

F4step 3.1step 3.2step 4.1induction

6.1

The hypothesis $n \geq 1$ excludes the zero-dimensional Euclidean convention; dimension one is included verbatim. The datum $a \in U$ makes the empty-domain case impossible. Invertibility excludes a degenerate derivative, while zero increments are covered in step 4.1. All domains are open, and the closed ball is used only as the complete space for iteration, so no boundary point is asserted to lie in $V$ . The construction chooses explicit $δ$ , starts every Newton iteration at the specified point $a$ , and defines each value by uniqueness; finite induction on derivative order and unique Euclidean limits use no choice axiom.

F1F2F4step 1.1step 1.2step 2.1step 4.1step 5.1∎

Depends on

Used by

Existence of geodesically convex neighborhoods Theorem
Existence of normal neighborhoods Theorem

Dependency tree · two levels

63 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. Lebl, Basic Analysis II, Theorem 8.5.1 and higher-regularity discussion (standard reference, not scraped)