Alphabeta Math
CounterexampleConstruction: AI-adaptedVerification: AI-generatedprecheck passverified 2026-08-09 (gpt-5.6-terra-codex-subscription)
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↦x on (0,1] is differentiable with unbounded derivative and is not Lipschitz there, so the boundedness hypothesis in the Lipschitz corollary cannot be dropped

Statement refuted

Facts & Assumptions

Given: The set I:=(0,1], order-convex with at least two elements (Intervals of R: the nine order-convex forms, nondegeneracy, and length), and the function s:I→R, s(b):=b1/2, the nonnegative square root (Existence and uniqueness of n-th roots: a unique a1/n≥0 with (a1/n)n=a, Rational powers ar of a positive base); numerals denote canonical naturals (The canonical natural ι(n)=n⋅1F of a field).

[L2]

A function differentiable at a point is continuous there (A function differentiable at c is continuous at c).

[L3]

Uniqueness of the nonnegative square root (Existence and uniqueness of n-th roots: a unique a1/n≥0 with (a1/n)n=a): for a≥0 there is exactly one t≥0 with t2=a, and it is a1/2 (Rational powers ar of a positive base, Integer powers am).

[L4]

Rational powers (Laws of rational exponents, Monotonicity of r↦ar and of a↦ar): ar>0 for a>0; a−r=1/ar; (ar)s=ars; and for rational r>0, 0<a<b implies ar<br (claim 2 of the monotonicity lemma).

[L5]

Archimedean property in reciprocal form (For every ε>0 in a complete ordered field there is a natural n≥1 with 1/n<ε, Every complete ordered field is Archimedean): for every real ε>0 there is a natural m≥1 with 1/ι(m)<ε.

[L6]

Order and numeral arithmetic (Inverses of positives are positive, and reciprocation reverses order, Sign rules for products and monotonicity of multiplication, Multiplying inequalities of positives, Canonical naturals are positive and strictly increasing, Monotonicity of x↦xn and of n↦an, Basic properties of the absolute value, The canonical natural ι(n)=n⋅1F of a field): ι(m)>0 for m≥1; 0<a<b gives 0<1/b<1/a (Inverses of positives are positive, and reciprocation reverses order); a product of positives is positive and multiplying a STRICT inequality by a positive real preserves it (Sign rules for products and monotonicity of multiplication); the NONSTRICT form, 0≤x≤y and 0≤u≤v imply xu≤yv, is not stated by Sign rules for products and monotonicity of multiplication, whose multiplicative claims are strict, but by Multiplying inequalities of positives, and it is what licenses both multiplying a ≤ by a positive real and dividing a ≤ by one, the divisor entering as its positive inverse; 0≤a≤b gives a2≤b2 (Monotonicity of x↦xn and of n↦an, claim 2); ∣u∣=u for u≥0 (Basic properties of the absolute value); and ι(mn)=ι(m)ι(n) and ι(m+n)=ι(m)+ι(n) for naturals m,n≥1, so ι(2)2=ι(4), ι(2)−1=1 and ι(4)−1=ι(3).

[L7]

Interiority and boundedness (Interior, closure, boundary and exterior of a subset of R, The ε-neighbourhood and the punctured ε-neighbourhood of a point of R, Lower bound, bounded below, bounded set): p is interior to S exactly when Nε(p)⊆S for some real ε>0; and a set of reals is bounded above when some real exceeds or equals all of its elements.

Counterexample

technique · direct
1.1

By [L1] the function s is differentiable at every b∈I with s′(b)=1ι(2)b−1/2>0, using [L4] and [L6]; and by [L2] it is continuous at every point of I, hence continuous on I.

L1L2L4L6
1.2

The interior points of I=(0,1] are exactly the reals b with 0<b<1: for such a b the neighbourhood Nρ(b) with ρ:=min⁡{b, 1−b}>0 lies in (0,1)⊆I; the point 1 is not interior, since 1+ε/2∈Nε(1) and 1+ε/2∉I for every real ε>0; and every interior point lies in I.

L7
2.1

The derivative is bounded above by no real. Let K be a real. If K≤0, any b with 0<b<1 has s′(b)>0≥K by step 1.1. If K>0, put β:=(1/(ι(2)K))2, a positive real, and use [L5] to fix a natural m≥1 with 1/ι(m)<min⁡{β, 1}; put b:=1/ι(m), so 0<b<1 and b<β. By [L4], b1/2<β1/2=(1/(ι(2)K))2⋅(1/2)=1/(ι(2)K), so b−1/2=1/b1/2>ι(2)K by [L6], and hence s′(b)=1ι(2)b−1/2>K. So for every real K there is an interior point b of I with s′(b)>K, and the set of values of s′ on the interior of I is bounded above by no real.

step 1.1step 1.2L4L5L6L7
2.2

s is not Lipschitz on I. Suppose some real L≥0 satisfied ∣s(x)−s(y)∣≤L∣x−y∣ for all x,y∈I. Let t be a real with 0<t≤1/ι(2), and put x:=t2 and y:=ι(4)t2. Then 0<x≤y=ι(4)t2≤ι(4)/ι(4)=1, so x,y∈I; and s(x)=t and s(y)=ι(2)t by [L3], since t≥0 with t2=x and ι(2)t≥0 with (ι(2)t)2=ι(4)t2=y. Hence ∣s(y)−s(x)∣=ι(2)t−t=t and ∣y−x∣=ι(3)t2 by [L6], and the supposition gives t≤L ι(3)t2; dividing by t>0 gives 1≤ι(3)Lt for every such t. Taking t:=1/ι(2) shows ι(3)L/ι(2)≥1, so L>0. Now use [L5] to fix a natural m≥1 with 1/ι(m)<1/(ι(3)L) and put t:=min⁡{1/ι(m), 1/ι(2)}, a real with 0<t≤1/ι(2); then ι(3)Lt≤ι(3)L/ι(m)<1, contradicting 1≤ι(3)Lt. So no such L exists.

step 1.1L3L4L5L6
3.1

The refuted claim therefore fails at I:=(0,1] and h:=s: by step 1.1 the function s is continuous on the order-convex set I and differentiable at every point of I, in particular at every interior point of I by step 1.2, and yet by step 2.2 it is not Lipschitz on I. Nothing in [L8] is contradicted: by step 2.1 no real M bounds ∣s′∣ on the interior of I, so the hypothesis deleted from that corollary is exactly the one that fails.

step 1.1step 1.2step 2.1step 2.2L8∎

Remarks

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

91 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