Alphabeta Math
TheoremStatement: Literature-sourcedProof: 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.

Conditional asymptotic validity of the Simpson /15 indicator

Statement

Let a<b, f∈C4([a,b]), nk=2k for k≥1, hk=(b−a)/nk, Qk=QS(f;a,b,nk), and c=−(1/180)∫abf(4)(x) dx. Let I=∫abf. Then the refinement indicator ηk=∣Qk+1−Qk∣15 satisfies ηk=∣c∣hk4/16+o(hk4). If c≠0, then ηk/∣I−Qk+1∣→1. The Richardson-corrected value Rk+1=Qk+1+(Qk+1−Qk)/15 satisfies I−Rk+1=o(hk4). When c=0, these statements give no relative error estimate for ηk; at no finite level does ηk alone certify the true error.

Facts & Assumptions

Given: A nondegenerate interval, a C4 integrand, nested composite Simpson grids with mesh widths hk+1=hk/2, and exact arithmetic.

[F1]

Leading composite Simpson error coefficient: I−Qk=chk4+o(hk4) with the stated coefficient c.

[F2]

Embedded Simpson refinement indicator: the magnitude of the embedded indicator is ∣Qk+1−Qk∣/15; a Richardson correction adds the signed quantity (Qk+1−Qk)/15 to the refined value.

[F3]

Higher derivatives and the classes Ck and C∞: C4 specifies continuous derivatives through order four on the closed interval.

[F4]

The reverse triangle inequality: for reals x,y, ∣∣x∣−∣y∣∣≤∣x−y∣.

Proof

1.1givenF1F3algebra

By [F3], the regularity hypothesis is f∈C4([a,b]). By [F1], write Ek:=I−Qk=chk4+rk where rk=o(hk4). Since hk+1=hk/2, Ek+1=chk4/16+o(hk4).

2.1givenF2F4step 1.1algebra

The signed difference Qk+1−Qk=Ek−Ek+1. Therefore [F2] and step 1.1 give (Qk+1−Qk)/15=chk4/16+sk for some sk=o(hk4). By [F4], the difference between ηk=∣(Qk+1−Qk)/15∣ and ∣c∣hk4/16 is at most ∣sk∣=o(hk4), so ηk=∣c∣hk4/16+o(hk4).

3.1givenF4step 1.1step 2.1algebra∎

If c≠0, step 1.1 and [F4] give ∣Ek+1∣/hk4→∣c∣/16>0, so Ek+1≠0 for all sufficiently large k; dividing the step 2.1 relation by ∣Ek+1∣ then gives ηk/∣Ek+1∣→1. Also I−Rk+1=(16Ek+1−Ek)/15, whose order-hk4 terms cancel by step 1.1, leaving o(hk4). If c=0, both leading terms vanish, and these asymptotic formulas do not give a relative-error conclusion. The limit statements do not bound any finite-level error.

Depends on

Used by

Dependency tree · two levels

23 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