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

Two-circuit mutual inductance, the perfect-linkage bound and ideal-transformer limitations

Physical scope

Conditional two-circuit bookkeeping and smooth-profile realization: the reciprocal energy and instantaneous power, the exact positive-semidefinite bound $∣ M ∣ \leq \sqrt{L_{1} L_{2}}$ and the sign-correct perfect-linkage null direction for either winding orientation, the positive common-flux model and its signed reversal, and failure of a universal voltage ratio under strict linkage with accidental histories retained. No physical leakage or loss mechanism and no measurement is asserted.

Example

Assume the lumped circuit model of Lumped circuit approximation: branch data, terminal laws and the declared quasistatic regime with the units of Framework-local SI units, the vacuum constants and the exact/measured status of their values, and let $L = (\begin{array}{cc} L_{1} & M \\ M & L_{2} \end{array})$ be a constant symmetric block of its inductance matrix with $L_{1}, L_{2} > 0$ . Let $I_{1}, I_{2} : J \to R$ be $C^{1}$ currents on a nonempty interval $J$ (each extending to a $C^{1}$ map on an open interval containing $J$ , as in the model's conventions) with terminal voltages $V_{α} = \sum_{β} L_{α β} {\dot{I}}_{β}$ . Assume Countable Choice ( ${A C}_{ω}$ , The Axiom of Countable Choice ( ${A C}_{ω}$ )) for the realization and bounded-linking clauses (b), inherited from the linkage and energy suppliers.

(a) [Energy and instantaneous power] the stored inductive bookkeeping energy is $W (t) = \frac{1}{2} L_{1} I_{1} (t)^{2} + \frac{1}{2} L_{2} I_{2} (t)^{2} + M I_{1} (t) I_{2} (t),$ and $V_{1} I_{1} + V_{2} I_{2} = \dot{W}$ by part (a) of Restricted inductor energy LI^2/2 and its identification with the frozen magnetic field energy; the mutual term increases the energy for currents of the same sign and decreases it for opposite signs (as the sign of the product $I_{1} I_{2}$ indicates when $M > 0$ ).

(b) [Perfect linkage and the bound] if the two currents are realised by fixed compact smooth conserved profiles of the class of The steady-current (magnetostatic) regime, the compact smooth current class and the declared ideal noncompact models(b) with linkage matrix $L$ as in Reciprocal linkage coefficients and magnetic energy of smooth compact conserved currents, then $W (t) \geq 0$ for all currents, and evaluating the quadratic form on both $(\sqrt{L_{2}}, - \sqrt{L_{1}})$ and $(\sqrt{L_{2}}, + \sqrt{L_{1}})$ gives the bound $∣ M ∣ \leq \sqrt{L_{1} L_{2}};$ moreover if $M = s \sqrt{L_{1} L_{2}}$ with $s \in {+ 1, - 1}$ (perfect linkage), the null direction $I = (\sqrt{L_{2}}, - s \sqrt{L_{1}})$ has $J_{I} = 0$ pointwise by the vanishing clause of Reciprocal linkage coefficients and magnetic energy of smooth compact conserved currents(c).

(c) [Ideal common-flux model] if $M = \sqrt{L_{1} L_{2}}$ , choose any $Λ > 0$ in henries and set $N_{1} : = \sqrt{L_{1} / Λ}$ , $N_{2} : = \sqrt{L_{2} / Λ}$ ; then $L_{1} = Λ N_{1}^{2}$ , $L_{2} = Λ N_{2}^{2}$ and $M = Λ N_{1} N_{2}$ . Writing $Φ_{c} : = Λ (N_{1} I_{1} + N_{2} I_{2})$ for the common flux linkage, the terminal voltages are $V_{1} = N_{1} {\dot{Φ}}_{c}, V_{2} = N_{2} {\dot{Φ}}_{c}, i.e. \frac{V_{1}}{N_{1}} = \frac{V_{2}}{N_{2}} = {\dot{Φ}}_{c},$ and the stored energy is $W = Φ_{c}^{2} / (2 Λ)$ ; equivalently the induced emfs $e_{α} : = - V_{α}$ satisfy $e_{1} / N_{1} = e_{2} / N_{2} = - {\dot{Φ}}_{c}$ . Here $N_{1}, N_{2} > 0$ are dimensionless real effective winding factors, rather than asserted integer turn counts; $Φ_{c}$ has unit Wb. This is the explicitly adopted common-linkage ('ideal transformer') model with effective ratio $N_{1} : N_{2}$ .

(d) [Limitations] for an imperfect realized linkage, $∣ M ∣ < \sqrt{L_{1} L_{2}}$ , the perfect common-flux voltage ratio is not an identity for all current histories; a particular history can nevertheless satisfy that ratio accidentally (including both voltages zero). Reversing the second winding retains $s = - 1$ : with $M = s \sqrt{L_{1} L_{2}}$ put $Φ_{c} = Λ (N_{1} I_{1} + s N_{2} I_{2})$ and obtain $V_{1} / N_{1} = V_{2} / (s N_{2}) = {\dot{Φ}}_{c}$ , with the same energy $Φ_{c}^{2} / (2 Λ)$ . The positive-orientation model (c) remains as stated. Winding resistance, hysteresis and core loss, stray capacitance, magnetising current and finite permeability are outside the declared model and are not inferred from it. No measurement is involved; the statements are conditional computations in the ideal model. Regularity on a non-open interval uses the stated $C^{1}$ neighbourhood extension; if the interval is a singleton its terminal-voltage jets are those of a specified extension, not derivatives inferred from its value restriction.

Verification

technique · direct expansion, the reciprocity theorem, and an explicit derivative-vector contradiction for the strict-linkage non-identity

Given: The lumped model data, the constant symmetric block $L = (\begin{array}{cc} L_{1} & M \\ M & L_{2} \end{array})$ with $L_{1}, L_{2} > 0$ , the interval $J$ , the $C^{1}$ currents $I_{1}, I_{2}$ with open-neighbourhood extension, the terminal voltages $V_{α} = \sum_{β} L_{α β} {\dot{I}}_{β}$ and ${A C}_{ω}$ for clauses (b).

[A1] Countable Choice, written ${A C}_{ω}$ , says 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}$ : each terminal potential is the rate of change of the branch flux linkage $L I$ ; the matrix and terminal data are declared model data. (Lumped circuit approximation: branch data, terminal laws and the declared quasistatic regime).

[F2] For constant symmetric $L$ and a $C^{1}$ current $I$ with open-neighbourhood extension, $\int_{t_{0}}^{t_{1}} ⟨ V, I ⟩ d t = \frac{1}{2} ⟨ I (t_{1}), L I (t_{1}) ⟩ - \frac{1}{2} ⟨ I (t_{0}), L I (t_{0}) ⟩$ with $V = L \dot{I}$ , and for a smooth compact conserved-profile realization the quadratic form equals the frozen magnetic field energy $\frac{1}{2 μ_{0}} \int ∣ B_{J_{I} (t)} ∣^{2}$ at each time. (Restricted inductor energy LI^2/2 and its identification with the frozen magnetic field energy).

[F3] For fixed compact smooth conserved profiles $j_{1}, \dots, j_{n}$ with linkage matrix $L = (L_{α β})$ one has $U (I) = \frac{1}{2} \int ⟨ J_{I}, A_{J_{I}} ⟩ = \frac{1}{2} \sum_{α, β} L_{α β} I_{α} I_{β} = \frac{1}{2 μ_{0}} \int ∣ B_{J_{I}} ∣^{2} \geq 0$ , and $U (I) = 0$ exactly when $J_{I} = \sum_{α} I_{α} j_{α} = 0$ pointwise; the matrix is positive definite exactly when the profiles are pointwise linearly independent. (Reciprocal linkage coefficients and magnetic energy of smooth compact conserved currents).

[F4] The compact smooth current class consists of the currents $J \in C_{c}^{\infty} (Ω; R^{3})$ with $div J = 0$ , extended by zero to $R^{3}$ . (The steady-current (magnetostatic) regime, the compact smooth current class and the declared ideal noncompact models).

[F5] The Euclidean inner product is $⟨ x, y ⟩ = \sum_{k} x_{k} y_{k}$ ; in particular for $I = (I_{1}, I_{2})$ and the block $L$ one has $⟨ I, L I ⟩ = L_{1} I_{1}^{2} + 2 M I_{1} I_{2} + L_{2} I_{2}^{2}$ . (The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ ).

[F6] Sums, scalar multiples and products of differentiable functions are differentiable, with the sum, scalar and product rules. (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$ ).

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

1.1F1F2F5F6algebra

Clause (a): by [F5], $\frac{1}{2} ⟨ I (t), L I (t) ⟩ = \frac{1}{2} L_{1} I_{1}^{2} + M I_{1} I_{2} + \frac{1}{2} L_{2} I_{2}^{2}$ , which is the displayed $W (t)$ . Differentiating termwise with the product and scalar rules of [F6] gives $\dot{W} = L_{1} I_{1} {\dot{I}}_{1} + M ({\dot{I}}_{1} I_{2} + I_{1} {\dot{I}}_{2}) + L_{2} I_{2} {\dot{I}}_{2} = (L_{1} {\dot{I}}_{1} + M {\dot{I}}_{2}) I_{1} + (M {\dot{I}}_{1} + L_{2} {\dot{I}}_{2}) I_{2} = V_{1} I_{1} + V_{2} I_{2}$ , since $[L \dot{I}]_{α} = V_{α}$ ; the sign reading of the mutual term is immediate from $W = \frac{1}{2} L_{1} I_{1}^{2} + \frac{1}{2} L_{2} I_{2}^{2} + M I_{1} I_{2}$ for $M > 0$ .

1.2A1F3F4algebracases

Clause (b): under the realization hypothesis, $W (t) = \frac{1}{2} \sum_{α, β} L_{α β} I_{α} (t) I_{β} (t) = U (I (t)) \geq 0$ at each $t$ by [F3], the block $L$ being by hypothesis the linkage matrix of the two profiles. Substituting $I = (\sqrt{L_{2}}, - \sqrt{L_{1}})$ gives $W = L_{1} L_{2} - M \sqrt{L_{1} L_{2}} \geq 0$ , that is $M \leq \sqrt{L_{1} L_{2}}$ ; substituting $I = (\sqrt{L_{2}}, + \sqrt{L_{1}})$ gives $W = L_{1} L_{2} + M \sqrt{L_{1} L_{2}} \geq 0$ , that is $M \geq - \sqrt{L_{1} L_{2}}$ ; together, $∣ M ∣ \leq \sqrt{L_{1} L_{2}}$ . If $M = s \sqrt{L_{1} L_{2}}$ and $I = (\sqrt{L_{2}}, - s \sqrt{L_{1}})$ , the same expansion gives $W = L_{1} L_{2} - s M \sqrt{L_{1} L_{2}} = L_{1} L_{2} - L_{1} L_{2} = 0$ , so by the vanishing clause of [F3] the associated current $J_{I}$ vanishes pointwise.

1.3F5F6algebra

Clause (c): with $N_{1} = \sqrt{L_{1} / Λ}$ and $N_{2} = \sqrt{L_{2} / Λ}$ one has $L_{1} = Λ N_{1}^{2}$ , $L_{2} = Λ N_{2}^{2}$ and $M = \sqrt{L_{1} L_{2}} = Λ N_{1} N_{2}$ because $N_{1} N_{2} = \sqrt{L_{1} L_{2}} / Λ$ . Hence, using $V_{α} = \sum_{β} L_{α β} {\dot{I}}_{β}$ , $V_{1} = L_{1} {\dot{I}}_{1} + M {\dot{I}}_{2} = Λ N_{1} (N_{1} {\dot{I}}_{1} + N_{2} {\dot{I}}_{2}) = N_{1} {\dot{Φ}}_{c}$ and $V_{2} = M {\dot{I}}_{1} + L_{2} {\dot{I}}_{2} = Λ N_{2} (N_{1} {\dot{I}}_{1} + N_{2} {\dot{I}}_{2}) = N_{2} {\dot{Φ}}_{c}$ with $Φ_{c} = Λ (N_{1} I_{1} + N_{2} I_{2})$ ; dividing by $N_{1}, N_{2} > 0$ gives the common ratio, and $e_{α} = - V_{α}$ reverses the common sign. For the energy, $W = \frac{1}{2} L_{1} I_{1}^{2} + M I_{1} I_{2} + \frac{1}{2} L_{2} I_{2}^{2} = \frac{1}{2} Λ (N_{1} I_{1} + N_{2} I_{2})^{2} = Φ_{c}^{2} / (2 Λ)$ by the displayed relations and the binomial expansion.

1.4F5F6algebracases

Clause (d), strict-linkage non-identity: suppose $∣ M ∣ < \sqrt{L_{1} L_{2}}$ and $V_{2} = k V_{1}$ held for all $C^{1}$ currents on $J$ ; then $\sum_{β} L_{2 β} {\dot{I}}_{β} = k \sum_{β} L_{1 β} {\dot{I}}_{β}$ for every such current. Fix any point $t_{0} \in J$ (any point when $J$ is a singleton) and, for each vector $a = (a_{1}, a_{2}) \in R^{2}$ , take the affine history $I (t) = c + (t - t_{0}) a$ (any fixed $c \in R^{2}$ ) on $J$ , which is the restriction of the affine map of $t$ on $R$ and hence carries the stated $C^{1}$ open-neighbourhood extension with $\dot{I} \equiv a$ ; substituting gives $(L_{21} - k L_{11}) a_{1} + (L_{22} - k L_{12}) a_{2} = 0$ for all $a$ , hence $L_{21} = k L_{11}$ and $L_{22} = k L_{12}$ , i.e. ${row}_{2} L = k {row}_{1} L$ . Then $L_{1} k = M$ and $L_{2} = k M = M^{2} / L_{1}$ , so $L_{1} L_{2} - M^{2} = 0$ , contradicting $L_{1} L_{2} - M^{2} > 0$ from $∣ M ∣ < \sqrt{L_{1} L_{2}}$ ; hence no such $k$ makes the ratio a universal identity. Accidental satisfaction occurs: any history with $\dot{I}$ in the kernel of the nonzero functional $a \mapsto (L_{21} - k L_{11}) a_{1} + (L_{22} - k L_{12}) a_{2}$ satisfies $V_{2} = k V_{1}$ at every time, that kernel containing the nonzero vector $(L_{22} - k L_{12}, - (L_{21} - k L_{11}))$ because the row difference is nonzero; in particular the constant currents give $V_{1} = V_{2} = 0$ . For the reversed winding with $M = s \sqrt{L_{1} L_{2}}$ , put $Φ_{c} = Λ (N_{1} I_{1} + s N_{2} I_{2})$ ; then $V_{1} = L_{1} {\dot{I}}_{1} + M {\dot{I}}_{2} = Λ N_{1} (N_{1} {\dot{I}}_{1} + s N_{2} {\dot{I}}_{2}) = N_{1} {\dot{Φ}}_{c}$ and $V_{2} = M {\dot{I}}_{1} + L_{2} {\dot{I}}_{2} = Λ s N_{2} (N_{1} {\dot{I}}_{1} + s N_{2} {\dot{I}}_{2}) = s N_{2} {\dot{Φ}}_{c}$ because $s^{2} = 1$ , so $V_{1} / N_{1} = V_{2} / (s N_{2}) = {\dot{Φ}}_{c}$ , and $W = \frac{1}{2} Λ (N_{1} I_{1} + s N_{2} I_{2})^{2} = Φ_{c}^{2} / (2 Λ)$ .

2.1A1F1F7step 1.1step 1.2step 1.3step 1.4∎

Steps 1.1-1.4 establish (a)-(d): steps 1.1-1.2 give (a) and the bound and null-direction clauses of (b), and steps 1.3-1.4 give the common-flux model (c) and the limitations (d). The computation is conditional on the adopted lumped model [F1], its units are [F7], and no leakage, loss, material or measurement claim is added; the terminal-voltage jets on a singleton interval are those of the specified extension. Countable Choice is used only through the realization clause (b), via [F3]; the algebraic clauses (a), (c) and (d) are choice-free.

Source notes

Fitzpatrick §7.4, printed pp. 222-225, computes the two-solenoid mutual inductance and records perfect linkage $M = \sqrt{L_{1} L_{2}}$ with the leakage warning; Griffiths §7.2.3, printed pp. 310-317, derives reciprocity and the Neumann formula; Tong §4.1.2, printed pp. 71-73, gives the single-coil energy and its field-energy representation; the mutual term here is obtained by local expansion of the linkage quadratic form. The example separates what is proved for the declared smooth compact profiles (the PSD bound and the null direction) from what is adopted as the common-flux ideal-transformer model, and it proves the failure of a universal voltage ratio under strict linkage by exhibiting the forced row proportionality and its contradiction; no physical transformer behaviour, loss mechanism or measurement is asserted.

Two-circuit mutual inductance, the perfect-linkage bound and ideal-transformer limitations

Example

Verification

Source notes

Depends on

Dependency tree · 2 levels

Sources