Physics theoremStatement: AI-adaptedProof: AI-adapted

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.

Restricted RL decay and LC oscillation under the adopted circuit model

Physical scope

Conditional scalar RL/LC dynamics of the adopted lumped model, with arbitrary positive model parameters, endpoint intervals and explicit singleton candidate jets retained. Algebraic bookkeeping is choice-free; the optional identification with a specified geometric capacitor $C = C_{11}$ carries full AC and the bounded smooth conductor hypotheses of its supplier, and the frozen magnetic realization separately carries the compact-profile and ${A C}_{ω}$ premises of the linkage theorem. Neither frozen realization is a time-dependent full Maxwell solution; no radiation or distributed effect is included.

Statement

Assume the lumped circuit model and its units as in Lumped circuit approximation: branch data, terminal laws and the declared quasistatic regime and Framework-local SI units, the vacuum constants and the exact/measured status of their values. Let $J \subseteq R$ be an interval (Intervals of $R$ : the nine order-convex forms, nondegeneracy, and length) and let $t_{0} \in J$ . For a nondegenerate $J$ , derivatives are domain-relative, with one-sided values at included endpoints, in the sense of First-order systems, initial value problems, and solutions on intervals; the functions constructed below also admit the stated $C^{k}$ open-neighbourhood extensions. If $J = {t_{0}}$ , the formulas specify the initial values and the jets of the explicitly constructed extensions below, rather than an intrinsic derivative of a singleton restriction. The RL solution, the LC candidate and the bookkeeping-energy algebra use no choice principle. Only the optional geometric capacitor identification in (b) assumes full Axiom of Choice (The Axiom of Choice) and its ${A C}_{ω}$ consequence (The Axiom of Countable Choice ( ${A C}_{ω}$ )), exactly as Capacitance and energy for specified linear conductor geometry requires. The inductive energy is that of Restricted inductor energy LI^2/2 and its identification with the frozen magnetic field energy.

(a) [RL circuit] Let $L > 0$ and $R \geq 0$ be constants and let $V : J \to R$ be continuous. Then the initial value problem $L \dot{I} (t) + R I (t) = V (t), I (t_{0}) = I_{0} \in R,$ has exactly one $C^{1}$ solution on every nondegenerate $J$ , namely $I (t) = \exp ⁣ (- \frac{R (t - t_{0})}{L}) [I_{0} + \frac{1}{L} \int_{t_{0}}^{t} \exp ⁣ (\frac{R (s - t_{0})}{L}) V (s) d s],$ and along it the inductive bookkeeping energy satisfies the power identity $\frac{d}{d t} (\frac{1}{2} L I (t)^{2}) = L \dot{I} (t) I (t) = V (t) I (t) - R I (t)^{2},$ i.e. the terminal power splits into the rate of change of the inductive energy and the Ohmic term $R I^{2}$ . (For $R = 0$ the same formula reduces to $I = I_{0} + L^{- 1} \int_{t_{0}}^{t} V$ .) For $J = {t_{0}}$ its unique restriction is $I (t_{0}) = I_{0}$ ; the canonical extension obtained using the constant source $V (t_{0})$ has jet $\dot{I} (t_{0}) = (V (t_{0}) - R I_{0}) / L$ and satisfies the same power algebra. No uniqueness of arbitrary extension germs is asserted.

(b) [LC oscillation] Let $L > 0$ , $C > 0$ and set $Ω : = (L C)^{- 1 / 2} > 0$ , $z_{0} : = Q_{0} - i I_{0} / Ω$ , $w (t) : = z_{0} \exp (i Ω (t - t_{0}))$ with the complex exponential of The complex exponential by its power series, and $Q (t) : = Re w (t)$ . Then $Q$ is of class $C^{2}$ on $J$ , $Q (t_{0}) = Q_{0}$ , $Q^{'} (t_{0}) = I_{0}$ , and $L Q^{''} (t) + \frac{Q (t)}{C} = 0 on J;$ equivalently, with the real trigonometric functions of Euler's formula: $\exp (i θ) = \cos θ + i \sin θ$ for every real $θ$ , $Q (t) = Q_{0} \cos (Ω (t - t_{0})) + \frac{I_{0}}{Ω} \sin (Ω (t - t_{0})) .$ Moreover the total bookkeeping energy $E (t) : = \frac{1}{2} L Q^{'} (t)^{2} + \frac{Q (t)^{2}}{2 C}$ satisfies $E^{'} (t) = Q^{'} (t) (L Q^{''} (t) + Q (t) / C) = 0$ on $J$ , hence $E$ is constant with value $\frac{1}{2} L I_{0}^{2} + \frac{Q_{0}^{2}}{2 C}$ : the two terms are the adopted capacitive and inductive bookkeeping energies, the latter as in Restricted inductor energy LI^2/2 and its identification with the frozen magnetic field energy(a), so in the lossless loop their sum is conserved. For the additional geometric identification, explicitly choose the fixed compact separated conductor arrangement of Capacitance and energy for specified linear conductor geometry with bounded smooth ambient domain, connected vacuum, grounded outer boundary, zero volume source and its unit-Dirichlet solutions; drive only conductor 1 and ground the others, set the circuit parameter $C$ equal to that arrangement's $C_{11} > 0$ , and at each time set $V_{1} = Q / C_{11}$ . Under full AC that supplier gives the frozen electrostatic field energy $Q^{2} / (2 C_{11})$ . An arbitrary declared $C > 0$ is model data and is not automatically the capacitance of a particular arrangement. Any magnetic field-energy identification likewise requires the extra smooth-profile linkage realization of Restricted inductor energy LI^2/2 and its identification with the frozen magnetic field energy(b), under its ${A C}_{ω}$ hypothesis. Neither frozen realization is an asserted time-dependent full Maxwell solution. At a singleton time the entire LC candidate supplies the jets $\dot{Q} = I_{0}$ , $\ddot{Q} = - Q_{0} / (L C)$ and the same constant energy.

(c) [Scope] both statements are consequences of the expressly adopted circuit reduction, with the sign conventions and relations of Lumped circuit approximation: branch data, terminal laws and the declared quasistatic regime; they assert no general network completeness, no derivation from the full time-dependent Maxwell system, no radiation or distributed-element effect and no empirical claim.

Facts & Assumptions

Given: Assume the lumped circuit data of Lumped circuit approximation: branch data, terminal laws and the declared quasistatic regime and the units of Framework-local SI units, the vacuum constants and the exact/measured status of their values, an interval $J$ with $t_{0} \in J$ , constants $L > 0$ , $R \geq 0$ in (a) and $C > 0$ in (b), a continuous source $V : J \to R$ , and the initial data $I_{0}, Q_{0} \in R$ . For clause (b)'s geometric identification assume full $A C$ with its ${A C}_{ω}$ consequence.

[A1]

The Axiom of Choice states that every family of nonempty sets has a choice function. (The Axiom of Choice).

[A2]

Countable Choice, written ${A C}_{ω}$ , states that every sequence of nonempty sets has a choice function. (The Axiom of Countable Choice ( ${A C}_{ω}$ )).

[F1]

The adopted lumped model carries the Faraday branch relation $V = L \dot{I}$ for an inductive branch, the capacitive branch relation $V = C^{- 1} Q$ (in the scalar case $V = Q / C$ ), the resistive branch relation $V = R I$ as the circuit form of the Ohmic branch of the material model, and Kirchhoff's loop voltage balance around each independent loop; the matrices and terminal data are declared model data, not derived from the vacuum Maxwell equations. (Lumped circuit approximation: branch data, terminal laws and the declared quasistatic regime).

[F2]

A subset of $R$ is an interval when it has one of the nine order-convex forms of the definition; in particular intervals are order-convex, nondegenerate intervals have at least two elements, and a nondegenerate interval contains the two-point set ${u, v}$ for suitable $u < v$ . (Intervals of $R$ : the nine order-convex forms, nondegeneracy, and length).

[F3]

Let $I \subseteq R$ be order-convex with at least two elements, let $x_{0} \in I$ and let $p, q : I \to R$ be continuous. The initial value problem $y^{'} + p y = q$ , $y (x_{0}) = y_{0}$ , has exactly one solution on $I$ , namely $y (x) = \exp (- P (x)) (y_{0} + \int_{x_{0}}^{x} \exp (P (t)) q (t) d t)$ with $P (x) = \int_{x_{0}}^{x} p (t) d t$ . (A scalar first-order linear ODE has a unique solution given by the integrating-factor formula).

[F4]

A solution of the first-order system $x^{'} = F (t, x (t))$ with $x (t_{0}) = x_{0}$ on an interval $I$ is a function $x : I \to R^{n}$ with $t_{0} \in I$ , differentiable on $I$ in the domain-relative sense, endpoints of $I$ using one-sided, domain-relative derivatives, and satisfying the equation and initial condition. (First-order systems, initial value problems, and solutions on intervals).

[F5]

If $f, g$ are differentiable at a point of their common domain and $α \in R$ , then $f + g$ , $α f$ and $f g$ are differentiable there with the sum, scalar and product rules; in particular $\frac{d}{d t} \frac{1}{2} L f (t)^{2} = L f (t) f^{'} (t)$ . (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$ ).

[F6]

Sums, scalar multiples, products, absolute values and (where defined) quotients of continuous functions are continuous, and every constant function and the identity are continuous. (Sums, scalar multiples, products, absolute values, maxima, minima and quotients with nonvanishing denominator of continuous functions are continuous, as are constants, the identity and every polynomial function).

[F7]

The complex exponential is $\exp z = \sum_{n \geq 0} z^{n} / n!$ , convergent for every $z \in C$ . (The complex exponential by its power series).

[F8]

The complex exponential is entire and $\exp^{'} (z) = \exp z$ for every $z \in C$ . (The complex exponential is entire and its complex derivative is itself).

[F9]

For $U \subseteq C$ open and $f : U \to C$ , the following are equivalent: $f$ is complex differentiable at $a$ ; under $C ≅ R^{2}$ the map $f$ is real totally differentiable at $a$ and $D f (a)$ is multiplication by a complex number; and the Cauchy--Riemann equations hold at $a$ with real total differentiability. When these hold, $f^{'} (a) = \partial_{z} f (a)$ . (Complex differentiability is equivalent to real total differentiability together with a complex-linear derivative, with $\partial_{\overset{ˉ}{z}} f = 0$ , or with the Cauchy–Riemann equations).

[F10]

Complex derivatives obey the sum, scalar, product and quotient rules, the derivative of a constant is $0$ , and the derivative of the identity is $1$ . (Linearity, product, reciprocal, and quotient rules for complex derivatives).

[F11]

If $f$ is complex differentiable at $a$ and $g$ at $f (a)$ , then $g \circ f$ is complex differentiable at $a$ with $(g \circ f)^{'} (a) = g^{'} (f (a)) f^{'} (a)$ . (The chain rule for complex derivatives).

[F12]

If $f$ is totally differentiable at $a$ and $g$ 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)$ ).

[F13]

For every real $θ$ , $\exp (i θ) = \cos θ + i \sin θ$ with the real cosine and sine. (Euler's formula: $\exp (i θ) = \cos θ + i \sin θ$ for every real $θ$ ).

[F14]

The complex trigonometric functions restrict to their real power-series counterparts on the real axis. (The exponential formulas, real restrictions, and trigonometric-hyperbolic dictionary over $C$ ).

[F15]

If $I \subseteq R$ is order-convex, $f : I \to R$ is continuous on $I$ and differentiable at every interior point of $I$ with $f^{'} (x) = 0$ there, then $f$ is constant on $I$ . (A function continuous on an interval $I$ whose derivative vanishes at every interior point of $I$ is constant on $I$ ; consequently two such functions with the same derivative differ by a constant).

[F16]

For clause (b) of the Statement, the inductive bookkeeping energy and its smooth-profile realization are those of Restricted inductor energy LI^2/2 and its identification with the frozen magnetic field energy: the terminal energy $\int ⟨ V, I ⟩$ is the change of $\frac{1}{2} L I^{2}$ for constant symmetric $L$ , and for a smooth compact conserved-profile realization it is the change of the frozen field energy $\frac{1}{2 μ_{0}} \int ∣ B ∣^{2}$ . (Restricted inductor energy LI^2/2 and its identification with the frozen magnetic field energy).

[F17]

The SI units are those of the framework: $V$ in volts, $I$ in amperes, $Q$ in coulombs, $t$ in seconds, $L$ in henries and $C$ in farads. (Framework-local SI units, the vacuum constants and the exact/measured status of their values).

[L1]

The optional geometric identification clause uses Capacitance and energy for specified linear conductor geometry: for the fixed compact separated conductor arrangement with bounded smooth ambient domain of its clause (f), its clause (c) gives the field-energy identity $U (V) = \frac{ε_{0}}{2} \int_{Ω_{v}} ∣ \nabla φ^{V} ∣^{2} d λ_{3} = \frac{1}{2} V^{T} C V = \frac{1}{2} \sum_{j} V_{j} Q_{j} (V)$ , valid under full AC and its stated Dirichlet solvability hypotheses, and its clause (d) gives, with only conductor $1$ driven and the others grounded, $C_{11} > 0$ , $Q_{1} = C_{11} V_{1}$ and the frozen electrostatic field energy $U = \frac{1}{2} C_{11} V_{1}^{2} = Q_{1}^{2} / (2 C_{11})$ . This consumer relies on exactly that clause with $C = C_{11}$ and no independent derivation of the electrostatic energy is substituted.

Proof

technique · direct

1.1F2F3F4F6algebracases

(a) Assume first that $J$ has at least two elements. Put $p : = R / L$ , a constant of class $C^{1}$ , and $q : = V / L$ , continuous on $J$ by [F6]; $J$ is order-convex with at least two elements by [F2]. With $P (x) : = \int_{t_{0}}^{x} p = \frac{R}{L} (x - t_{0})$ one has $\exp (- P (x)) = \exp (- \frac{R (x - t_{0})}{L})$ and $\exp (P (s)) = \exp (\frac{R (s - t_{0})}{L})$ , so the unique solution supplied by [F3] is exactly the displayed $I$ . The ODE gives $\dot{I} = (V - R I) / L$ , continuous on $J$ . At each included finite endpoint extend $I$ to the outer side by the affine function with that endpoint value and slope; its derivative matches the one-sided ODE value, giving a $C^{1}$ extension to an open interval containing $J$ . Its derivative on $J$ is the domain-relative derivative of [F4] (one-sided at included endpoints), and the uniqueness is the uniqueness assertion of [F3], which is the uniqueness of the $C^{1}$ solution in the sense of [F4]. If $J = {t_{0}}$ , the restriction of any solution is $I_{0}$ by [F4]; choosing the constant extension $V \equiv V (t_{0})$ on an open interval and applying the already-proved nondegenerate case there produces a $C^{1}$ extension of the candidate whose jet at $t_{0}$ is obtained by substituting $t = t_{0}$ into the differential equation, $\dot{I} (t_{0}) = (V (t_{0}) - R I_{0}) / L$ , and no other extension is distinguished.

1.2F7F8F9F10F11F12F13F14algebracases

(b) Define the entire function $G (z) : = z_{0} \exp (i Ω (z - t_{0}))$ on $C$ . By [F10] and [F11], applied to the affine map $z \mapsto i Ω (z - t_{0})$ (derivative $i Ω$ ) and to [F8], $G$ is complex differentiable with $G^{'} (z) = i Ω G (z)$ for every $z$ ; differentiating once more gives $G^{''} = (i Ω)^{2} G = - Ω^{2} G$ . The function $w$ of the Statement is the restriction of $G$ to the real interval $J$ , so by [F9] and the real chain rule [F12] it is real differentiable with $w^{'} (t) = i Ω w (t)$ and $w^{''} (t) = - Ω^{2} w (t)$ for every $t \in J$ ; taking real parts, $Q = Re w$ is of class $C^{2}$ with $Q^{'} (t) = Re w^{'} (t)$ and $Q^{''} (t) = Re w^{''} (t)$ , because the real part is real-linear. Hence $Q^{''} = - Ω^{2} Q$ , which is $L Q^{''} + Q / C = 0$ since $Ω^{2} = 1 / (L C)$ by definition. At $t_{0}$ : $w (t_{0}) = z_{0}$ gives $Q (t_{0}) = Re z_{0} = Q_{0}$ , and $w^{'} (t_{0}) = i Ω z_{0} = i Ω Q_{0} + I_{0}$ gives $Q^{'} (t_{0}) = I_{0}$ . Euler's formula [F13] expands $\exp (i Ω (t - t_{0})) = \cos Ω (t - t_{0}) + i \sin Ω (t - t_{0})$ , and multiplying out $w = z_{0} \exp (i Ω (t - t_{0}))$ gives $Re w = Q_{0} \cos Ω (t - t_{0}) + (I_{0} / Ω) \sin Ω (t - t_{0})$ , with the real trigonometric functions of [F13] and the real restriction recorded in [F14]. For $J = {t_{0}}$ the same formulas are evaluated at $t_{0}$ , the entire function supplying the jets $\dot{Q} (t_{0}) = I_{0}$ and $\ddot{Q} (t_{0}) = - Ω^{2} Q_{0} = - Q_{0} / (L C)$ by the same computation, so the LC candidate needs no separate singleton convention.

2.1F1F5step 1.1algebra

(a) Along the solution of step 1.1 the function $t \mapsto \frac{1}{2} L I (t)^{2}$ is differentiable at every interior point of $J$ (and one-sidedly at included endpoints) by [F5], with derivative $L I \dot{I}$ ; substituting the circuit equation $L \dot{I} = V - R I$ gives $L I \dot{I} = V I - R I^{2}$ , which is the power identity.

2.2A1A2F16L1F5F6F15step 1.2algebracases

(b) Define $E (t) : = \frac{1}{2} L Q^{'} (t)^{2} + \frac{Q (t)^{2}}{2 C}$ ; by [F6] and step 1.2 the functions $Q$ and $Q^{'}$ are continuous, so $E$ is continuous on $J$ , and at every interior point of $J$ the product and scalar rules of [F5] give $E^{'} = L Q^{'} Q^{''} + Q Q^{'} / C = Q^{'} (L Q^{''} + Q / C) = 0$ by the equation of step 1.2. By [F15], $E$ is constant on $J$ , and its value is $E (t_{0}) = \frac{1}{2} L I_{0}^{2} + \frac{Q_{0}^{2}}{2 C}$ by the initial values of step 1.2. The first summand is the inductive bookkeeping energy of [F16], and for the optional geometric identification of the Statement the second summand is the frozen electrostatic field energy supplied by the declared clause of [L1] under full AC and the stated conductor arrangement, with $C = C_{11}$ and $V_{1} = Q / C_{11}$ ; the magnetic realization of the inductive term is the separate smooth-profile clause of [F16], under its ${A C}_{ω}$ premise. For $J = {t_{0}}$ the constant-energy display is the value at $t_{0}$ supplied by step 1.2, so no derivative of a singleton restriction is used.

3.1A1A2F16step 1.1step 1.2step 2.1step 2.2algebra

The full choice hypothesis of the geometric identification is [A1], and the inductive realization of [F16] carries the ${A C}_{ω}$ of [A2]; full AC yields it, because for a sequence $(X_{n})_{n \in N}$ of nonempty sets the family ${X_{n} : n \in N}$ of its values consists of nonempty sets, so [A1] provides a choice function $g$ on that family and $n \mapsto g (X_{n})$ is a choice function for the sequence, as [A2] requires. Hence clause (b) is available under its stated hypotheses, and the RL and LC algebra of steps 1.1, 1.2, 2.1 and 2.2 is choice-free and uses neither [A1] nor [A2].

4.1F1F17step 1.1step 1.2step 2.1step 2.2step 3.1∎

Clauses (a)-(c) are established: step 1.1 and step 2.1 give the existence, uniqueness, formula and power identity of (a); step 1.2 and step 2.2 give the solution, initial values, cosine-sine form, energy identity and conservation of (b), with the geometric identification delegated to [L1]; step 3.1 accounts for the choice use. The units are [F17]; no general network completeness, no full time-dependent Maxwell solution, no radiation or distributed-element effect and no empirical claim is asserted, and both statements are consequences of the expressly adopted relations of [F1].

Source notes

Fitzpatrick §7.5-7.6, printed pp. 225-234, writes the RL equation and the LCR circuit equation with the ideal element relations; Griffiths §7.2.3, printed pp. 310-317, records the battery-plus-RL exponential approach with time constant $L / R$ ; Tong §4.1.3, printed pp. 74-77, presents resistance as an additional material input in the circuit treatment. The RL solution is proved from the published integrating-factor theorem; the lossless LC candidate is verified by explicit complex-exponential differentiation with the real cosine-sine form displayed through Euler's formula, rather than through a real-trigonometric derivative supplier outside this page's declared prerequisite closure; and the optional capacitive identification is referred to its own supplier with its exact conductor and Choice hypotheses recorded. No numerical value, measurement or error bound is asserted.

Restricted RL decay and LC oscillation under the adopted circuit model

Statement

Facts & Assumptions

Proof

Source notes

Depends on

Dependency tree · 2 levels

Sources