# Nonuniform trapezoids and signed error

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

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-trapezoidal-quadrature-01 · ocme-new142-reader-adoption-20261021



## Goal and scope

For f(x)=x^2 and nodes (0,1/2,2), compute T, I-T and absolute error.

Nonuniform partitions are allowed; the full quadratic gives an independent reference integral, not a general error bound or convergence order.





## Givens and symbols


- algebra
- polynomial
- trap_def
- integral_poly


- G1 — f(x)=x^2 on [0,2], nodes (0,1/2,2), values (0,1/4,4).


- T — trapezoid value
- E=I-T — fixed signed error
- h_i — individual interval width





## Rules and sources


- mko_definition · cited — Source semantic paraphrase: on a qualified nonuniform partition, sum each width times its endpoint-value average; a finite table does not determine a general integral. · mko-trapezoidal-quadrature
- algebra · prerequisite — Use real-field identities; division requires a nonzero denominator and multiplication by a positive number preserves inequalities.
- polynomial · prerequisite — Real polynomials are continuous and differentiate termwise: the derivative of x^k is k*x^(k-1), and constants differentiate to zero.
- trap_def · prerequisite — The composite trapezoid value sums (x_i-x_(i-1))*(y_(i-1)+y_i)/2; nodes are strictly increasing with aligned endpoint values, and n intervals have n+1 nodes.
- integral_poly · prerequisite — Integrate real polynomials on finite intervals termwise using antiderivative x^(k+1)/(k+1).





## Main derivation

S01 · impliesBefore

0<1/2<2,\quad\#\text{nodes}=3

After

n=2,\quad\#\text{values}=3

Conditions: none

Rule: trap_def · Uses: G1

Leaf basis: trap_def

The valid partition has two intervals and three nodes, with a matching value array.



S02 · equivalentBefore

(f(0),f(1/2),f(2))

After

(0,1/4,4)

Conditions: none

Rule: algebra · Uses: G1, S01

Leaf basis: algebra

Independently recompute every endpoint value from the full function.



S03 · equivalentBefore

h_1=x_1-x_0,\quad h_2=x_2-x_1

After

h_1=1/2,\quad h_2=3/2

Conditions: none

Rule: algebra · Uses: G1, S01

Leaf basis: algebra

The widths differ, so a single h cannot be substituted.



S04 · impliesBefore

T_1=\tfrac12\tfrac{0+1/4}{2},\quad T_2=\tfrac32\tfrac{1/4+4}{2}

After

T_1=1/16,\quad T_2=51/16

Conditions: none

Rule: trap_def · Uses: S02, S03

Leaf basis: trap_def

Each interval uses its own width times its own endpoint-value average.



S05 · equivalentBefore

T=T_1+T_2

After

T=52/16=13/4

Conditions: none

Rule: algebra · Uses: S04

Leaf basis: algebra

Sum the two intervals exactly.



S06 · impliesBefore

I=\int_0^2x^2\,dx

After

I=[x^3/3]_0^2=8/3

Conditions: none

Rule: integral_poly · Uses: G1

Leaf basis: integral_poly

The full quadratic permits an independent reference integral not inferred from samples.



S07 · equivalentBefore

E=I-T=8/3-13/4

After

E=-7/12,\quad|E|=7/12

Conditions: none

Rule: algebra · Uses: S05, S06

Leaf basis: algebra

Signed error is fixed as exact integral minus trapezoid value; report its magnitude separately.



S08 · impliesBefore

\ell(x)=mx+b,\quad u<v

After

\int_u^v\ell(x)\,dx=(v-u)\left(m\frac{u+v}{2}+b\right)=(v-u)\frac{\ell(u)+\ell(v)}2

Conditions: u<v

Rule: integral_poly · Uses: S03

Leaf basis: integral_poly

The per-interval antiderivative identity proves affine exactness on any valid partition; sum the intervals. The nonaffine main example has nonzero error.







## Substeps and lemmas

No substeps in this guide.





## Reverse audits


- S08 · premise_audit · S03 — Affine exactness is not a general second-derivative error bound or convergence rate.
- S07 · inverse_equivalence · S05, S06 — The negative sign means overestimation; an error magnitude is not negative.
- S06 · premise_audit · G1 — A node table alone would not supply this full-integrand certificate.
- S05 · inverse_equivalence · S04 — T is the quadrature value, not yet called the exact integral.
- S04 · premise_audit · S02, S03 — The interior node participates once in each adjacent interval as intended.
- S03 · inverse_equivalence · G1, S01 — Their sum is 2=b-a as a consistency check.
- S02 · inverse_equivalence · G1, S01 — The table is bound to a specified full function.
- S01 · premise_audit · G1 — Three nodes do not make three subintervals.





## Error controls and negative controls

Each widthCompute each h_i before multiplying its endpoint average.

Error signKeep I-T fixed and report its absolute value separately.


- Three nodes give three intervals. → reject — There are only two adjacent endpoint pairs.
- One h applies to this nonuniform partition. → reject — The widths are 1/2 and 3/2.
- Three sampled values uniquely determine the integral. → reject — Adding a positive multiple of x^2*(x-1/2)^2*(x-2)^2 preserves nodes but increases the integral.





## Result and limitations

T=13/4, I=8/3, I-T=-7/12 and absolute error 7/12; affine functions are exact on each interval.







## Verification and source binding

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


- source commit: b1b2f1dcf8c50d67a93fe52d95f8eef7b3abba9f
- adopted source SHA-256: 0523238679e2cdf17d8dbeaaa405cec37b031589a6c3c5e271550f3786ebdf06
- original source SHA-256: 0523238679e2cdf17d8dbeaaa405cec37b031589a6c3c5e271550f3786ebdf06
- Lean: NOT_RUN · independent AI: SCOPED_LEAD_AND_BILINGUAL_CONTEXT_REVIEW

[Same-source full JSON (formulas, ASTs, controls and revision log)](https://ocme.evemisslab.com/data/derivations/coverage-20261021/guides/derivation-mko-trapezoidal-quadrature-01.json)