LemmaStatement: Literature-sourcedProof: AI-generatedPipeline-generatedprecheck passjudge pass (gpt-6-luna)

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 ARS(2,2,2) coefficients satisfy the coupled second-order identities

Statement

For $γ = 1 - 1 / \sqrt{2}$ and $δ = - 1 / \sqrt{2}$ in The ARS(2,2,2) additive tableau and its three stages, one has $γ > 0$ and $δ = 1 - \frac{1}{2 γ}, γ (1 - δ) = \frac{1}{2}, γ (2 - γ) = \frac{1}{2}, γ (1 - γ - δ) = \frac{1}{2} - γ^{2} .$

Facts & Assumptions

Given: The coefficient definitions in the statement.

[F1]

The ARS(2,2,2) additive tableau and its three stages: $γ = 1 - 1 / \sqrt{2}$ and $δ = - 1 / \sqrt{2}$ .

[F2]

Square roots exist: a unique $\sqrt{a} \geq 0$ with $(\sqrt{a})^{2} = a$ ; the positives are ${x^{2} : x \neq 0}$ : $r : = \sqrt{2}$ is nonnegative and $r^{2} = 2$ .

[F3]

Squaring is monotone on the nonnegatives: squaring is strictly increasing on nonnegative reals.

[F4]

Inverses of positives are positive, and reciprocation reverses order: if $0 < a < b$ , then $0 < b^{- 1} < a^{- 1}$ .

Proof

1.1F2F3F4algebra

Let $r = \sqrt{2}$ . If $r \leq 1$ , then $0 \leq r \leq 1$ and [F3] gives $r^{2} \leq 1$ , contradicting $r^{2} = 2$ from [F2]; hence $r > 1$ . Applying [F4] to $0 < 1 < r$ gives $0 < 1 / r < 1$ , so $γ = 1 - 1 / r > 0$ .

2.1F1F2step 1.1algebra

By [F1] and $γ = (r - 1) / r$ from step 1.1, $1 - 1 / (2 γ) = 1 - r / (2 (r - 1)) = (r - 2) / (2 (r - 1))$ . Since $r^{2} = 2$ , $r (r - 2) = 2 - 2 r = - 2 (r - 1)$ ; dividing by the nonzero $2 r (r - 1)$ gives $(r - 2) / (2 (r - 1)) = - 1 / r = δ$ .

2.2F1F2step 1.1algebra

Using $δ = - 1 / r$ and $γ = (r - 1) / r$ , $γ (1 - δ) = ((r - 1) / r) (1 + 1 / r) = (r^{2} - 1) / r^{2} = 1 / 2$ , and $γ (2 - γ) = 1 - (1 - γ)^{2} = 1 - 1 / r^{2} = 1 / 2$ .

3.1step 2.1step 2.2algebra∎

The identity in step 2.1 gives $γ (1 - γ - δ) = γ (1 / (2 γ) - γ) = 1 / 2 - γ^{2}$ . This proves all coefficient identities.

Depends on

Used by

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

Uri M. Ascher, Steven J. Ruuth, and Raymond J. Spiteri, Implicit-explicit Runge-Kutta methods for time-dependent partial differential equations (standard reference, not scraped)
Lorenzo Pareschi and Giovanni Russo, Implicit-explicit Runge-Kutta schemes and applications to hyperbolic systems with relaxation (standard reference, not scraped)