Session-authored (Fable 5 assisted)

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.

✓ 3 results · all verified · 0 also independently AI-judged

Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs. The 3 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.

The Inverse and Implicit Function Theorems: Examples and Counterexamples

1 · Prerequisites

2 · Summary

3 · Logical flowchart

4 · Definitions, theorems and proofs

None yet.

5 · Examples, counterexamples and false statements

ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passaudited 2026-08-03Open item page →

The unit circle is locally a $C^{1}$ graph at every point

Example

At every point $(a, b)$ of the unit circle $a^{2} + b^{2} = 1$ , the circle is locally the graph of a $C^{1}$ function of one coordinate.

Facts & Assumptions

Given: No hypotheses beyond those quantified in the statement.

[L1]

On an open domain, a $C^{1}$ map satisfying $F (a, b) = 0$ can be solved locally for the second block when $D_{y} F (a, b)$ is invertible (The Euclidean implicit function theorem with derivative formula).

[L2]

Direct difference quotients give $\partial_{x} F (x, y) = 2 x$ and $\partial_{y} F (x, y) = 2 y$ ; their displayed affine formulas are continuous. Thus the continuous-partials theorem gives $D F (x, y) (u, v) = 2 x u + 2 y v$ , and $F$ 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, For a natural $n \geq 1$ the function $x \mapsto x^{n}$ is differentiable everywhere with derivative $ι (n) x^{n - 1}$ ; for $n = 0$ it is the constant $1$ , with derivative $0$ ; for a natural $n \geq 1$ the function $x \mapsto x^{- n}$ is differentiable at every $x \neq 0$ with derivative $- ι (n) x^{- n - 1}$ ; consequently every polynomial function is differentiable at every real, with the derivative computed term by term).

Proof

technique · direct

1.1

Let $F (x, y) : = x^{2} + y^{2} - 1$ . Then [L2] gives $D F (x, y) (u, v) = 2 x u + 2 y v$ . At a point $(a, b)$ on the circle, at least one of $a, b$ is nonzero.

L2givenalgebra

2.1

If $b \neq 0$ , then $D_{y} F (a, b)$ is multiplication by $2 b$ and is invertible, so [L1] expresses the circle locally as $y = φ (x)$ . If $a \neq 0$ , exchange the coordinate blocks and obtain $x = ψ (y)$ . These alternatives cover every circle point by step 1.1.

step 1.1L1cases∎

CounterexampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passaudited 2026-08-03Open item page →

The real complex-squaring map is locally but not globally invertible off the origin

Example

For

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

$D S (x, y)$ is invertible exactly when $(x, y) \neq (0, 0)$ , so $S$ is locally invertible off the origin. Nevertheless $S (x, y) = S (- x, - y)$ , and every nonzero target in $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} \geq 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 $(2 x, - 2 y)$ and $(2 y, 2 x)$ ; 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 $D S (x, y) (u, v) = (2 x u - 2 y v, 2 y u + 2 x v) .$ The domain $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) ⟼ (\frac{x p + y q}{2 r^{2}}, \frac{- y p + x q}{2 r^{2}}) .$ 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) \neq (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}, y^{2} = \frac{r - u}{2}, 2 x y = v .$ The square equations and the sign condition $2 x y = 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∎

CounterexampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passaudited 2026-08-03Open item page →

An invertible derivative at one point does not give a local inverse without $C^{1}$ regularity

Example

Define

$f (x) : = {\begin{cases} x + 2 x^{2} \sin (1 / x), & x \neq 0, \\ 0, & x = 0. \end{cases}$

Then $f$ is differentiable at $0$ with $f^{'} (0) = 1$ , but it is injective on no neighbourhood of $0$ . Its derivative is not continuous at $0$ , so this does not contradict the $C^{1}$ inverse function theorem.

Facts & Assumptions

Given: No hypotheses beyond those quantified in the statement.

[L1]

Derivatives obey the algebra and chain rules; the power rule gives the derivatives of $x$ , $x^{2}$ , and $x^{- 1}$ on its nonzero domain; and $(\sin x)^{'} = \cos x$ (Sums, scalar multiples, products and quotients: $(f + g)^{'} (c) = f^{'} (c) + g^{'} (c)$ , $(α f)^{'} (c) = α f^{'} (c)$ , $(f g)^{'} (c) = f^{'} (c) g (c) + f (c) g^{'} (c)$ , and $(f / g)^{'} (c) = (f^{'} (c) g (c) - f (c) g^{'} (c)) / g (c)^{2}$ when $g (c) \neq 0$ , The chain rule, in one line from Carathéodory: if $g$ is differentiable at $c$ and $f$ is differentiable at $g (c)$ , then $f \circ g$ is differentiable at $c$ with $(f \circ g)^{'} (c) = f^{'} (g (c)) g^{'} (c)$ , For a natural $n \geq 1$ the function $x \mapsto x^{n}$ is differentiable everywhere with derivative $ι (n) x^{n - 1}$ ; for $n = 0$ it is the constant $1$ , with derivative $0$ ; for a natural $n \geq 1$ the function $x \mapsto x^{- n}$ is differentiable at every $x \neq 0$ with derivative $- ι (n) x^{- n - 1}$ ; consequently every polynomial function is differentiable at every real, with the derivative computed term by term, The derivatives of sine and cosine are cosine and minus sine).

[L2]

Sine and cosine have the integer-multiple values determined by their zero sets, periods, and quarter-turn values (The zero sets of sine and cosine and the least positive common period 2 pi, Quarter-turn values and shifts by pi/2 and pi).

[L3]

Differentiability implies continuity, and a continuous injective real function on an interval is strictly monotone (A function differentiable at $c$ is continuous at $c$ , Continuous inverse theorem: a continuous injective $f$ on an interval $I$ is a bijection onto the order-convex set $f [I]$ , and the inverse $g : f [I] \to I$ is continuous and strictly monotone in the same sense as $f$ ).

[L4]

Sine is bounded by $1$ in absolute value (Signs, monotonicity intervals, and ranges of sine and cosine).

[L5]

A derivative is the limit of the relative difference quotient (The derivative $f^{'} (c) = \lim_{x \to c} \frac{f (x) - f (c)}{x - c}$ of $f : A \to R$ at a point $c \in A$ that is a limit point of $A$ , and differentiability on a set).

Proof

technique · contradiction

1.1

At zero, $\frac{f (h) - f (0)}{h} = 1 + 2 h \sin (1 / h) ⟶ 1,$ because sine is bounded. Thus $f^{'} (0) = 1$ . For $x \neq 0$ , [L1] gives $f^{'} (x) = 1 + 4 x \sin (1 / x) - 2 \cos (1 / x) .$

L1L4L5algebra

2.1

For $n \geq 1$ , put $x_{n} : = 1 / (2 π n)$ and $y_{n} : = 1 / ((2 n + 1) π)$ . Both sequences tend to zero; [L2] gives $\sin (1 / x_{n}) = \sin (1 / y_{n}) = 0$ , $\cos (1 / x_{n}) = 1$ , and $\cos (1 / y_{n}) = - 1$ . Thus step 1.1 gives $f^{'} (x_{n}) = - 1$ and $f^{'} (y_{n}) = 3$ , so $f^{'}$ is not continuous at zero.

step 1.1L2

3.1

Suppose $f$ were injective on an open interval about zero. It is continuous there because it is differentiable, so [L3] would make it strictly increasing or strictly decreasing. At every differentiability point an increasing function has nonnegative derivative, while a decreasing function has nonpositive derivative, directly from the signs of its difference quotients. Step 2.1 supplies both a negative and a positive derivative in every such interval, a contradiction.

assume-contrastep 2.1L3L5

4.1

Thus no neighbourhood gives injectivity; step 2.1 also identifies the failure of the $C^{1}$ hypothesis.

step 2.1step 3.1L4discharge-contradiction∎

Sources

Standard references

Recommended treatments; not extraction sources.

The Inverse and Implicit Function Theorems: Examples and Counterexamples

1 · Prerequisites

2 · Summary

3 · Logical flowchart

4 · Definitions, theorems and proofs

5 · Examples, counterexamples and false statements

The unit circle is locally a C1C1 graph at every point

Example

Facts & Assumptions

Proof

The real complex-squaring map is locally but not globally invertible off the origin

Example

Facts & Assumptions

Proof

An invertible derivative at one point does not give a local inverse without C1C1 regularity

Example

Facts & Assumptions

Proof

Sources

Standard references

The unit circle is locally a $C^{1}$ graph at every point

An invertible derivative at one point does not give a local inverse without $C^{1}$ regularity