Alphabeta Math
ExampleConstruction: AI-generatedVerification: AI-generatedSession-authored (Fable 5 assisted)precheck passjudge pass (z-ai/glm-5.2)audited 2026-07-29
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.

A step function integrated by additivity over subintervals, and the same value from the definition

Example

Let f:[0,2]Rf : [0,2] \to \mathbb{R} be

f(x)  :=  {10x<1,31x2.f(x) \;:=\; \begin{cases} 1 & 0 \le x < 1, \\ 3 & 1 \le x \le 2. \end{cases}

Then ff is integrable on [0,2][0,2] and

02f  =  1+3  =  4.\int_0^2 f \;=\; 1 + 3 \;=\; 4 .

Two routes are carried out below. The first splits at the jump with For a<c<ba<c<b: ff is integrable on [a,b][a,b] if and only if it is integrable on [a,c][a,c] and on [c,b][c,b], and then abf=acf+cbf\int_a^b f = \int_a^c f + \int_c^b f; with the oriented form for arbitrary a,b,ca,b,c and evaluates each piece with Changing an integrable function at finitely many points changes neither its integrability nor its integral and the constant case of If mfMm \le f \le M on [a,b][a,b] then m(ba)L(f,P)abfabfU(f,P)M(ba)m(b-a) \le L(f,P) \le \underline{\int_a^b} f \le \overline{\int_a^b} f \le U(f,P) \le M(b-a) for every partition PP; in particular every constant function is integrable, with abc=c(ba)\int_a^b c = c(b-a). The second computes lower and upper Darboux sums directly on a three-point partition and squeezes.

Why this is the smallest interesting example. The jump sits at the interior point 11, which is a partition point of both routes, and a partition point lies in two subintervals (Partition of [a,b][a,b] as a finite strictly increasing list a=t0<t1<<tn=ba = t_0 < t_1 < \dots < t_n = b, its subintervals and their lengths, its mesh, refinement, and the common refinement of two partitions). That is exactly the case singled out in the proof of Changing an integrable function at finitely many points changes neither its integrability nor its integral, and it is why the value of ff at the single point 11 is irrelevant to both the integrability and the value while the upper sums still see it.

Facts & Assumptions

Given: The function ff above on [0,2][0,2], and a real η\eta with 0<η<10 < \eta < 1.

[L3]

Changing an integrable function at finitely many points changes neither its integrability nor its integral (Changing an integrable function at finitely many points changes neither its integrability nor its integral).

[L6]

Ordered-field arithmetic: the order is total and transitive, and a real that is 4+2η\le 4 + 2\eta for every η\eta in (0,1)(0,1) is 4\le 4 (Ordered field, Complete ordered field (least-upper-bound property), Intervals of R\mathbb{R}: the nine order-convex forms, nondegeneracy, and length).

Verification

technique · direct
1.1

ff is nondecreasing on [0,2][0,2]: for xyx \le y the only possibility not giving f(x)=f(y)f(x) = f(y) is x<1yx < 1 \le y, where f(x)=1<3=f(y)f(x) = 1 < 3 = f(y). Hence ff is bounded and integrable on [0,2][0,2], and likewise on [0,1][0,1] and on [1,2][1,2], by [L1].

givenL1
1.2

Second route. Let PηP_{\eta} be the partition of [0,2][0,2] with point set {0, 1η, 1, 2}\{0,\ 1-\eta,\ 1,\ 2\}, so n=3n = 3 with Δ0=1η\Delta_0 = 1-\eta, Δ1=η\Delta_1 = \eta and Δ2=1\Delta_2 = 1.

givenL5construct
2.1

First route, the piece [0,1][0,1]. The constant function 11 on [0,1][0,1] agrees with ff at every point of [0,1][0,1] except x=1x = 1, a single point; so by [L3] and [L4], 01f=011=1(10)=1\int_0^1 f = \int_0^1 1 = 1\cdot(1-0) = 1.

step 1.1L3L4
2.2

The piece [1,2][1,2]. There ff is the constant 33, so 12f=3(21)=3\int_1^2 f = 3\cdot(2-1) = 3 by [L4].

step 1.1L4
2.3

On I0=[0,1η]I_0 = [0,1-\eta], ff is constantly 11, so m0=M0=1m_0 = M_0 = 1. On I1=[1η,1]I_1 = [1-\eta,1], ff takes the value 11 at every point below 11 and 33 at 11, so m1=1m_1 = 1 and M1=3M_1 = 3 by [L5]. On I2=[1,2]I_2 = [1,2], ff is constantly 33, so m2=M2=3m_2 = M_2 = 3.

step 1.2givenL5
3.1

By [L2] with c:=1c := 1, 02f=01f+12f=1+3=4\int_0^2 f = \int_0^1 f + \int_1^2 f = 1 + 3 = 4.

step 1.1step 2.1step 2.2L2
3.2

Hence L(f,Pη)=1(1η)+1η+31=4L(f,P_{\eta}) = 1(1-\eta) + 1\cdot\eta + 3\cdot 1 = 4 and U(f,Pη)=1(1η)+3η+31=4+2ηU(f,P_{\eta}) = 1(1-\eta) + 3\eta + 3\cdot1 = 4 + 2\eta, by [L5].

step 2.3L5
4.1

By [L4] the number 02f\int_0^2 f lies between L(f,Pη)=4L(f,P_\eta) = 4 and U(f,Pη)=4+2ηU(f,P_\eta) = 4+2\eta for every η(0,1)\eta \in (0,1), so 402f44 \le \int_0^2 f \le 4 by [L6]; the second route agrees with step 3.1.

step 1.1step 3.1step 3.2L4L6

Remarks

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 80 results over 19 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