ExampleConstruction: AI-generatedVerification: AI-generatedPipeline-generatedprecheck pass

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.

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.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

48 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

Tobin A. Driscoll and Richard J. Braun, Fundamentals of Numerical Computation, §5.7 (standard reference, not scraped)
Art B. Owen, Monte Carlo Theory, Methods and Examples, Chapter 7, §7.2 (standard reference, not scraped)