False statementConstruction: Literature-sourcedVerification: AI-adaptedSession-authored (Fable 5 assisted)precheck 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.

FALSE: every injective real-differentiable planar map has nonzero Jacobian

Statement

Every injective differentiable map $F : R^{2} \to R^{2}$ has nonzero Jacobian determinant at every point.

Facts & Assumptions

Given: The map $F (x, y) = (x^{3}, y)$ , the definition of injectivity (Injection, surjection, bijection), the Jacobian-matrix convention (The Jacobian matrix of partial derivatives and the gradient in the scalar-valued case), and total differentiability from continuous partial derivatives (If all partial derivatives exist on a neighbourhood and are continuous at a point, then the map is totally differentiable there with Jacobian derivative).

[L1]

The derivative of $x \mapsto x^{3}$ is $x \mapsto 3 x^{2}$ (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).

[L2]

An injective holomorphic map on a complex domain has nowhere-zero derivative and is biholomorphic onto its open image (An injective holomorphic map has no critical point and is biholomorphic onto its image).

Refutation

technique · direct

1.1

If $F (x, y) = F (u, v)$ , then $y = v$ and $0 = x^{3} - u^{3} = (x - u) ((x + u / 2)^{2} + 3 u^{2} / 4)$ . The second factor is nonnegative and vanishes only when $x = u = 0$ , so in every case $x = u$ . Thus $F$ is injective.

givenalgebra

1.2

By [L1], the derivative matrix is $D F (x, y) = (\begin{array}{cc} 3 x^{2} & 0 \\ 0 & 1 \end{array}),$ so $F$ is differentiable and $\det D F (x, y) = 3 x^{2}$ .

L1givenalgebra

2.1

On the entire vertical axis $x = 0$ , the determinant in step 1.2 is zero even though step 1.1 shows that $F$ is injective. Hence the real-differentiable statement is false; [L2] shows the contrasting conclusion that does hold for injective holomorphic maps.

step 1.1step 1.2L2∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

30 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

B. V. Shabat, Introduction to Complex Analysis, Remark 1.11 (standard reference, not scraped)