ExampleConstruction: AI-adaptedVerification: AI-adaptedjudge pass (gpt-6.1-sol)

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.

Exponential RL response under a constant terminal voltage

Physical scope

The exponential transient of the scalar RL circuit of the adopted lumped model under a constant source voltage and constant positive $L$ and $R$ , with time constant $L / R$ . It carries the model idealisations (fixed geometry, ideal elements, no radiation or distributed effects) and contains no measurement or empirical claim.

Example

In the RL branch of Restricted RL decay and LC oscillation under the adopted circuit model with the declared units of Framework-local SI units, the vacuum constants and the exact/measured status of their values, let the source voltage be the constant $V_{0} \in R$ , let $R > 0$ and $L > 0$ , let $t_{0} \in J$ and $I_{0} \in R$ , with $J$ an interval and derivatives read in the model's domain-relative convention, through the stated $C^{1}$ open-neighbourhood extension for a non-open $J$ . For nondegenerate $J$ the unique $C^{1}$ solution of $L \dot{I} + R I = V_{0}$ , $I (t_{0}) = I_{0}$ , is $I (t) = \frac{V_{0}}{R} + (I_{0} - \frac{V_{0}}{R}) \exp ⁣ (- \frac{R (t - t_{0})}{L}), t \in J .$ In particular $I (t) - V_{0} / R = (I_{0} - V_{0} / R) \exp (- R (t - t_{0}) / L)$ and hence $∣ I (t) - V_{0} / R ∣ = ∣ I_{0} - V_{0} / R ∣ \exp (- R (t - t_{0}) / L)$ for every $t \in J$ , with time constant $τ = L / R$ ; $I \equiv V_{0} / R$ is the unique stationary solution (an extension with zero derivative, also in the singleton convention); if $J$ is unbounded above, then $I (t) \to V_{0} / R$ as $t \to + \infty$ along $J$ ; and the transient part is the free decay $\exp (- R (t - t_{0}) / L)$ of the initial deviation $I_{0} - V_{0} / R$ . For $J = {t_{0}}$ the restriction is $I (t_{0}) = I_{0}$ and the jets are those of the same formula read through the stated extension, giving $\dot{I} (t_{0}) = (V_{0} - R I_{0}) / L$ . The computation is conditional on the adopted lumped model, constant elements and fixed geometry; no measurement is involved.

Verification

technique · explicit differentiation of the candidate, with uniqueness inherited from the RL theorem

Given: The RL branch data of the adopted lumped model with constants $V_{0} \in R$ , $R > 0$ , $L > 0$ , an interval $J$ with $t_{0} \in J$ and initial value $I_{0} \in R$ .

[F1] In the RL branch let $L > 0$ , $R \geq 0$ and let $V : J \to R$ be continuous. Then the initial value problem $L \dot{I} + R I = V$ , $I (t_{0}) = I_{0}$ , has exactly one $C^{1}$ solution on every nondegenerate interval $J$ , namely $I (t) = \exp (- R (t - t_{0}) / L) [I_{0} + L^{- 1} \int_{t_{0}}^{t} \exp (R (s - t_{0}) / L) V (s) d s]$ ; for $J = {t_{0}}$ the restriction is $I (t_{0}) = I_{0}$ and the canonical extension for the constant source $V (t_{0})$ has jet $\dot{I} (t_{0}) = (V (t_{0}) - R I_{0}) / L$ ; the RL solution uses no choice principle. (Restricted RL decay and LC oscillation under the adopted circuit model).

[F2] The real exponential is $C^{\infty}$ and $\exp^{'} = \exp$ . (The exponential function is smooth and $(\exp)^{'} = \exp$ ).

[F3] Sums, scalar multiples and products of differentiable functions are differentiable, with the sum, scalar and product rules; the derivative of a constant is $0$ and the derivative of the identity is $1$ , since their difference quotients are respectively $0$ and $1$ . (Sums, scalar multiples, products and quotients: $(f + g)^{'} (c) = f^{'} (c) + g^{'} (c)$ , $(α f)^{'} (c) = α f^{'} (c)$ , $(f g)^{'} (c) = f^{'} (c) g (c) + f (c) g^{'} (c)$ , and $(f / g)^{'} (c) = (f^{'} (c) g (c) - f (c) g^{'} (c)) / g (c)^{2}$ when $g (c) \neq 0$ ).

[F4] If $f$ is totally differentiable at $a$ and $g$ is totally differentiable at $f (a)$ , then $g \circ f$ is totally differentiable at $a$ with $D (g \circ f) (a) = D g (f (a)) \circ D f (a)$ . (The chain rule for total derivatives: $D (g \circ f) (a) = D g (f (a)) \circ D f (a)$ ).

[F5] $\exp (x) \to + \infty$ as $x \to + \infty$ and $\exp (x) \to 0$ as $x \to - \infty$ . (The exponential tends to $+ \infty$ at $+ \infty$ and to $0$ at $- \infty$ ).

[F6] For every real $x$ , $\exp (x) > 0$ and $\exp (- x) = 1 / \exp (x)$ . (The exponential is positive and satisfies $\exp (- x) = 1 / \exp (x)$ ).

[F7] The SI units are those of the framework: $V$ in volts, $I$ in amperes, $t$ in seconds, $R$ in ohms and $L$ in henries. (Framework-local SI units, the vacuum constants and the exact/measured status of their values).

[F8] A subset of $R$ is an interval when it has one of the nine order-convex forms of the definition; an interval is unbounded above exactly when it contains a ray $[r, + \infty)$ . (Intervals of $R$ : the nine order-convex forms, nondegeneracy, and length).

1.1F2F3F4algebra

Define the candidate $φ (t) : = \frac{V_{0}}{R} + (I_{0} - \frac{V_{0}}{R}) \exp (- \frac{R (t - t_{0})}{L})$ on $J$ . The function $t \mapsto - \frac{R (t - t_{0})}{L}$ is affine with derivative $- \frac{R}{L}$ by [F3], and $\exp^{'} = \exp$ by [F2], so the chain rule [F4] gives $φ^{'} (t) = (I_{0} - \frac{V_{0}}{R}) (- \frac{R}{L}) \exp (- \frac{R (t - t_{0})}{L}) = - \frac{R}{L} (φ (t) - \frac{V_{0}}{R})$ . Therefore $L φ^{'} (t) + R φ (t) = - R (φ (t) - \frac{V_{0}}{R}) + R φ (t) = V_{0}$ identically, and $φ (t_{0}) = \frac{V_{0}}{R} + (I_{0} - \frac{V_{0}}{R}) = I_{0}$ .

1.2F3algebra

Stationary solutions: if $I \equiv c$ is constant, then $L \dot{I} + R I = R c$ , so the equation $L \dot{I} + R I = V_{0}$ holds exactly when $c = V_{0} / R$ ; since $R > 0$ there is exactly one such constant, namely $I \equiv V_{0} / R$ .

1.3F5F8algebra

Limit statement: if $J$ is unbounded above, then for $t \in J \cap [t_{0}, + \infty)$ the argument $- \frac{R (t - t_{0})}{L}$ satisfies $- \frac{R (t - t_{0})}{L} \to - \infty$ as $t \to + \infty$ because $R / L > 0$ , so [F5] gives $\exp (- \frac{R (t - t_{0})}{L}) \to 0$ and hence $I (t) \to V_{0} / R$ along that ray; the time constant is $τ : = L / R$ , so the decay factor is $\exp (- (t - t_{0}) / τ)$ .

1.4F6algebra

Deviation identity: subtracting $V_{0} / R$ from the displayed formula gives $I (t) - V_{0} / R = (I_{0} - \frac{V_{0}}{R}) \exp (- \frac{R (t - t_{0})}{L})$ ; since $\exp (x) > 0$ for real $x$ by [F6], taking absolute values preserves the exponential factor, so $∣ I (t) - V_{0} / R ∣ = ∣ I_{0} - \frac{V_{0}}{R} ∣ \exp (- \frac{R (t - t_{0})}{L})$ for every $t \in J$ .

2.1F1step 1.1algebracases

Identification of the solution: by step 1.1 the candidate $φ$ is a $C^{1}$ solution of the initial value problem (its derivative exists on all of $J$ through the stated extension convention) and by [F1] the initial value problem with the constant source $V \equiv V_{0}$ has exactly one $C^{1}$ solution on every nondegenerate $J$ ; hence the displayed $I$ equals $φ$ there and is the unique solution, and for $J = {t_{0}}$ the restriction and jets are those of [F1] with $V (t_{0}) = V_{0}$ , namely $I (t_{0}) = I_{0}$ and $\dot{I} (t_{0}) = (V_{0} - R I_{0}) / L$ .

3.1F1F7step 1.1step 1.2step 1.3step 1.4step 2.1∎

Steps 1.1-1.4 and 2.1 establish the formula, its uniqueness, the deviation identity with time constant $τ = L / R$ , the unique stationary solution, the limit behaviour on intervals unbounded above, and the singleton reading. The computation uses only the adopted lumped model and its constant positive elements, with units [F7]; no radiation, distributed-element, material or measurement claim is added, and the RL existence and uniqueness supplier is the choice-free clause (a) of [F1].

Source notes

Griffiths §7.2.3, printed pp. 310-317, records the battery-plus-RL solution $I (t) = E_{0} / R + k e^{- R t / L}$ with time constant $τ = L / R$ ; Fitzpatrick §7.5, printed pp. 225-231, writes the RL equation and its exponential approach to the steady current. The example verifies the constant-source candidate by explicit differentiation and inherits uniqueness from the RL theorem; no other current history, transient measurement or numerical value is asserted.

Exponential RL response under a constant terminal voltage

Example

Verification

Source notes

Depends on

Dependency tree · 2 levels

Sources