LemmaStatement: AI-adaptedProof: AI-adaptedPipeline-generatedprecheck passjudge 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.

The two-equation interface system at normal incidence

Statement

Let $ε_{j}, μ_{j} > 0$ be real for $j = 1, 2$ , put $Z_{j} : = \sqrt{μ_{j} / ε_{j}}$ for the nonnegative square root of Square roots exist: a unique $\sqrt{a} \geq 0$ with $(\sqrt{a})^{2} = a$ ; the positives are ${x^{2} : x \neq 0}$ , and let $E_{i}, E_{r}, E_{t} \in C$ with $E_{i} \neq 0$ satisfy the two linear equations

$E_{i} + E_{r} = E_{t}, \frac{E_{i} - E_{r}}{Z_{1}} = \frac{E_{t}}{Z_{2}} .$

Then

$\frac{E_{r}}{E_{i}} = \frac{Z_{2} - Z_{1}}{Z_{2} + Z_{1}}, \frac{E_{t}}{E_{i}} = \frac{2 Z_{2}}{Z_{1} + Z_{2}},$

and the real numbers $R : = ∣ E_{r} / E_{i} ∣^{2}$ and $T : = (Z_{1} / Z_{2}) ∣ E_{t} / E_{i} ∣^{2}$ satisfy

$R + T = 1.$

The two displayed equations are assumptions, not derived from any wave or field model; the ratio definitions of $R$ and $T$ are algebraic, and no electromagnetic validity is asserted. Oblique incidence, complex impedance and anisotropic media require further systems and branch conventions and are outside this statement.

Facts & Assumptions

Given: Real numbers $ε_{j}, μ_{j} > 0$ for $j = 1, 2$ , the square roots $Z_{j} = \sqrt{μ_{j} / ε_{j}}$ , and complex numbers $E_{i}, E_{r}, E_{t}$ with $E_{i} \neq 0$ satisfying $E_{i} + E_{r} = E_{t}$ and $(E_{i} - E_{r}) / Z_{1} = E_{t} / Z_{2}$ .

[L1]

Square roots and positivity: for real $x \geq 0$ there is a unique $s \geq 0$ with $s^{2} = x$ , written $\sqrt{x}$ , and $x > 0$ implies $\sqrt{x} > 0$ ; also $\sqrt{x^{2}} = x$ for $x \geq 0$ (Square roots exist: a unique $\sqrt{a} \geq 0$ with $(\sqrt{a})^{2} = a$ ; the positives are ${x^{2} : x \neq 0}$ ). Order and field arithmetic in $R$ are those of Complete ordered field (least-upper-bound property): sums and products of positive reals are positive, a positive real is nonzero, and $R \subseteq C$ under the embedding of The complex numbers as $R [x] / (x^{2} + 1)$ , with the real embedding and imaginary unit $i$ , on which the field operations of $C$ restrict to those of $R$ ( $C = R [x] / (x^{2} + 1)$ is a field, every element is uniquely $a + b i$ , and every nonzero element has inverse $(a - b i) / (a^{2} + b^{2})$ ).

[L2]

For a real $r$ , the coordinate definition $∣ r + 0 i ∣ = \sqrt{r^{2}}$ and [L1] give $∣ r ∣^{2} = r^{2}$ (Real and imaginary parts, complex conjugation, and modulus). This is the only modulus property needed below.

Proof

technique · direct; solve the two linear equations by substitution, then substitute the resulting ratios into the algebraic expressions defining $R$ and $T$

1.1givenL1algebra

Positivity and invertibility. Since $μ_{j} > 0$ and $ε_{j} > 0$ , the quotients $μ_{j} / ε_{j}$ are positive by [L1], so $Z_{j} = \sqrt{μ_{j} / ε_{j}} > 0$ for $j = 1, 2$ ; in particular $Z_{1}, Z_{2} \neq 0$ and $Z_{1} + Z_{2} > 0$ , so $Z_{1} + Z_{2}$ , $Z_{1} Z_{2}$ and $E_{i}$ are invertible complex numbers.

2.1step 1.1L1algebra

Solving the system. Substituting the first equation $E_{t} = E_{i} + E_{r}$ into the second gives $\frac{E_{i} - E_{r}}{Z_{1}} = \frac{E_{i} + E_{r}}{Z_{2}}$ ; multiplying by the nonzero number $Z_{1} Z_{2}$ and collecting terms yields $Z_{2} E_{i} - Z_{2} E_{r} = Z_{1} E_{i} + Z_{1} E_{r}$ , that is, $E_{r} (Z_{1} + Z_{2}) = E_{i} (Z_{2} - Z_{1})$ . Dividing by the nonzero numbers $E_{i}$ and $Z_{1} + Z_{2}$ gives $\frac{E_{r}}{E_{i}} = \frac{Z_{2} - Z_{1}}{Z_{1} + Z_{2}}$ , and then $\frac{E_{t}}{E_{i}} = 1 + \frac{E_{r}}{E_{i}} = \frac{Z_{1} + Z_{2} + Z_{2} - Z_{1}}{Z_{1} + Z_{2}} = \frac{2 Z_{2}}{Z_{1} + Z_{2}}$ by the field arithmetic of [L1]. Both ratios are real numbers, since all $Z_{j}$ are real.

3.1step 2.1L1L2algebra∎

The balance $R + T = 1$ . Because the ratios of step 2.1 are real, [L2] gives $∣ E_{r} / E_{i} ∣^{2} = (\frac{Z_{2} - Z_{1}}{Z_{1} + Z_{2}})^{2}$ and $∣ E_{t} / E_{i} ∣^{2} = (\frac{2 Z_{2}}{Z_{1} + Z_{2}})^{2}$ , so $R = \frac{(Z_{2} - Z_{1})^{2}}{(Z_{1} + Z_{2})^{2}}$ and $T = \frac{Z_{1}}{Z_{2}} \cdot \frac{4 Z_{2}^{2}}{(Z_{1} + Z_{2})^{2}} = \frac{4 Z_{1} Z_{2}}{(Z_{1} + Z_{2})^{2}}$ , and therefore $R + T = \frac{(Z_{2} - Z_{1})^{2} + 4 Z_{1} Z_{2}}{(Z_{1} + Z_{2})^{2}} = \frac{Z_{2}^{2} - 2 Z_{1} Z_{2} + Z_{1}^{2} + 4 Z_{1} Z_{2}}{(Z_{1} + Z_{2})^{2}} = \frac{(Z_{1} + Z_{2})^{2}}{(Z_{1} + Z_{2})^{2}} = 1$ by the expansion $(Z_{1} + Z_{2})^{2} = Z_{1}^{2} + 2 Z_{1} Z_{2} + Z_{2}^{2}$ and the invertibility of $Z_{1} + Z_{2}$ from step 1.1.

Remarks

In the period-averaged reading of the amplitudes as time-harmonic complex phasors, Period averages of products of real parts of complex exponentials with $a = d = A$ gives $\frac{1}{T_{0}} \int_{0}^{T_{0}} Re (A e^{- i ω t})^{2} d t = \frac{1}{2} ∣ A ∣^{2}$ for $ω > 0$ and $T_{0} = 2 π / ω$ , so $∣ E_{r} / E_{i} ∣^{2}$ is the ratio of the mean squares of the real reflected and incident fields and $T$ differs from the corresponding transmitted mean-square ratio by the real factor $Z_{1} / Z_{2}$ ; the identity $R + T = 1$ itself is the algebraic consequence proved above and does not rest on any field model.
Neither the system nor the conclusion involves $A C$ or any choice principle; it is finite algebra in $R$ and $C$ . The equations are satisfied by $E_{t} = E_{i}$ , $E_{r} = 0$ exactly when $Z_{1} = Z_{2}$ , in which case $R = 0$ , $T = 1$ .

Depends on

Dependency tree · 2 levels

Sources

R. Fitzpatrick, Electromagnetism lecture notes (UT Austin), Reflection at a dielectric boundary, Eqs. (1210)-(1232)