Alphabeta Math
TheoremStatement: AI-adaptedProof: AI-generatedPipeline-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.

Sectional forward Euler separates temporal, quadrature, and cutoff errors

Statement

Assume all hypotheses of Sectional size discretization separates grid and cutoff errors, with continuous-model solution μt on [0,T], initial mass M1, grid spacing Δ≤1, and pivot endpoint R. Let the finite grid have m retained bins, take T>0, an integer N≥1, and h=T/N. Initialize both the exact finite sectional system and forward Euler by that theorem's same retained projection and tail-mass reservoir. Let yk be the successful forward-Euler states under the uniform positivity CFL, and let νtR be the exact finite-sectional retained measure. There are constants CE,T,R,Δ and CT independent of N such that dBL(∑iniNδxi,μT)≤m CE,T,R,Δh+eCTT[CQTΔ+Δ2M0(μT)+M1R+2K∗M12TaR]. The first term is temporal error for the fixed finite ODE; the terms in Δ and R−1 are the separate grid and cutoff errors. The temporal constant may depend on the fixed grid and cutoff.

Facts & Assumptions

Given: A fixed finite-dimensional sectional ODE, its accepted forward-Euler steps, and the grid/cutoff estimate.

[F1]

Sectional forward Euler converges globally with first-order error: ∥yN−y(T)∥2≤CE,T,R,Δh for the fixed finite system.

[F2]

Sectional size discretization separates grid and cutoff errors: the exact finite-sectional retained measure differs from μT by the displayed grid and cutoff terms.

[F3]

Bounded-Lipschitz discrepancy for finite measures: dBL(σ,0)≤∥σ∥TV.

Proof

1.1F1F3algebra

Write the population-coordinate error vector as e=nN−n(T). Its total-variation norm as an atomic signed measure is at most ∑i=1m∣ei∣≤m∥e∥2 by Cauchy-Schwarz. Thus [F1] and [F3] bound the temporal discrepancy by mCE,T,R,Δh.

2.1F2step 1.1algebra∎

Insert the exact finite-sectional measure between the Euler retained measure and μT. The triangle inequality and [F2] add the temporal term from step 1.1 to the grid and cutoff terms in [F2], giving the asserted separated error budget.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

16 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