Alphabeta Math
ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-28
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.

x↦x3 is increasing on R although its derivative vanishes at 0, which is the witness for the false statement that a vanishing derivative forbids strict increase, and which makes its inverse non-differentiable at 0

Example

Let f:R→R be f(x)=x3 (Integer powers am), with ι the canonical natural of The canonical natural ι(n)=n⋅1F of a field.

Claim 1. f is differentiable at every c∈R with f′(c)=ι(3)c2, and f′(0)=0.

Claim 2. f is increasing on R, in the strict sense of Nondecreasing, increasing (strictly increasing), nonincreasing, decreasing, monotone and strictly monotone real functions on a subset of R, with the dictionary to monotone sequences.

Claim 3. So the hypothesis "f′>0 at every interior point" of claim 2 of On an interval I, for f continuous on I and differentiable at every interior point: f′≥0 throughout gives f nondecreasing, f′>0 gives f increasing, f′≤0 and f′<0 give the two decreasing forms; conversely a nondecreasing f has f′≥0 and a nonincreasing f has f′≤0 wherever it is differentiable, and no strict converse is claimed is sufficient but not necessary for a function on an interval to be increasing; and the converse recorded there, claim 5, which gives only f′≥0, cannot be strengthened to f′>0.

Claim 4. f is continuous and injective on R, so it has a continuous inverse g on f[R] (Derivative of an inverse: if f is continuous and injective on a nondegenerate interval I and differentiable at c∈I with f′(c)≠0, then the inverse g is differentiable at f(c) with g′(f(c))=1/f′(c); and if f′(c)=0 then g is not differentiable at f(c)); and since f′(0)=0, that inverse is not differentiable at f(0)=0.

Claims 1 and 2 are established in the refutation of FALSE: if f′(c)=0 then f is not increasing on any interval containing c and are quoted here; claims 3 and 4 are the two consequences worth drawing from them.

Facts & Assumptions

Given: The function f:R→R, f(x)=x3.

[L5]

Derivative of an inverse (Derivative of an inverse: if f is continuous and injective on a nondegenerate interval I and differentiable at c∈I with f′(c)≠0, then the inverse g is differentiable at f(c) with g′(f(c))=1/f′(c); and if f′(c)=0 then g is not differentiable at f(c)): for I order-convex with at least two elements and f:I→R continuous and injective, with inverse g:f[I]→I, and for c∈I at which f is differentiable, if f′(c)=0 then g is not differentiable at f(c).

[L7]

03=0, since 0n=0 for every natural n≥1 (Integer powers am).

Verification

technique · direct
1.1

Claims 1 and 2. By [L1] the function f is differentiable at every c∈R with f′(c)=ι(3)c2, its derivative at 0 is 0, and f is increasing on R.

L1
2.1

f is injective by [L2], being increasing; it is continuous on R by [L3]; and R is order-convex with at least two elements by [L4]. So f satisfies every hypothesis of [L5] with I:=R.

step 1.1L2L3L4L5
2.2

Claim 3. The hypothesis of claim 2 of [L6] fails for f on R, since f′(0)=0 is not positive, and yet the conclusion holds, f being increasing on R by step 1.1. So that hypothesis is sufficient and not necessary. Likewise the conclusion f′≥0 of claim 5 of [L6] is attained with equality at 0 by step 1.1, so it cannot be strengthened to f′>0.

step 1.1L6
3.1

Claim 4. By step 2.1 the hypotheses of [L5] hold, and by step 1.1 the function f is differentiable at 0 with f′(0)=0. So [L5] gives that the inverse g:f[R]→R is not differentiable at f(0), which is 0 by [L7].

step 1.1step 2.1L5L7
4.1

All four claims are verified: claims 1 and 2 by step 1.1, claim 3 by step 2.2 and claim 4 by step 3.1.

step 1.1step 2.2step 3.1∎

Remarks

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

59 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