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

A capacitor-resistor circuit has one consistent algebraic current

Example

Let $v (t)$ be the capacitor voltage and $i (t)$ the series current in a circuit with capacitance $C > 0$ , resistance $R > 0$ , and source voltage $u (t)$ . Kirchhoff's current law and voltage law give the semi-explicit system

C v^{'} = i, 0 = R i + v - u (t) .

The algebraic equation determines $i = (u (t) - v) / R$ . With $C = R = 1$ , $u (t) = 1$ , and $v (0) = 0$ , the consistent initial current is $i (0) = 1$ , and the reduced ODE is $v^{'} = 1 - v$ . One backward-Euler step of size $h$ gives

v_{1} = \frac{h}{1 + h}, i_{1} = \frac{1}{1 + h} .

For $h = 1$ , this is $(v_{1}, i_{1}) = (1 / 2, 1 / 2)$ . The pair $v (0) = 0, i (0) = 0$ is inconsistent for this same source.

Facts & Assumptions

Given: $C, R > 0$ , the displayed circuit equations, the constant source and initial voltage in the example.

[F1]

Semi-explicit index-one DAEs and consistent initial data: a consistent initial pair must satisfy the algebraic equation at the initial time.

[F2]

Backward Euler step equation and algebraic residual: for an ODE $Y^{'} = f (t, Y)$ , backward Euler uses the endpoint equation $Y_{1} = Y_{0} + h f (t_{1}, Y_{1})$ .

[F3]

A regular index-one DAE has a local reduced ODE branch: if the derivative of the algebraic equation with respect to its algebraic variable is invertible, it defines a local branch and reduced ODE.

Verification

1.1givenF3algebra

In the circuit, $f (t, v, i) = i / C$ and $g (t, v, i) = R i + v - u (t)$ , so $g_{i} = R \neq 0$ . Thus the selected algebraic branch is $i = (u (t) - v) / R$ , and the reduced ODE follows from [F3].

1.2givenF1algebra

For $C = R = 1$ , $u (0) = 1$ , and $v_{0} = 0$ , the algebraic residual at $i_{0} = 1$ is $1 \cdot 1 + 0 - 1 = 0$ , whereas it is $1 \cdot 0 + 0 - 1 = - 1$ at $i_{0} = 0$ . By [F1], the first pair is consistent and the second cannot be the initial value of a solution.

2.1givenF2step 1.1algebra

Apply [F2] to the reduced ODE $v^{'} = 1 - v$ from step 1.1. With $v_{0} = 0$ and $h > 0$ , the endpoint equation $v_{1} = h (1 - v_{1})$ gives $v_{1} = h / (1 + h)$ . Recovering the current from the algebraic branch gives $i_{1} = 1 - v_{1} = 1 / (1 + h)$ , so $v_{1} - v_{0} = h i_{1}$ and $i_{1} + v_{1} = 1$ . For $h = 1$ , both values equal $1 / 2$ .

3.1givenstep 1.2step 2.1algebra∎

The exact reduced solution $v (t) = 1 - e^{- t}$ , $i (t) = e^{- t}$ satisfies $v^{'} = i$ and $i + v = 1$ , and it starts at the consistent pair $(0, 1)$ . Thus the example's initialization and one-step calculations satisfy both circuit equations.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

7 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

Ernst Hairer and Gerhard Wanner, Solving Ordinary Differential Equations II, Chapter VI §VI.1, Solving Index 1 Problems, pp. 372–381 (standard reference, not scraped)
Kendall Atkinson, Weimin Han, and David Stewart, Numerical Solution of Ordinary Differential Equations, Chapter 10 §10.0 (standard reference, not scraped)