CounterexampleConstruction: Literature-sourcedVerification: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-03

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 real complex-squaring map is locally but not globally invertible off the origin

Example

For

$S(x,y):=(x^2-y^2,2xy),$

$DS(x,y)$ is invertible exactly when $(x,y)\ne(0,0)$ , so $S$ is locally invertible off the origin. Nevertheless $S(x,y)=S(-x,-y)$ , and every nonzero target in $\mathbb R^2$ has exactly two preimages. Thus the inverse function theorem is irreducibly local. At the origin the derivative is not invertible, and zero has only one preimage.

Facts & Assumptions

Given: No hypotheses beyond those quantified in the statement.

[L1]

A $C^1$ map on an open Euclidean domain with an invertible derivative has a local $C^1$ inverse (The Euclidean inverse function theorem).

[L2]

Invertibility means the existence of a two-sided linear inverse (Invertible Euclidean linear maps).

[L3]

Nonnegative reals have unique nonnegative square roots (Square roots exist: a unique $\sqrt{a} \ge 0$ with $(\sqrt{a})^2 = a$ ; the positives are $\{x^2 : x \neq 0\}$ ).

[L4]

Direct difference quotients give the two coordinate partial-derivative rows $(2x,-2y)$ and $(2y,2x)$ ; these affine entries are continuous. Thus the continuous-partials theorem gives the displayed total derivative, and $S$ is $C^1$ (If all partial derivatives exist on a neighbourhood and are continuous at a point, then the map is totally differentiable there with Jacobian derivative, Continuously differentiable maps, local inverses, and local diffeomorphisms).

[L5]

A metric space is open in itself (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.1

The total derivative is $DS(x,y)(u,v)=(2xu-2yv,2yu+2xv).$ The domain $\mathbb R^2$ is open by [L5], and [L4] makes $S$ $C^1$ . If $r^2:=x^2+y^2>0$ , its inverse is $(p,q)\longmapsto \left(\frac{xp+yq}{2r^2},\frac{-yp+xq}{2r^2}\right).$ Direct substitution verifies both inverse identities, so [L1] gives local invertibility at every nonzero point. At $(0,0)$ the derivative is the zero map; moreover every ball about the origin contains distinct $(t,0)$ and $(-t,0)$ with the same image, so no local inverse exists there.

L1L2L4L5algebra

1.2

If $S(x,y)=(u,v)$ , then $(x^2+y^2)^2=u^2+v^2.$ For $(u,v)\ne(0,0)$ , [L3] therefore fixes the positive value $r:=x^2+y^2=\sqrt{u^2+v^2}$ , and $x^2=\frac{r+u}{2},\qquad y^2=\frac{r-u}{2},\qquad 2xy=v.$ The square equations and the sign condition $2xy=v$ leave exactly one pair $(x,y)$ up to simultaneous negation. Thus there are exactly two preimages.

L3algebra

2.1

For the zero target, the identity in step 1.2 forces $x^2+y^2=0$ , hence $(x,y)=(0,0)$ .

step 1.2L3algebra

3.1

Steps 1.1--2.1 establish every local, global, and origin qualification in the example.

step 1.1step 1.2step 2.1∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 107 results over 23 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources

J. Lebl, Basic Analysis II, §8.5 exercises on local versus global invertibility (standard reference, not scraped)