Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-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 forward and central error bounds have explicit balancing steps

Statement

Let H>0. Consider the conservative error bounds from Forward and central differences have first- and second-order error bounds on a permitted step interval (0,H], where every stencil with h≤H stays inside the domain. If M2>0 and δ>0, the forward bound

E+(h)=M2h/2+2δ/h

has the unique unconstrained minimizer h+=4δ/M2 and minimum 2M2δ. On (0,H] the minimizer is min⁡{h+,H}. If M3>0 and δ>0, the central conservative bound

E0(h)=M3h2/6+2δ/h

has the unique unconstrained minimizer h0=6δ/M33 and minimum M3h02/2; on (0,H] the minimizer is min⁡{h0,H}. These optimize the displayed error bounds, not the unknown actual error.

If δ=0 and the corresponding truncation constant is positive, the bound has infimum 0 as h↓0 and no minimizer for h>0. If the corresponding truncation constant is 0 and δ>0, the bound decreases with h, so its capped minimum is at H. If δ and the corresponding truncation constant are both zero, every permitted step is optimal.

Facts & Assumptions

Given: The derivative bounds, evaluation-error bound and permitted cap described above.

[F1]

Forward and central differences have first- and second-order error bounds: the forward and central conservative bounds are M2h/2+2δ/h and M3h2/6+2δ/h.

Proof

Given: The hypotheses listed above.

1.1givenF1F2algebra

Set r:=h/h+>0. The identity h+2=4δ/M2 gives E+(h)=M2h+2(r+r−1), while E+(h+)=M2h+. Since r+r−1−2=(r−1)2/r≥0, equality holds exactly at r=1. Thus h+ is the unique unconstrained minimizer and its value is 2M2δ.

1.2givenF1F2algebra

Set r:=h/h0 and a:=M3h02/6>0. From h03=6δ/M3, E0(h)=a(r2+2/r) and E0(h0)=3a. The difference is a(r2+2/r−3)=a(r−1)2(r+2)/r≥0, with equality only at r=1. Thus h0 uniquely minimizes the unconstrained bound, and the minimum is 3a=M3h02/2.

2.1givenstep 1.1algebra

If 0<r1<r2≤1, then (r1+r1−1)−(r2+r2−1)=(r2−r1)(1/(r1r2)−1)>0, since r1r2<1. Hence E+ strictly decreases up to h+; the global bound from step 1.1 gives the cap minimizer min⁡{h+,H}.

2.2givenstep 1.2algebra

If 0<r1<r2≤1, then (r12+2/r1)−(r22+2/r2)=(r2−r1)(2/(r1r2)−(r1+r2))>0, since r1r2<1 and r1+r2<2. Hence the central bound strictly decreases up to h0, so the cap minimizer is min⁡{h0,H}.

3.1givenF1algebra∎

If δ=0 and the corresponding truncation constant is positive, the bound in [F1] is a positive multiple of h or h2 and has infimum 0 as h↓0, not attained for h>0. If a truncation constant is 0 and δ>0, the bound is a positive multiple of h−1 and decreases to 0 as h→∞, while on a permitted capped interval it is minimized at H. If both constants vanish the bound is identically zero.

Depends on

Used by

Dependency tree · two levels

27 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