Alphabeta Math
ExampleConstruction: AI-adaptedVerification: AI-generatedprecheck 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.

Worked derivatives from the algebra of derivatives and the power rule: (3x4−5x+2)′=12x3−5, and the quotient rule applied to (x2+1)/(x−1) on R∖{1}

Example

Numerals below denote canonical naturals of R: 3 is ι(3), 12 is ι(12), and so on (The canonical natural ι(n)=n⋅1F of a field). Powers are those of Integer powers am.

Claim 1. Let p:R→R be given by

p(x)  =  ι(3) x4  −  ι(5) x  +  ι(2).

Then p is differentiable at every c∈R (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) and

p′(c)  =  ι(12) c3−ι(5).

Claim 2. Put A0:={ x∈R:x−1≠0 }=R∖{1} and let r:A0→R be given by r(x)=(x2+1)/(x−1). Then every c∈A0 is a limit point of A0, r is differentiable at c as a function on A0, and

r′(c)  =  c2−ι(2)c−1(c−1)2.

Nothing here is new: both computations are readings of Sums, scalar multiples, products and quotients: (f+g)′(c)=f′(c)+g′(c), (αf)′(c)=αf′(c), (fg)′(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)≠0 on top of For a natural n≥1 the function x↦xn is differentiable everywhere with derivative ι(n) x n−1; for n=0 it is the constant 1, with derivative 0; for a natural n≥1 the function x↦x−n is differentiable at every x≠0 with derivative −ι(n) x−n−1; consequently every polynomial function is differentiable at every real, with the derivative computed term by term. They are written out because the two places a computation of this kind goes wrong are the constant term, whose derivative is 0 and not ι(0)c−1, and the domain of the quotient, which is not R.

Facts & Assumptions

Given: The functions p and r of the statement, and an arbitrary real c; for claim 2 also c≠1.

[L2]

Algebra of derivatives (Sums, scalar multiples, products and quotients: (f+g)′(c)=f′(c)+g′(c), (αf)′(c)=αf′(c), (fg)′(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)≠0): at a limit point c of the common domain, sums, scalar multiples and products of functions differentiable at c are differentiable at c with the stated formulas; and if the denominator v is nonzero at c then, on D0:={x:v(x)≠0}, the point c lies in D0 and is a limit point of D0, and (u/v)∣D0 is differentiable at c with derivative (u′(c)v(c)−u(c)v′(c))/v(c)2.

[L3]

Canonical naturals (The canonical natural ι(n)=n⋅1F of a field, Canonical naturals are positive and strictly increasing): ι(1)=1, ι(m+n)=ι(m)+ι(n) and ι(mn)=ι(m)ι(n) for naturals m,n≥1; in particular ι(3)ι(4)=ι(12) and ι(2)−1=1, the latter from ι(2)=ι(1)+1=1+1.

[L4]

Powers (Integer powers am): x0=1, x1=x and x2=x⋅x.

Verification

technique · direct
1.1

Let c∈R, a limit point of R by [L5]. By [L1] the functions x↦x4, x↦x1 and x↦x0 are differentiable at c with derivatives ι(4)c3, ι(1)c0=1 and 0 respectively, using [L4].

L1L4L5
1.2

Put u(x):=x2+1 and v(x):=x−1, both functions on R, and let c∈R with c≠1.

construct
2.1

Claim 1. The function p is the sum of the scalar multiples ι(3)⋅(x↦x4), (−ι(5))⋅(x↦x1) and ι(2)⋅(x↦x0), so by the sum and scalar-multiple rules of [L2] it is differentiable at c with p′(c)=ι(3)ι(4)c3+(−ι(5))⋅1+ι(2)⋅0=ι(12)c3−ι(5), the last step by [L3].

step 1.1L2L3
2.2

The functions u and v are differentiable at every real c with u′(c)=ι(2)c and v′(c)=1: u is the sum of x↦x2 and the constant 1, whose derivatives at c are ι(2)c1=ι(2)c and 0 by [L1] and [L4]; and v is the sum of x↦x1 and the constant −1.

step 1.1L1L2L4
3.1

Claim 2. By step 1.2 one has v(c)=c−1≠0, and {x∈R:v(x)≠0} is exactly A0. So the quotient rule of [L2] applies: c∈A0, the point c is a limit point of A0, and r=(u/v)∣A0 is differentiable at c with r′(c)=(u′(c)v(c)−u(c)v′(c))/v(c)2=(ι(2)c (c−1)−(c2+1))/(c−1)2.

step 1.2step 2.2L2
4.1

Expanding the numerator: ι(2)c(c−1)−(c2+1)=ι(2)c2−ι(2)c−c2−1=(ι(2)−1)c2−ι(2)c−1=c2−ι(2)c−1, the last equality because ι(2)−1=1 by [L3]. So r′(c)=(c2−ι(2)c−1)/(c−1)2.

step 3.1L3L4
5.1

Both claims are verified: claim 1 by step 2.1 and claim 2 by steps 3.1 and 4.1.

step 2.1step 4.1∎

Remarks

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

40 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