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

The map $(x, y) \mapsto (x, x y)$ has nonconstant rank on every neighbourhood of the origin

Example

For $f (x, y) = (x, x y)$ , the derivative has rank $1$ on the vertical axis and rank $2$ off it. Thus no neighbourhood of $(0, 0)$ has constant rank, although $D f$ is continuous.

Facts & Assumptions

Given: The polynomial map $f : R^{2} \to R^{2}$ , $f (x, y) = (x, x y)$ .

[L1]

The power and product rules give the continuous partial derivatives $J f (x, y) = (\begin{array}{cc} 1 & 0 \\ y & x \end{array})$ , and the continuous-partials theorem identifies this Jacobian with the total derivative (The Jacobian matrix of partial derivatives and the gradient in the scalar-valued case, 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, 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$ , If all partial derivatives exist on a neighbourhood and are continuous at a point, then the map is totally differentiable there with Jacobian derivative).

[L2]

A square matrix has rank $2$ exactly when its determinant is nonzero, while its nonzero first row gives rank at least $1$ ; every point of an open set has a ball contained in it (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 metric topology: a set is open when every one of its points has a ball around it inside the set; closed means open complement).

Verification

technique · direct

1.1

By [L1], $\det J f (x, y) = x$ . Thus [L2] gives rank $2$ when $x \neq 0$ and rank exactly $1$ when $x = 0$ .

givenL1L2algebra

1.2

Every open ball about the origin contains $(0, 0)$ and also $(ε, 0)$ for some nonzero sufficiently small $ε$ .

givenL2choose

2.1

Step 1.1 assigns different ranks to those points, so no neighbourhood of the origin has constant rank. The polynomial entries in [L1] are continuous, proving the final assertion.

step 1.1step 1.2∎

Depends on

Used by

FALSE: continuity of the derivative implies constant rank False statement

Dependency tree · two levels

41 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. M. Lee, Introduction to Smooth Manifolds, rank theorem examples (standard reference, not scraped)
L. W. Tu, An Introduction to Manifolds, Section 11.1 (standard reference, not scraped)

The map (x,y)↦(x,xy)(x,y)↦(x,xy) has nonconstant rank on every neighbourhood of the origin