Pipeline-generated

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.

✓ 3 results · all verified · 0 also independently AI-judged

Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs. The 3 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.

Adaptive quadrature and error indicators — Examples

1 · Prerequisites

2 · Summary

Objective

These exact examples show why an embedded Simpson difference remains an indicator: the sampled nodes can miss a positive feature entirely, and cancellation of the leading error coefficient changes the finite-level ratio. A narrow peak with a zero depth budget also demonstrates the explicit cap-reached result. None of these examples asserts a general accuracy rate.

3 · Logical flowchart

4 · Definitions, theorems and proofs

None yet.

5 · Examples, counterexamples and false statements

ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passOpen item page →

The Simpson indicator misses a feature between its sample nodes

Example

On $[0, 1]$ , let $f (x) = \prod_{r = 0}^{4} (x - r / 4)^{2} .$ The root indicator is zero, so for every $τ > 0$ the call to Finite-depth adaptive Simpson with an indicator with $D = 0$ and $P = 1$ accepts its root panel and returns estimate $0$ . Choose $τ = C / 32$ ; for this tolerance the true error is strictly greater than $τ$ .

Facts & Assumptions

Given: The polynomial $f$ above, the exact-real Simpson algorithm, and the adaptive call with $D = 0$ , $P = 1$ , and $τ = C / 32$ , where $C = {(\frac{1}{8} \frac{1}{16} \frac{5}{16} \frac{9}{16} \frac{13}{16})}^{2} > 0.$

[F1]

Finite-depth adaptive Simpson with an indicator: the root call returns the refined Simpson value with accepted status when its indicator does not exceed $τ$ .

[F2]

Embedded Simpson refinement indicator: the root indicator is $∣ S_{1} - S_{0} ∣ / 15$ using the parent and its two child Simpson values.

[F3]

Sums, scalar multiples, products, absolute values, maxima, minima and quotients with nonvanishing denominator of continuous functions are continuous, as are constants, the identity and every polynomial function: every polynomial is continuous.

[F4]

Every continuous function on a closed nondegenerate rectangle in $R^{m}$ is Riemann integrable: a continuous real function on $[0, 1]$ is Riemann integrable.

[F5]

If $f \leq g$ on $[a, b]$ and both are integrable then $\int_{a}^{b} f \leq \int_{a}^{b} g$ ; and $m (b - a) \leq \int_{a}^{b} f \leq M (b - a)$ : if integrable functions satisfy $g \leq f$ pointwise on the interval, then $\int g \leq \int f$ .

[F6]

Composite Simpson rule on an even uniform grid: for an even grid, the Simpson value is the stated weighted sum of its endpoint, midpoint and quarter-grid values.

[F7]

For $a < c < b$ : $f$ is integrable on $[a, b]$ if and only if it is integrable on $[a, c]$ and on $[c, b]$ , and then $\int_{a}^{b} f = \int_{a}^{c} f + \int_{c}^{b} f$ ; with the oriented form for arbitrary $a, b, c$ : for bounded integrable $f$ and $a < c < b$ , $\int_{a}^{b} f = \int_{a}^{c} f + \int_{c}^{b} f$ ; applying this twice splits the integral over the three adjacent intervals used below.

[F8]

If $m \leq f \leq M$ on $[a, b]$ then $m (b - a) \leq L (f, P) \leq \underline{\int_{a}^{b}} f \leq \overline{\int_{a}^{b}} f \leq U (f, P) \leq M (b - a)$ for every partition $P$ ; in particular every constant function is integrable, with $\int_{a}^{b} c = c (b - a)$ : the constant function $C$ on an interval of length $1 / 16$ has integral $C / 16$ .

Verification

1.1givenF2F6algebra

Every parent and child sample node is in ${0, 1 / 4, 1 / 2, 3 / 4, 1}$ . Each node makes one factor of $f$ zero, so [F6] gives $S_{0} = S_{1} = 0$ and [F2] gives indicator $0$ .

2.1givenF1step 1.1algebra

Since $0 \leq τ$ , [F1] accepts immediately, before the depth cap is relevant, and returns $S_{1} = 0$ .

3.1givenF3F4F5F7F8step 2.1algebra∎

On $[1 / 8, 3 / 16]$ , the five absolute factors are at least $1 / 8, 1 / 16, 5 / 16, 9 / 16, 13 / 16$ , respectively, so $f \geq C$ there. Since $f$ is a product of squares, $f \geq 0$ on all of $[0, 1]$ ; each factor has absolute value at most $1$ there, so $f \leq 1$ and is bounded. By [F3]–[F4], its restrictions to the three adjacent intervals determined by $1 / 8$ and $3 / 16$ are integrable. Monotonicity [F5] and the constant integral [F8] give $\int_{1 / 8}^{3 / 16} f \geq C / 16$ ; monotonicity [F5] gives nonnegative integrals on the two outer intervals. Applying the two-piece identity [F7] twice therefore yields $\int_{0}^{1} f \geq C / 16 = 2 τ$ . Step 2.1 gives returned estimate $0$ , so the returned error satisfies $∣ \int_{0}^{1} f - 0 ∣ \geq 2 τ > τ$ , despite the accepted status.

ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passOpen item page →

A narrow peak reaches the adaptive Simpson depth cap

Example

Let $f (x) = 1 / (1 + 10000 (x - 1 / 2)^{2})$ on $[0, 1]$ . With tolerance $τ = 1 / 1000$ , depth cap $D = 0$ , and panel-call budget $P = 1$ , Finite-depth adaptive Simpson with an indicator returns the refined estimate with cap-reached status.

Facts & Assumptions

Given: The real-valued rational function $f$ on $[0, 1]$ , exact arithmetic, and the adaptive call with $D = 0$ , $P = 1$ , $τ = 1 / 1000$ .

[F1]

Finite-depth adaptive Simpson with an indicator: if the local indicator exceeds its tolerance and the depth cap is reached, the call returns its refined estimate with cap-reached status.

[F2]

Embedded Simpson refinement indicator: the local indicator is $∣ S_{1} - S_{0} ∣ / 15$ .

[F3]

Composite Simpson rule on an even uniform grid: on an even uniform grid, the composite Simpson value is the weighted sum of the sampled endpoint, midpoint and quarter-grid values.

Verification

1.1givenF2F3algebra

The endpoint values are $f (0) = f (1) = 1 / 2501$ , the midpoint value is $f (1 / 2) = 1$ , and the quarter-point values are $f (1 / 4) = f (3 / 4) = 1 / 626$ . The composite rule [F3] gives $S_{0} = 2 / 3 + 1 / 7503$ and $S_{1} = (1 / 12) (2 + 8 / 626 + 2 / 2501)$ .

2.1givenF2step 1.1algebra

Since $8 / 626 = 4 / 313 < 1 / 75$ and $2 / 2501 < 1 / 1000$ , $S_{1} < 6043 / 36000$ , while $S_{0} > 2 / 3$ . Therefore $S_{0} - S_{1} > 17957 / 36000$ , and the indicator exceeds $17957 / 540000 > 1 / 1000 = τ$ .

3.1givenF1step 2.1algebra∎

The indicator rejects the root, and $D = 0$ prevents subdivision. By [F1], the procedure returns the refined estimate with cap-reached status; it makes no tolerance-success claim.

ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passOpen item page →

Cancellation of the leading Simpson error coefficient

Example

For $f (x) = x^{6} - 5 x^{4}$ on $[0, 1]$ , the leading coefficient $- (1 / 180) \int_{0}^{1} f^{(4)}$ in Conditional asymptotic validity of the Simpson /15 indicator vanishes, but the one-level indicator and the refined Simpson error are nonzero. In fact, the indicator is $21 / 5$ times the true refined error in this exact example.

Facts & Assumptions

Given: The polynomial $f (x) = x^{6} - 5 x^{4}$ on $[0, 1]$ , the exact integral, and composite Simpson grids with $n = 2$ and $n = 4$ .

[F1]

Composite Simpson rule on an even uniform grid: on an even uniform grid, $Q_{S} = (h / 3) \sum_{j < n / 2} (f (x_{2 j}) + 4 f (x_{2 j + 1}) + f (x_{2 j + 2}))$ .

[F2]

Embedded Simpson refinement indicator: $η = ∣ Q_{n = 4} - Q_{n = 2} ∣ / 15$ for this parent and its two-half refinement.

[F3]

Conditional asymptotic validity of the Simpson /15 indicator: the leading coefficient is $- (1 / 180) \int_{0}^{1} f^{(4)}$ .

[F4]

For a natural $n \geq 1$ the function $x \mapsto x^{n}$ is differentiable everywhere with derivative $ι (n) x^{n - 1}$ ; for $n = 0$ it is the constant $1$ , with derivative $0$ ; for a natural $n \geq 1$ the function $x \mapsto x^{- n}$ is differentiable at every $x \neq 0$ with derivative $- ι (n) x^{- n - 1}$ ; consequently every polynomial function is differentiable at every real, with the derivative computed term by term and Sums, scalar multiples, products and quotients: $(f + g)^{'} (c) = f^{'} (c) + g^{'} (c)$ , $(α f)^{'} (c) = α f^{'} (c)$ , $(f g)^{'} (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) \neq 0$ : polynomial powers differentiate by the power rule, and derivatives distribute over finite sums and scalar multiples.

[F5]

[F6]

Every continuous function on a closed nondegenerate rectangle in $R^{m}$ is Riemann integrable: continuous polynomials on $[0, 1]$ are Riemann integrable.

[F7]

The second fundamental theorem: if $G$ is differentiable on $[a, b]$ with $G^{'} = f$ and $f$ is integrable, then $\int_{a}^{b} f = G (b) - G (a)$ : integrating a continuous derivative gives the endpoint difference of its antiderivative.

[F8]

Higher derivatives and the classes $C^{k}$ and $C^{\infty}$ : $C^{4}$ means the derivatives through order four are continuous on the closed interval.

The polynomial is $C^{4}$ on $[0, 1]$ .

Verification

1.1givenF3F4F5F6F7F8algebra

By [F4] and [F5], $f^{(4)} (x) = 360 x^{2} - 120$ and this derivative is continuous. An antiderivative is $120 x^{3} - 120 x$ , so [F6]–[F7] give $\int_{0}^{1} f^{(4)} (x) d x = 0$ . Hence $f \in C^{4} ([0, 1])$ by [F8], and the leading coefficient in [F3] is zero.

1.2givenF1F4F5F6F7algebra

By [F4]–[F5], $x^{7} / 7 - x^{5}$ has derivative $f$ and $f$ is continuous, so [F6]–[F7] give the exact integral $1 / 7 - 1 = - 6 / 7$ . Also $f (0) = 0$ , $f (1 / 2) = - 19 / 64$ , and $f (1) = - 4$ ; substitution in [F1] gives $Q_{n = 2} = - 83 / 96$ . The quarter-point values are $f (1 / 4) = - 79 / 4096$ and $f (3 / 4) = - 5751 / 4096$ , so [F1] also gives $Q_{n = 4} = \frac{1}{12} (4 (- \frac{79}{4096}) + 2 (- \frac{19}{64}) + 4 (- \frac{5751}{4096}) - 4) = - \frac{5267}{6144} .$ Thus the refined error is $- 6 / 7 - Q_{n = 4} = 5 / 43008$ , and the coarse error is $- 6 / 7 - Q_{n = 2} = 5 / 672$ .

2.1givenF2step 1.1step 1.2algebra∎

From [F2], $η = ∣ Q_{n = 4} - Q_{n = 2} ∣ / 15 = 1 / 2048$ . Hence $η / (5 / 43008) = 21 / 5$ . The nonzero refined error and zero leading coefficient show why the asymptotic /15 relation supplies no relative finite-level guarantee in the cancelled case.

Adaptive quadrature and error indicators — Examples

1 · Prerequisites

2 · Summary

Objective

3 · Logical flowchart

4 · Definitions, theorems and proofs

5 · Examples, counterexamples and false statements

The Simpson indicator misses a feature between its sample nodes

Example

Facts & Assumptions

Verification

A narrow peak reaches the adaptive Simpson depth cap

Example

Facts & Assumptions

Verification

Cancellation of the leading Simpson error coefficient

Example

Facts & Assumptions

Verification

Sources