# Definite integral: computing ∫₀³(x²−4)dx as a limit of left sums and by the moment formula

[← Guide index](https://ocme.evemisslab.com/en/derivations/) · [Original MKO](https://ocme.evemisslab.com/en/mko/mko-definite-integral/)

This is an owner-adopted natural-language teaching guide. Finite/arithmetic checks are not universal proofs; no Lean was run, and review scope is recorded per revision. Original source status labels are retained as historical data. Formulas retain exact TeX; no new semantic AST is invented.

derivation-mko-definite-integral-01 · production-20261019-adopted-96



## Goal and scope

Let f(x)=x²−4, a=0, b=3. (1) Using only the Riemann definition (the common limit of all valid tagged-partition sums as the mesh tends to zero) and the premise that f is integrable, find I(f,0,3) as the limit of the N-piece left sums L_N; (2) recompute it independently with the moment formula listed in this MKO and compare; (3) find the reversed integral I(f,3,0); (4) use N=3 and N=50 to show that a finite left sum is not the integral, and explain why the signed integral is not a nonnegative area.

Treats only one continuous polynomial within the MKO's scope, f(x)=x²−4 (integer coefficients, degree 2), and its signed Riemann integral over the finite interval [0,3]. Integrability of f is taken from MKO assumption a1 and is not proved here; what is proved is that, given integrability, the integral must equal −3. The general fundamental theorem of calculus is neither used nor claimed; general integrable functions, Lebesgue integration and area theory are not treated; the canonical MKO and its English edition are not changed.





## Givens and symbols


- finite_sum_rules
- seq_limit_def
- archimedean
- order_basics
- numeric_evaluation


- G1 — f(x)=x²−4 with endpoints a=0≤b=3. f is a polynomial of degree 2 with integer coefficients (ascending coefficients −4, 0, 1), as MKO assumption a1 requires.
- G2 — MKO assumption a1: f is continuous on all of ℝ and integrable on finite intervals; so I(f,0,3) exists and is a real number.
- G3 — The left sum of MKO assumption a3: for a≤b and a positive integer N, Δx=(b−a)/N, x_i=a+iΔx and L_N=Σ_{i=0}^{N−1} f(x_i)Δx. Here Δx=3/N and x_i=3i/N.


- f(x)=x^2-4 — the integrand polynomial
- I(f,a,b) — the oriented definite integral of f from a to b
- N — number of equal pieces, a positive integer
- \Delta x=\tfrac{3}{N} — length of each piece, which is also the mesh
- x_i=\tfrac{3i}{N} — the division point at index i; for 0≤i<N, also the left tag of piece i+1
- L_N — the N-piece left sum
- S(f,P,\xi) — the Riemann sum of a tagged partition (P,ξ)





## Rules and sources


- finite_sum_rules · prerequisite — Finite sums: Σ_{i=1}^{0} a_i=0 and Σ_{i=1}^{n+1} a_i=Σ_{i=1}^{n} a_i + a_{n+1}; Σ(a_i+b_i)=Σa_i+Σb_i; Σ c·a_i=c·Σa_i.
- seq_limit_def · prerequisite — Limit of a sequence: a_n→L means that for every ε>0 there is N such that |a_n−L|<ε for all n≥N.
- archimedean · prerequisite — Archimedean property: for every real x there is a natural number n>x; hence for every ε>0 there is n with 1/n<ε.
- order_basics · prerequisite — Order of the reals: exactly one of u<v, u=v, u>v holds; u<v and v<w give u<w; u<v gives u+w<v+w; u<v and w>0 give uw<vw; u<v and w<0 give uw>vw.
- numeric_evaluation · prerequisite — Exact evaluation of an explicit integer or rational expression; independently recomputable.
- def_unfold · prerequisite — Unfolding a definition: replacing a defined term by its definition (or folding it back) does not change whether a statement is true.
- distributive · prerequisite — Distributivity: u(v+w)=uv+uw; with commutativity also (v+w)u=vu+wu.
- frac_rules · prerequisite — Fraction rules (all denominators nonzero): a/c+b/c=(a+b)/c; (a/b)(c/d)=(ac)/(bd); (a/b)/(c/d)=(ad)/(bc) (also needing c≠0); a/b=(ak)/(bk) for k≠0.
- power_laws · prerequisite — Integer exponent laws (base nonzero, or exponents positive integers): a^m·a^n=a^{m+n}, (a^m)^n=a^{mn}, (ab)^n=a^n b^n, a^0=1.
- nat_induction · prerequisite — Principle of induction: for a family P(n) starting at n₀, if P(n₀) holds and P(n)⇒P(n+1) for every n≥n₀, then P(n) holds for every n≥n₀.
- add_comm · prerequisite — Commutativity of addition: u+v=v+u.
- mul_inverse_nonzero · prerequisite — Inverse of a nonzero number: in ℚ, ℝ or ℂ, if u≠0 there is 1/u with u·(1/u)=1, and v/u means v·(1/u). 0 has no inverse, so v/0 is undefined.
- abs_rules · prerequisite — Absolute value (reals): |u|=u if u≥0 and |u|=−u if u<0; |u|≥0; |uv|=|u||v|; triangle inequality |u+v|≤|u|+|v|; |u|<r ⇔ −r<u<r.
- modus_ponens · prerequisite — Modus ponens: from P and P⇒Q infer Q.
- neg_mul · prerequisite — Signs and multiplication: (−u)v=−(uv) and (−u)(−v)=uv.
- and_intro_elim · prerequisite — Conjunction: from P and Q infer P∧Q; from P∧Q infer P and infer Q.
- mko_riemann_def · cited — For a continuous polynomial f on a finite real interval a≤b, its Riemann integral is the common limit of all valid tagged-partition sums as the mesh tends to zero. · mko-definite-integral
- mko_reverse · cited — Reversing endpoints changes the sign: I(f,a,b)=−I(f,b,a); equal endpoints give I(f,a,a)=0. · mko-definite-integral
- mko_moment · cited — This slice explicitly uses the moment formula I(x^n,a,b)=(b^{n+1}−a^{n+1})/(n+1); for f=Σc_k x^k the moments are summed coefficientwise: I(f,a,b)=Σc_k(b^{k+1}−a^{k+1})/(k+1). · mko-definite-integral
- riemann_limit_meaning · prerequisite — The precise meaning of 'the common limit is I': for every ε>0 there is δ>0 such that every tagged partition (P,ξ) of [a,b] with mesh less than δ has |S(f,P,ξ)−I|<ε. A partition P is a finite strictly increasing list of points t_0=a<t_1<t_2 up to t_m=b; a tag ξ_j lies in [t_{j−1},t_j]; the mesh is the largest t_j−t_{j−1}; S(f,P,ξ)=Σ_{j=1}^{m} f(ξ_j)(t_j−t_{j−1}).
- limit_unique · prerequisite — Limits of sequences are unique: if s_N→L and s_N→L′, then L=L′.
- L_sum_sq · lemma — For every positive integer N, Σ_{i=0}^{N−1} i²=(N−1)N(2N−1)/6.





## Main derivation

S01 · definitionBefore

I(f,0,3)

After

\forall\varepsilon>0\ \exists\delta>0:\ \operatorname{mesh}(P)<\delta\Rightarrow|S(f,P,\xi)-I(f,0,3)|<\varepsilon

Conditions: 0\le 3

Rule: mko_riemann_def · Uses: G1, G2

Leaf basis: mko_riemann_def + riemann_limit_meaning + def_unfold

By the MKO's definition, I(f,0,3) is the common limit of all valid tagged-partition sums on [0,3] as the mesh tends to zero; by riemann_limit_meaning this means precisely: for every ε>0 there is δ>0 such that every tagged partition (P,ξ) with mesh less than δ has |S(f,P,ξ)−I(f,0,3)|<ε. G2 guarantees that such a number exists; the task here is to find its value.



S02 · impliesBefore

L_N=\sum_{i=0}^{N-1} f(x_i)\,\Delta x

After

L_N=S(f,P_N,\xi_N),\quad \operatorname{mesh}(P_N)=\tfrac{3}{N}

Conditions: N\ge 1

Rule: riemann_limit_meaning · Uses: G3, S01

Leaf basis: riemann_limit_meaning + order_basics + numeric_evaluation

Take the division points x_i=3i/N for i=0 to N. Consecutive points differ by 3/N>0, so they increase strictly, with x_0=0 and x_N=3; they form a partition P_N of [0,3]. Piece i+1, [x_i,x_{i+1}], is tagged by its left endpoint x_i, which does lie in that piece. Every piece has length 3/N, so the mesh is 3/N. Thus L_N is exactly a valid tagged-partition sum.



S03 · impliesBefore

\operatorname{mesh}(P_N)=\tfrac{3}{N}\ \text{and S01}

After

L_N\to I(f,0,3)\quad(N\to\infty)

Conditions: N\ge 1

Rule: seq_limit_def · Uses: S01, S02, archimedean

Leaf basis: seq_limit_def + archimedean + order_basics

Given ε>0, take the δ of S01. By the Archimedean property choose a natural number N_0>3/δ (with N_0≥1). For every N≥N_0, 3/N≤3/N_0<δ, so the mesh of P_N is below δ and S01 gives |L_N−I(f,0,3)|<ε. This is exactly the definition of the sequence limit L_N→I(f,0,3).



S04 · equivalentBefore

f(x_i)\,\Delta x

After

\tfrac{27i^2}{N^3}-\tfrac{12}{N}

Conditions: N\ge 1

Rule: distributive · Uses: G1, G3

Leaf basis: distributive + frac_rules + power_laws

Substitute x_i=3i/N: f(x_i)=(3i/N)²−4=9i²/N²−4; multiplying by Δx=3/N and distributing gives 27i²/N³−12/N.



S05 · equivalentBefore

L_N=\sum_{i=0}^{N-1}\left(\tfrac{27i^2}{N^3}-\tfrac{12}{N}\right)

After

L_N=\tfrac{27}{N^3}\sum_{i=0}^{N-1} i^2-12

Conditions: N\ge 1

Rule: finite_sum_rules · Uses: S04, finite_sum_rules

Leaf basis: finite_sum_rules + frac_rules

A finite sum splits term by term and the constant factor 27/N³ comes out of the sum; the constant term 12/N appears N times (i=0 to N−1), giving N·(12/N)=12.



S06 · equivalentBefore

\sum_{i=0}^{N-1} i^2

After

\tfrac{(N-1)N(2N-1)}{6}

Conditions: N\ge 1

Rule: L_sum_sq · Uses: S05, L_sum_sq

Leaf basis: nat_induction + finite_sum_rules + distributive

By Lemma L_sum_sq (proved in S06.1 to S06.3), replace the sum of squares by its closed form.



S07 · equivalentBefore

L_N=\tfrac{27}{N^3}\cdot\tfrac{(N-1)N(2N-1)}{6}-12

After

L_N=-3-\tfrac{27}{2N}+\tfrac{9}{2N^2}

Conditions: N\ge 1

Rule: frac_rules · Uses: S05, S06

Leaf basis: frac_rules + distributive + mul_inverse_nonzero

Simplify: 27/N³·(N−1)N(2N−1)/6=9(N−1)(2N−1)/(2N²)=9(2N²−3N+1)/(2N²)=9−27/(2N)+9/(2N²). Subtracting 12 gives −3−27/(2N)+9/(2N²). Cancelling N needs N≠0, which N≥1 guarantees.



S08 · impliesBefore

L_3,\ L_{50}

After

L_3=-7,\quad L_{50}=-\tfrac{16341}{5000}

Conditions: none

Rule: numeric_evaluation · Uses: S07, G3

Leaf basis: numeric_evaluation

N=3: Δx=1, left points 0, 1, 2, values of f −4, −3, 0, so directly L_3=−7; the formula gives −3−27/6+9/18=−3−9/2+1/2=−7, which agrees. N=50 (the largest N allowed by MKO assumption a3): L_50=−3−27/100+9/5000=−16341/5000=−3.2682. Neither equals −3.



S09 · impliesBefore

|L_N-(-3)|

After

\tfrac{27N-9}{2N^2}\le\tfrac{27}{2N}

Conditions: N\ge 1

Rule: abs_rules · Uses: S07

Leaf basis: abs_rules + order_basics + frac_rules

By S07, L_N+3=−27/(2N)+9/(2N²)=−(27N−9)/(2N²). For N≥1, 27N−9≥18>0, so |L_N+3|=(27N−9)/(2N²). Since −9<0, (27N−9)/(2N²)≤27N/(2N²)=27/(2N).



S10 · impliesBefore

|L_N+3|\le\tfrac{27}{2N}\ \ (N\ge 1)

After

L_N\to -3

Conditions: \varepsilon>0

Rule: seq_limit_def · Uses: S09, archimedean

Leaf basis: seq_limit_def + archimedean + order_basics

Given ε>0, the Archimedean property gives a natural number N_1>27/(2ε). For every N≥N_1, |L_N−(−3)|≤27/(2N)≤27/(2N_1)<ε. By the definition of a sequence limit, L_N→−3.



S11 · impliesBefore

L_N\to I(f,0,3),\quad L_N\to -3

After

I(f,0,3)=-3

Conditions: none

Rule: limit_unique · Uses: S03, S10, limit_unique

Leaf basis: limit_unique + modus_ponens

The same sequence L_N converges to I(f,0,3) (S03) and to −3 (S10); a sequence has at most one limit, so I(f,0,3)=−3.



S12 · theorem_applicationBefore

I(f,0,3)=I(x^2,0,3)-4\,I(x^0,0,3)

After

\tfrac{3^3-0^3}{3}-4\cdot\tfrac{3^1-0^1}{1}=9-12=-3

Conditions: 0\le 3

Rule: mko_moment · Uses: G1, mko_moment

Leaf basis: mko_moment + numeric_evaluation

A second route: the MKO's listed moment formula, summed coefficientwise. The moment of x² is (3³−0³)/3=9 and that of the constant 1=x⁰ is (3−0)/1=3, so I(f,0,3)=9−4·3=−3, the same as S11.



S13 · equivalentBefore

I(f,3,0)

After

-I(f,0,3)=3

Conditions: none

Rule: mko_reverse · Uses: S11, mko_reverse

Leaf basis: mko_reverse + neg_mul

Reversing the endpoints changes the sign: I(f,3,0)=−I(f,0,3)=−(−3)=3.



S14 · theorem_applicationBefore

I(f,0,2),\ I(f,2,3)

After

-\tfrac{16}{3},\ \tfrac{7}{3}

Conditions: 0\le 2; 2\le 3

Rule: mko_moment · Uses: G1, mko_moment

Leaf basis: mko_moment + numeric_evaluation + order_basics

Apply the moment formula piecewise: I(f,0,2)=(2³−0)/3−4·2=8/3−8=−16/3; I(f,2,3)=(3³−2³)/3−4·(3−2)=19/3−4=7/3. The two pieces add to −16/3+7/3=−3=I(f,0,3). The signs come from f(x)=(x−2)(x+2), which is negative for 0≤x<2 (for example f(1)=−3) and positive for 2<x≤3.



S15 · impliesBefore

|I(f,0,3)|

After

3\neq\tfrac{23}{3}=|I(f,0,2)|+|I(f,2,3)|

Conditions: none

Rule: numeric_evaluation · Uses: S11, S14

Leaf basis: abs_rules + numeric_evaluation

The signed integral lets the negative piece and the positive piece cancel: |I(f,0,3)|=3, while the absolute values of the two pieces add to 16/3+7/3=23/3. So 'the integral is a nonnegative area' and 'taking an absolute value gives the integral' both fail here; MKO assumption a2 states that the integral is oriented and signed.



S16 · impliesBefore

\text{goals (1) to (4)}

After

I(f,0,3)=-3,\ I(f,3,0)=3,\ L_3=-7,\ L_{50}=-\tfrac{16341}{5000}

Conditions: none

Rule: and_intro_elim · Uses: S08, S11, S12, S13, S15

Leaf basis: and_intro_elim

Combine: (1) S11 gives I(f,0,3)=−3 from the definition; (2) S12 gives the same value by the moment formula; (3) S13 gives I(f,3,0)=3; (4) S08 shows finite left sums differ from the integral and S15 shows the signed integral is not a nonnegative area.







## Substeps and lemmas

S06.1 · induction_baseBefore

\sum_{i=0}^{0} i^2

After

0=\tfrac{(1-1)\cdot 1\cdot(2\cdot 1-1)}{6}

Conditions: N=1

Rule: numeric_evaluation · Uses: finite_sum_rules

Leaf basis: finite_sum_rules + numeric_evaluation

N=1: the sum has the single term i=0, equal to 0²=0; the right side is (1−1)·1·(2−1)/6=0. The base case holds.



S06.2 · induction_stepBefore

\sum_{i=0}^{N-1} i^2=\tfrac{(N-1)N(2N-1)}{6}

After

\sum_{i=0}^{N} i^2=\tfrac{N(N+1)(2N+1)}{6}

Conditions: N\ge 1

Rule: finite_sum_rules · Uses: finite_sum_rules, distributive

Leaf basis: finite_sum_rules + distributive + add_comm

Assume the formula for N. The new sum has one more term, i=N: Σ_{i=0}^{N} i²=(N−1)N(2N−1)/6+N²=N[(N−1)(2N−1)+6N]/6=N(2N²+3N+1)/6=N(N+1)(2N+1)/6. This is the formula with N replaced by N+1, since (N+1)−1=N and 2(N+1)−1=2N+1.



S06.3 · impliesBefore

P(1)\ \land\ \forall N\ge 1\,(P(N)\Rightarrow P(N+1))

After

\forall N\ge 1:\ P(N)

Conditions: none

Rule: nat_induction · Uses: S06.1, S06.2, nat_induction

Leaf basis: nat_induction

Let P(N) be 'Σ_{i=0}^{N−1} i²=(N−1)N(2N−1)/6'. S06.1 gives P(1) and S06.2 gives P(N)⇒P(N+1); by the induction principle (n₀=1), P(N) holds for every N≥1. S06.1 to S06.3 together prove Lemma L_sum_sq.







## Reverse audits


- S16 · sufficient_goal_reduction · S08, S11, S12, S13, S15, and_intro_elim — Goal G: the four parts. Sufficient condition H: the conclusions of S08, S11, S12, S13 and S15 together; H⇒G is just conjunction. H is proved forwards from G1 to G3; G is never used as a premise.
- S15 · premise_audit · S11, S14, abs_rules — This compares explicit numbers (N15). Area theory is not developed here; 23/3 is only the sum of the two absolute values.
- S14 · premise_audit · mko_moment, numeric_evaluation, order_basics — This only applies the moment formula on two pieces (N12 to N14, N16); additivity over intervals for general functions is not claimed.
- S13 · inverse_equivalence · S11, mko_reverse — Reversing once more gives I(f,0,3)=−I(f,3,0)=−3, back to S11; the sign rule works in both directions.
- S12 · premise_audit · G1, mko_moment, numeric_evaluation — The moment formula is a rule listed for this slice and is only applied here; agreement of the two routes is a cross-check. It is not, and is not claimed to be, a proof of the general fundamental theorem of calculus.
- S11 · premise_audit · S03, S10, G2, limit_unique — Both limits must concern the same sequence, and S03 relies on existence from G2. Without integrability one would only know that the left sums tend to −3, which could not be called the integral.
- S10 · premise_audit · S09, seq_limit_def, archimedean — The definition requires the bound for all N≥N_1, not only N≤50; this is why the bound of S09 had to be proved for general N rather than read off a finite table.
- S09 · premise_audit · S07, abs_rules, order_basics — N≥1 is needed to know 27N−9>0 and remove the absolute value; the inequality is a one-way bound, not an equality. N10 is a finite check for N=1 to 50.
- S08 · premise_audit · S07, numeric_evaluation — These are values at two N (N5 to N8), used to cross-check the formula of S07 and to show that a finite sum is not the integral; they do not prove the limit.
- S07 · inverse_equivalence · frac_rules, distributive, mul_inverse_nonzero — Multiplying both sides by the nonzero 2N² turns each into the same polynomial −6N²−27N+9 (N3 checks this degree-2 identity); dividing back by 2N² is allowed, so the step is two-way. N4 also checks N=1 to 50 point by point, which is only a finite check.
- S06.3 · premise_audit · S06.1, S06.2, nat_induction — Induction needs both the base and the step; both are proved, and neither uses the lemma itself.
- S06.2 · premise_audit · finite_sum_rules, distributive — It uses only the induction hypothesis for N and the polynomial identity (N−1)N(2N−1)/6+N²=N(N+1)(2N+1)/6 (N1, a grid check of a degree-3 identity).
- S06.1 · premise_audit · finite_sum_rules, numeric_evaluation — Only direct evaluation of both sides is needed (N2).
- S06 · inverse_equivalence · L_sum_sq — The two expressions are equal for every N≥1, so the replacement works in both directions.
- S05 · inverse_equivalence · finite_sum_rules, frac_rules — Backward: multiply 27/N³ back into each term and write 12 as the sum of N copies of 12/N to return to the original; the finite-sum rules used are identities.
- S04 · inverse_equivalence · distributive, frac_rules, power_laws — Backward: factor out 3/N to get (3/N)(9i²/N²−4)=f(x_i)Δx. For N≠0 both expressions are the same number.
- S03 · premise_audit · S01, S02, G2, seq_limit_def, archimedean — This step uses the existence of I(f,0,3) (G2). The converse is not claimed: convergence of one family of left sums does not imply integrability; MKO paragraph 0 also stresses that the definition requires the common limit over all valid tagged partitions.
- S02 · premise_audit · G3, riemann_limit_meaning, order_basics — It needs N≥1, so that Δx=3/N is defined and positive. It claims only that each left sum is a tagged-partition sum; the converse (every tagged-partition sum is a left sum) is false and is not claimed.
- S01 · premise_audit · G1, G2, mko_riemann_def, riemann_limit_meaning — This step only unfolds the definition and records the existence premise; it derives no value. Existence comes from G2 (MKO assumption a1), not from the convergence of one special family of sums later on.





## Error controls and negative controls

A finite left sum is not the integralOne misconception the MKO names is taking a finite left sum for the integral. By S09 the error |L_N+3|=(27N−9)/(2N²) is positive for every N≥1, so no left sum with finite N equals −3 (for example L_3=−7 and L_50=−3.2682); only the limit as N→∞ equals the integral.

Reversed endpoints change the sign∫₃⁰ and ∫₀³ have the same integrand and opposite orientation, so the value is 3, not −3. One may not ignore orientation on the grounds that it is 'the same interval', nor take absolute values by default (MKO assumption a2).

A signed integral is not an areaf is negative on [0,2) and positive on (2,3]; the pieces −16/3 and 7/3 cancel to −3, while the unsigned quantity is the sum of absolute values 23/3. Treating every integral as a nonnegative area would wrongly give 23/3 or 3 instead of −3.

A moment check is not the general FTCS12 applies the polynomial moment formula listed in this MKO; its agreement with S11 is only a cross-check of two routes. The MKO says the general fundamental theorem of calculus is not treated as a completed prerequisite, and this guide does not claim to prove it.


- L_50=−3.2682 is ∫₀³(x²−4)dx → reject — L_50 differs from −3 by (27·50−9)/(2·50²)=1341/5000≠0; the integral is the limit as N→∞.
- ∫₃⁰(x²−4)dx=∫₀³(x²−4)dx=−3 because it is the same interval → reject — The reversal rule gives I(f,3,0)=−I(f,0,3)=3.
- A definite integral is never negative, so ∫₀³(x²−4)dx should be 23/3 → reject — The integral is signed and equals −3; 23/3 is the sum of the absolute values of the two pieces.
- If one family of equal-piece left sums converges, the function is integrable and the integral is that limit → reject — The Dirichlet function D (1 at rationals, 0 elsewhere) on [0,1]: the left points i/N are rational, so every left sum is 1; but with irrational tags the sums are 0 for arbitrarily small mesh, so there is no common limit and D is not Riemann integrable (MKO paragraph 0).





## Result and limitations

Given integrability of f (MKO assumption a1), the Riemann definition and the limit of the left sums L_N=−3−27/(2N)+9/(2N²) give ∫₀³(x²−4)dx=−3; the MKO's moment formula independently gives the same value. With reversed endpoints ∫₃⁰(x²−4)dx=3. The finite left sums L_3=−7 and L_50=−3.2682 differ from the integral; the pieces −16/3 and 7/3 cancel, so the integral is not a nonnegative area.


- Integrability of f (G2) is taken from MKO assumption a1 and is not proved from the definition here; S03 depends on it.
- The moment formula (mko_moment) is a rule listed by the MKO; this guide checks its value independently from the definition for f(x)=x²−4 only and does not prove the general moment formula.
- N4 and N10 are finite checks for N=1 to 50 and support only those points; the conclusions for general N rest on the algebra of S07 and S09 and the polynomial identity N3.





## Verification and source binding

17 declared checks for this guide; only the listed expressions are covered.


- source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
- adopted source SHA-256: 1358dfe43443e21f9926bd2ea2dd97a3b9034b0966a92b412d106d4ae7195ad4
- original source SHA-256: 1358dfe43443e21f9926bd2ea2dd97a3b9034b0966a92b412d106d4ae7195ad4
- Lean: NOT_RUN · independent AI: NOT_MEASURED

[Same-source full JSON (formulas, ASTs, controls and revision log)](https://ocme.evemisslab.com/data/derivations/production-20261019/guides/derivation-mko-definite-integral-01.json)