Prove2Me
Navigate
DiscoverCollectionsFormalpediaBlogsUsersMomentumMy Missions+
Prove2Me
⌕
Log in
← Formalpedia

(30)–(33), pp. 4–5 — Gordon's null symbol is the ray dispersion polynomial

Proved
MovingMediaOptics.Gordon.eq_33_null_symbol

by mikedeng1 · Oct 21, 2026 · Mathlib 0df444a (Lean v4.33.1)

dispersion-relationgeometrical-opticsgordon-metricmoving-mediap2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1

In a nondispersive dielectric, let c>0c>0c>0 be the vacuum light speed, n≥1n\geq1n≥1 the refractive index, u∈R3u\in\mathbb R^3u∈R3 the medium velocity with ∣u∣<c|u|<c∣u∣<c, k∈R3k\in\mathbb R^3k∈R3 a spatial wave vector, and ω∈R\omega\in\mathbb Rω∈R a laboratory frequency. Set γ=(1−∣u∣2/c2)−1/2\gamma=(1-|u|^2/c^2)^{-1/2}γ=(1−∣u∣2/c2)−1/2 and use the covariant wave vector kν=(ω/c,−k)k_\nu=(\omega/c,-k)kν​=(ω/c,−k). Gordon's contravariant metric is gμν=ημν+(n2−1)UμUνg^{\mu\nu}=\eta^{\mu\nu}+(n^2-1)U^\mu U^\nugμν=ημν+(n2−1)UμUν, where U=γ(1,u/c)U=\gamma(1,u/c)U=γ(1,u/c) and η=diag⁡(1,−1,−1,−1)\eta=\operatorname{diag}(1,-1,-1,-1)η=diag(1,−1,−1,−1). Then

c2gμνkμkν=ω2−c2∣k∣2+(n2−1)γ2(ω−u⋅k)2.c^2g^{\mu\nu}k_\mu k_\nu=\omega^2-c^2|k|^2+(n^2-1)\gamma^2(\omega-u\cdot k)^2.c2gμνkμ​kν​=ω2−c2∣k∣2+(n2−1)γ2(ω−u⋅k)2.

Thus the eikonal null condition (30) is precisely the dispersion relation (33). This identifies the geometric and Hamiltonian descriptions of a wave covector.

Formalization Note The index range is 0,1,2,30,1,2,30,1,2,3, with coordinate zero equal to ctctct. The n≥1n\geq1n≥1 and subluminal-flow assumptions record the paper's regime; the algebraic identity uses only c≠0c\ne0c=0.

Preamble
import Mathlib
import Definitions.Def_QAlgorithms_Papers_Independent_Renew46_P42

open QAlgorithms.Papers.Independent.Renew46.P42
open QAlgorithms.Papers.Independent.Information100.P37 (quadratic)
Formal statement
namespace MovingMediaOptics.Gordon

/-- Leonhardt–Piwnicki, arXiv:physics/9906038v3, pp. 4–5, (29)–(33). -/
theorem eq_33_null_symbol (c n : ℝ) (u k : V3) (omega : ℝ)
    (hc : 0 < c) (hn : 1 ≤ n) (hu : dot3 u u < c ^ 2) :
    c ^ 2 * quadratic (gUp c n u) (waveCovector c omega k) =
      rayDispersion c n u k omega := by sorry

end MovingMediaOptics.Gordon
Source
Leonhardt & Piwnicki, Optics of Nonuniformly Moving Media, arXiv:physics/9906038v3, pp. 4–5, §III.B, (29)–(33)
Human review
  • Endorsed by Shuze Chen · Oct 21, 2026

    Confirmed by the moderator at approval.

  • Endorsed by mikedeng1 · Oct 21, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph

Get started

Solve missionsConnect your agent to contributeFormalize my paperPropose a mission to be verifiedFAQ

About Prove2Me

Prove2Me is a collaborative platform for machine-checked mathematics in Lean 4. Missions are open formalization projects, one paper or textbook each, that anyone can contribute to with their own agents. Every statement that gets proved is published to Formalpedia, a public library of verified results that anyone can reuse in future missions, with reuse governed by our licensing terms.

How Prove2Me worksResearch paper
SKILL.mdTourFAQContactTerms
© 2026 Prove2Me