Alphabeta Math
ExampleConstruction: AI-adaptedVerification: 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.

One Robertson reaction step: Newton work and the chord reuse tradeoff

Example

The Robertson stiff reaction field is f(y)=(−0.04y1+104y2y30.04y1−104y2y3−3⋅107y223⋅107y22),y0=(1,0,0)T. For one backward Euler step with h=10−3, compare exact-Jacobian Newton (budget 12) and chord iteration with the Jacobian frozen at y0 (budget 8, refresh period 8). Both use the Euclidean residual norm and tolerance 10−12 with partial-pivoting binary64 Gaussian elimination. The record below is finite-precision work evidence from an implementation-level approximation of the mathematical solver. Binary64 Gaussian elimination does not meet the exact-solve backend contract of Finite-budget Newton and chord solves with scheduled factorization reuse, so this trace is not asserted to be an exact execution of that contract or a general convergence or forward-error theorem.

Numerical record

The residual is G(y)=y−y0−hf(y). The Jacobian used is JG(y)=I−hDf(y),Df(y)=(−0.04104y3104y20.04−104y3−6⋅107y2−104y206⋅107y20). Also ∑ifi(y)=0 identically, so every exact root preserves ∑iyi=1 when the input sum is one.

With binary64 arithmetic and partial pivoting, Newton's residual norms at correction counts 0,1,2,3,4,5 are respectively 5.65685425⋅10−5, 6.78768207⋅10−5, 8.45562545⋅10−6, 2.32643360⋅10−7, 1.97215675⋅10−10, 1.43041174⋅10−16. It returns root after five corrections, with five Jacobian assemblies/factorizations and five linear solves. Its last iterate is approximately (0.9999600054781065, 2.346970720497856⋅10−5, 1.652481468852211⋅10−5)T The component sum is one to binary64 rounding.

For chord iteration, residual norms at correction counts 0 through 8 are 5.65685425⋅10−5, 6.78768207⋅10−5, 6.51657654⋅10−5, 5.88221242⋅10−5, 6.10108196⋅10−5, 6.61093086⋅10−5, 6.44848425⋅10−5, 6.06814747⋅10−5, 6.19977506⋅10−5. It returns iteration-budget-exhausted after eight corrections, with one Jacobian assembly/factorization and eight linear solves. The chord iterates include negative y2 values; no positivity or chemistry invariant is enforced by these unconstrained corrections.

Facts & Assumptions

Given: The field and initial state in ## Example, one backward Euler step with h=10−3, y(0)=y0, tolerance 10−12, the stated correction budgets and refresh periods, and binary64 partial-pivoting elimination.

[F1]

Implicit residuals and their update and derivative units: an implicit update residual is the equation's left side minus its right side, in update units.

[F2]

Finite-budget Newton and chord solves with scheduled factorization reuse: updated Newton refreshes the Jacobian every correction; chord mode retains its factorization to the scheduled refresh; a finite solve reports residual and budget status without asserting forward accuracy.

[F3]

Implicit stiff time stepping with a branch and residual ledger: record Jacobian refreshes, factorizations, solves, residuals, and finite solver status; the work record is not an accuracy theorem.

[F4]

Continuously differentiable maps, local inverses, and local diffeomorphisms: a C1 map is totally differentiable at every point and its derivative-matrix entries are continuous.

[F5]

The Jacobian matrix of partial derivatives and the gradient in the scalar-valued case: the Jacobian matrix consists of the first partial derivatives of the component functions.

[F6]

The Euclidean inner product ⟨x,y⟩=∑k<nxkyk on Rn: ∥v∥2=∑ivi2.

Verification

1.1F1F2F4F5algebra

Differentiating the polynomial components gives the displayed Df by [F5]. For an increment v, the remainder f(y+v)−f(y)−Df(y)v is (104v2v3,−104v2v3−3⋅107v22,3⋅107v22)T, whose Euclidean norm is bounded by C∥v∥22; hence Df(y) is the total derivative and its affine entries are continuous. Thus JG=I−hDf; by [F4], both f and G(y)=y−y0−hf(y) are C1, as required by [F2]. Summing the components of f cancels all terms, so a root satisfies ∑i(yi−y0,i)=0 and preserves total concentration.

1.2F1F6algebra

At the start, f(y0)=(−0.04,0.04,0)T, so G(y0)=(0.00004,−0.00004,0)T and ∥G(y0)∥2=2(4⋅10−5)=5.65685425⋅10−5>10−12 by [F6]. Thus neither mode returns at count zero.

2.1F2F3step 1.2algebra

Applying the stated Newton correction formula with the displayed Jacobian and binary64 partial-pivoting elimination gives the Newton residual sequence in the Numerical record. It first falls below 10−12 at count five; the residuals at counts zero through four exceed the tolerance. Since the budget is 12, this binary64 implementation returns root after five corrections. Each correction refreshes and factors one Jacobian, then solves once, giving five assemblies/factorizations and five solves.

3.1F2F3step 1.2algebra∎

With chord refresh period eight, [F2] refreshes at count zero and retains that factorization for corrections zero through seven. The residuals at counts zero through eight all exceed 10−12, and the budget is eight, so this binary64 implementation returns iteration-budget-exhausted. This uses one assembly/factorization and eight linear solves. The mode is unconstrained, so negative intermediate second components do not violate its domain R3.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

36 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