Alphabeta Math
False statementConstruction: Literature-sourcedVerification: AI-adaptedSession-authored (Fable 5 assisted)precheck 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)=0f'(c) = 0 then ff is not increasing on any interval containing cc

Statement

False claim: let IRI \subseteq \mathbb{R} be an interval (Intervals of R\mathbb{R}: the nine order-convex forms, nondegeneracy, and length), let f:IRf : I \to \mathbb{R} and let cIc \in I be a point at which ff is differentiable with

f(c)  =  0f'(c) \;=\; 0

(The derivative f(c)=limxcf(x)f(c)xcf'(c) = \lim_{x \to c} \frac{f(x) - f(c)}{x - c} of f:ARf : A \to \mathbb{R} at a point cAc \in A that is a limit point of AA, and differentiability on a set). Then ff is not increasing on II, in the strict sense of Nondecreasing, increasing (strictly increasing), nonincreasing, decreasing, monotone and strictly monotone real functions on a subset of R\mathbb{R}, with the dictionary to monotone sequences.

Why it is tempting. On an interval II, for ff continuous on II and differentiable at every interior point: f0f' \ge 0 throughout gives ff nondecreasing, f>0f' > 0 gives ff increasing, f0f' \le 0 and f<0f' < 0 give the two decreasing forms; conversely a nondecreasing ff has f0f' \ge 0 and a nonincreasing ff has f0f' \le 0 wherever it is differentiable, and no strict converse is claimed proves that f>0f' > 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 ff has f0f' \ge 0 wherever it is differentiable, and nothing forbids equality at isolated points.

Facts & Assumptions

Given: The interval I:=RI := \mathbb{R}, the point c:=0c := 0 and the function f:RRf : \mathbb{R} \to \mathbb{R}, f(x):=x3f(x) := x^{3} (Integer powers ama^m, Intervals of R\mathbb{R}: the nine order-convex forms, nondegeneracy, and length).

[L2]

Canonical naturals (The canonical natural ι(n)=n1F\iota(n) = n \cdot 1_F of a field, Canonical naturals are positive and strictly increasing): ι(n)>0\iota(n) > 0 for every natural n1n \ge 1, so in particular ι(3)>0\iota(3) > 0.

[L3]

Powers (Integer powers ama^m): a0=1a^{0} = 1, a2=aaa^{2} = a \cdot a, and 0a=00 \cdot a = 0, so 02=00^{2} = 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)=limxcf(x)f(c)xcf'(c) = \lim_{x \to c} \frac{f(x) - f(c)}{x - c} of f:ARf : A \to \mathbb{R} at a point cAc \in A that is a limit point of AA, and differentiability on a set): if BAB \subseteq A, if pBp \in B is a limit point of BB and if h:ARh : A \to \mathbb{R} is differentiable at pp, then hBh|_B is differentiable at pp 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\mathbb{R}); and a point pp is interior to a set SS exactly when Nε(p)SN_{\varepsilon}(p) \subseteq S for some real ε>0\varepsilon > 0 (The ε\varepsilon-neighbourhood and the punctured ε\varepsilon-neighbourhood of a point of R\mathbb{R}, Interior, closure, boundary and exterior of a subset of R\mathbb{R}).

[L9]

A positive base has positive natural powers (Monotonicity of xxnx \mapsto x^n and of nann \mapsto a^n, claim 1).

Refutation

technique · direct
1.1

By [L1] with n:=3n := 3, the function ff is differentiable at every real cc with f(c)=ι(3)c2f'(c) = \iota(3)\,c^{2}. In particular f(0)=ι(3)02=ι(3)0=0f'(0) = \iota(3) \cdot 0^{2} = \iota(3) \cdot 0 = 0 by [L3].

L1L3
1.2

For every real c0c \ne 0 one has c2>0c^{2} > 0: if c>0c > 0 this is [L9]; if c<0c < 0 then c2=ccc^{2} = c \cdot c is a product of two negative reals, hence positive by [L3] and [L4]. Therefore f(c)=ι(3)c2>0f'(c) = \iota(3)c^{2} > 0 for every c0c \ne 0, being a product of two positive reals by [L2] and [L4].

L2L3L4L9
1.3

Put I1:=(,0]I_1 := (-\infty, 0] and I2:=[0,)I_2 := [0,\infty), both order-convex with at least two elements (Intervals of R\mathbb{R}: the nine order-convex forms, nondegeneracy, and length). Every real x<0x < 0 is interior to I1I_1, since Nx(x)(,0)I1N_{|x|}(x) \subseteq (-\infty,0) \subseteq I_1; and 00 is not interior to I1I_1, since every Nε(0)N_{\varepsilon}(0) contains ε/2>0\varepsilon/2 > 0, which is not in I1I_1. As every interior point of I1I_1 lies in I1I_1 and so satisfies x0x \le 0, the interior points of I1I_1 are exactly the reals x<0x < 0. The same argument gives that the interior points of I2I_2 are exactly the reals x>0x > 0.

L4L7
2.1

By [L6] the function ff is continuous on R\mathbb{R}, hence fI1f|_{I_1} is continuous on I1I_1 and fI2f|_{I_2} is continuous on I2I_2. At every interior point xx of I1I_1 one has x<0x < 0 by step 1.3, so xx is a limit point of I1I_1 by [L7] and fI1f|_{I_1} is differentiable at xx with derivative f(x)=ι(3)x2>0f'(x) = \iota(3)x^{2} > 0 by step 1.2 and [L7]. So [L5] gives that fI1f|_{I_1} is increasing on I1I_1; the same argument on I2I_2 gives that fI2f|_{I_2} is increasing on I2I_2.

step 1.2step 1.3L5L6L7
3.1

Let a,bRa, b \in \mathbb{R} with a<ba < b. If b0b \le 0 then a,bI1a, b \in I_1 and step 2.1 gives f(a)<f(b)f(a) < f(b). If a0a \ge 0 then a,bI2a, b \in I_2 and step 2.1 gives f(a)<f(b)f(a) < f(b). Otherwise b>0b > 0 and a<0a < 0, so a,0I1a, 0 \in I_1 with a<0a < 0 gives f(a)<f(0)f(a) < f(0), while 0,bI20, b \in I_2 with 0<b0 < b gives f(0)<f(b)f(0) < f(b), and transitivity gives f(a)<f(b)f(a) < f(b). The three cases are exhaustive, since failing both b0b \le 0 and a0a \ge 0 means b>0b > 0 and a<0a < 0. So ff is increasing on R\mathbb{R} by [L8].

step 2.1L4L8
4.1

The false claim fails on this witness: R\mathbb{R} is an interval, ff is differentiable at c=0c = 0 with f(0)=0f'(0) = 0 by step 1.1, and yet ff is increasing on R\mathbb{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 · next 3 levels

Direct dependencies and their dependencies through the next three levels: 93 results over 26 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources