Alphabeta Math
False statementConstruction: 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.

FALSE: if f′(c)=0 then f is not increasing on any interval containing c

Statement

False claim: let I⊆R be an interval (Intervals of R: the nine order-convex forms, nondegeneracy, and length), let f:I→R and let c∈I be a point at which f is differentiable with

f′(c)  =  0

(The derivative f′(c)=lim⁡x→cf(x)−f(c)x−c of f:A→R at a point c∈A that is a limit point of A, and differentiability on a set). Then f is not increasing on I, 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.

Why it is tempting. 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 proves that f′>0 at every interior point gives an increasing function, and one reads the implication backwards: if strict increase comes from a strictly positive derivative, surely a derivative that fails to be strictly positive somewhere must destroy the strict increase there. It does not. Claim 5 of that theorem is the true converse, and it is non-strict: an increasing f has f′≥0 wherever it is differentiable, and nothing forbids equality at isolated points.

Facts & Assumptions

Given: The interval I:=R, the point c:=0 and the function f:R→R, f(x):=x3 (Integer powers am, Intervals of R: the nine order-convex forms, nondegeneracy, and length).

[L2]

Canonical naturals (The canonical natural ι(n)=n⋅1F of a field, Canonical naturals are positive and strictly increasing): ι(n)>0 for every natural n≥1, so in particular ι(3)>0.

[L3]

Powers (Integer powers am): a0=1, a2=a⋅a, and 0⋅a=0, so 02=0.

[L4]

Order arithmetic (Sign rules for products and monotonicity of multiplication, Ordered field): a product of two positive reals is positive and a product of two negative reals is positive; the order is total and transitive, and trichotomy holds.

[L7]

Restriction of the derivative (The derivative f′(c)=lim⁡x→cf(x)−f(c)x−c of f:A→R at a point c∈A that is a limit point of A, and differentiability on a set): if B⊆A, if p∈B is a limit point of B and if h:A→R is differentiable at p, then h∣B is differentiable at p with the same derivative; every point of an order-convex set with at least two elements is a limit point of it (Limit point, isolated point, adherent point, derived set, and dense subset of R); and a point p is interior to a set S exactly when Nε(p)⊆S for some real ε>0 (The ε-neighbourhood and the punctured ε-neighbourhood of a point of R, Interior, closure, boundary and exterior of a subset of R).

[L9]

A positive base has positive natural powers (Monotonicity of x↦xn and of n↦an, claim 1).

Refutation

technique · direct
1.1

By [L1] with n:=3, the function f is differentiable at every real c with f′(c)=ι(3) c2. In particular f′(0)=ι(3)⋅02=ι(3)⋅0=0 by [L3].

L1L3
1.2

For every real c≠0 one has c2>0: if c>0 this is [L9]; if c<0 then c2=c⋅c is a product of two negative reals, hence positive by [L3] and [L4]. Therefore f′(c)=ι(3)c2>0 for every c≠0, being a product of two positive reals by [L2] and [L4].

L2L3L4L9
1.3

Put I1:=(−∞,0] and I2:=[0,∞), both order-convex with at least two elements (Intervals of R: the nine order-convex forms, nondegeneracy, and length). Every real x<0 is interior to I1, since N∣x∣(x)⊆(−∞,0)⊆I1; and 0 is not interior to I1, since every Nε(0) contains ε/2>0, which is not in I1. As every interior point of I1 lies in I1 and so satisfies x≤0, the interior points of I1 are exactly the reals x<0. The same argument gives that the interior points of I2 are exactly the reals x>0.

L4L7
2.1

By [L6] the function f is continuous on R, hence f∣I1 is continuous on I1 and f∣I2 is continuous on I2. At every interior point x of I1 one has x<0 by step 1.3, so x is a limit point of I1 by [L7] and f∣I1 is differentiable at x with derivative f′(x)=ι(3)x2>0 by step 1.2 and [L7]. So [L5] gives that f∣I1 is increasing on I1; the same argument on I2 gives that f∣I2 is increasing on I2.

step 1.2step 1.3L5L6L7
3.1

Let a,b∈R with a<b. If b≤0 then a,b∈I1 and step 2.1 gives f(a)<f(b). If a≥0 then a,b∈I2 and step 2.1 gives f(a)<f(b). Otherwise b>0 and a<0, so a,0∈I1 with a<0 gives f(a)<f(0), while 0,b∈I2 with 0<b gives f(0)<f(b), and transitivity gives f(a)<f(b). The three cases are exhaustive, since failing both b≤0 and a≥0 means b>0 and a<0. So f is increasing on R by [L8].

step 2.1L4L8
4.1

The false claim fails on this witness: R is an interval, f is differentiable at c=0 with f′(0)=0 by step 1.1, and yet f is increasing on R by step 3.1. So a vanishing derivative forbids nothing of the kind, and the claim is false.

step 1.1step 3.1∎

Remarks

Depends on

Used by

Dependency tree · two levels

61 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