ExampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6-luna)

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.

Normal-incidence reflection at a planar dielectric interface

Example

Let the planar interface be $x = 0$ , with constant lossless isotropic media with $ϵ_{i} > 0$ and $μ_{i} > 0$ on $x < 0$ ( $i = 1$ ) and $x > 0$ ( $i = 2$ ). For a nonzero incident amplitude $E_{0} \in C ∖ {0}$ and angular frequency $ω > 0$ , define impedances $η_{i} = \sqrt{μ_{i} / ϵ_{i}}$ and wave numbers $k_{i} = ω \sqrt{ϵ_{i} μ_{i}}$ . Take the real parts of the phasors $E_{z}^{-} = E_{0} (e^{i (k_{1} x - ω t)} + R e^{i (- k_{1} x - ω t)}), H_{y}^{-} = - \frac{E_{0}}{η_{1}} e^{i (k_{1} x - ω t)} + \frac{R E_{0}}{η_{1}} e^{i (- k_{1} x - ω t)},$ $E_{z}^{+} = T E_{0} e^{i (k_{2} x - ω t)}, H_{y}^{+} = - \frac{T E_{0}}{η_{2}} e^{i (k_{2} x - ω t)} .$ The electric field is directed along $z$ , and the magnetic intensity is along $y$ .

Facts & Assumptions

Given: Source-free, conductivity-free Maxwell fields in each constant medium and the interface convention with no singular surface charge or current.

[F1]

The tangential traces of $E$ and $H = μ^{- 1} B$ are continuous across a material interface with no singular surface current; the normal traces of $ϵ E$ and $B$ are continuous when there is no surface charge. (Transient Maxwell system with piecewise materials and boundary conditions)

Verification

1.1F1givenalgebra

For a wave with sign $s = + 1$ (right-going) or $s = - 1$ (left-going), write its phasor as $E_{z} = A e^{i (s k_{i} x - ω t)}$ and $H_{y} = - s A e^{i (s k_{i} x - ω t)} / η_{i}$ . Then $(curl E)_{y} = - i s k_{i} E_{z}$ and $(curl H)_{z} = i s k_{i} H_{y} = - i k_{i} A e^{i (s k_{i} x - ω t)} / η_{i}$ . Faraday's equation holds because $B_{y} = μ_{i} H_{y} = - s (k_{i} / ω) E_{z}$ , and Ampere's equation holds because $k_{i} / η_{i} = ω ϵ_{i}$ . Also $div (ϵ_{i} E) = 0$ since $E_{z}$ is independent of $z$ , and $div B = 0$ since $B_{y}$ is independent of $y$ . Real parts also solve these real linear equations. Since $E_{0} \neq 0$ , at $x = 0$ continuity of tangential $E_{z}$ and $H_{y}$ is exactly $1 + R = T, \frac{1 - R}{η_{1}} = \frac{T}{η_{2}} .$

2.1F1step 1.1algebra∎

Solving the first equation for $T$ and substituting into the second gives $η_{2} (1 - R) = η_{1} (1 + R)$ , hence $R = \frac{η_{2} - η_{1}}{η_{1} + η_{2}}, T = \frac{2 η_{2}}{η_{1} + η_{2}} .$ Because both fields have only tangential components, their normal traces vanish on both sides, so the normal interface conditions in [F1] also hold.

Depends on

Transient Maxwell system with piecewise materials and boundary conditions

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

2 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

John B. Schneider, Understanding the Finite-Difference Time-Domain Method (standard reference, not scraped)