(30)–(33), pp. 4–5 — Gordon's null symbol is the ray dispersion polynomial
ProvedMovingMediaOptics.Gordon.eq_33_null_symboldispersion-relationgeometrical-opticsgordon-metricmoving-mediap2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1
In a nondispersive dielectric, let be the vacuum light speed, the refractive index, the medium velocity with , a spatial wave vector, and a laboratory frequency. Set and use the covariant wave vector . Gordon's contravariant metric is , where and . Then
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 , with coordinate zero equal to . The and subluminal-flow assumptions record the paper's regime; the algebraic identity uses only .
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
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.