V-01 single-mode notation

-- Generated by scripts/release05/gen_platform_tree.py (ATLAS-RELEASE-05) by skeleton subtraction from Atlas/EinsteinMaxwell/NP/ModeOperators.lean
-- definition bundle: kept ExactVacuumAtlas.EinsteinMaxwell.NP.modeField, ExactVacuumAtlas.EinsteinMaxwell.NP.phaseP, ExactVacuumAtlas.EinsteinMaxwell.NP.toRT
import Mathlib
import Definitions.Def_Atlas_Core_Basic
import Definitions.Def_Atlas_Core_Lift
import Definitions.Def_Atlas_EinsteinMaxwell_Basic
import Definitions.Def_Atlas_EinsteinMaxwell_Certificate
import Definitions.Def_Atlas_EinsteinMaxwell_KN_Defs
import Definitions.Def_Atlas_EinsteinMaxwell_KN_Domain
import Definitions.Def_Atlas_EinsteinMaxwell_NP_Basic
import Definitions.Def_Atlas_EinsteinMaxwell_NP_KNFaraday
import Definitions.Def_Atlas_EinsteinMaxwell_NP_KNFrame
import Definitions.Def_Atlas_Kerr_InAtoms
import Definitions.Def_Hintz2026_Core
import Definitions.Def_Hintz2026_Domain
import Definitions.Def_Hintz2026_System1
import Definitions.Def_Hintz2026_System4
/-! # Single-mode frame derivatives and III's `j = 0` operators (ATLAS-V-01)

For real `ω`, `m` (`om`, `mm`; III's local real mode parameters — no integrality of `m`, no complex frequency) and an
**arbitrary** function `u : ℝ² → ℂ` of `(r, θ)` (III's coordinates, index `0 = r`, `1 = θ`), the four-dimensional
mode field is `modeField om mm u (t,r,θ,φ) = P(t,φ) u(r,θ)` with `P = exp(−iωt + imφ)` (`phaseP`; the phase
convention of Hintz arXiv:2609.33661v1 and of III). Derivatives are the complex-valued **real** slice derivatives
`cpdC` (`Atlas.EinsteinMaxwell.NP.Basic`); the frame acts by `cdir` (complex-linear combination of real partials).

Bridge to III's existing two-dimensional derivative `Hintz2026.cpd` (not a copy): `cpdC_mode_r`, `cpdC_mode_th`
(`∂_r`, `∂_θ` of the mode field are `P` times III's `cpd 0`, `cpd 1` of `u` at `toRT x = (r, θ)`), together with
`∂_t ↦ −iω`, `∂_φ ↦ im`. With `K = −(r²+a²)ω + am`, `Q̂ = −aω sinθ + m/sinθ`:

    l(P u)  = P (∂_r u + iK/Δ u)                       = P · Dop    p 0 ω m u     (every x)
    n(P u)  = P (−Δ/(2Σ)) (∂_r u − iK/Δ u)             = P (−Δ/(2Σ)) · DopDag p 0 ω m u   (Δ ≠ 0)
    m(P u)  = P/(√2 q) (∂_θ u − Q̂ u)                    = P/(√2 ρ̄) · LopDag p 0 ω m u  (every x)
    m̄(P u)  = P/(√2 q̄) (∂_θ u + Q̂ u)                    = P/(√2 ρ̄*) · Lop  p 0 ω m u   (every x)

where `Dop`, `DopDag`, `Lop`, `LopDag` are III's original definitions (`Atlas/Perturbations/Hintz2026/System1Defs.lean`)
at `j = 0`, imported unchanged. The general-parameter forms `dir_*_mode` hold for every real `M a Q` (`a = 0`, `Q = 0`
allowed); III's `SubextremalKN p` enters only in the `*_eq_Dop…` bridges. The identities need no regularity of `u`
(both sides use the same `deriv` semantics); for `u` `C^∞` (order `∞`) on III's `U p`, the mode field is `C^∞` on
`domKN` and every `cpdC` is a genuine derivative (`hasDerivAt_modeField`). `P ≠ 0`, so each frame derivative vanishes iff
the corresponding III operator does (`dir_*_eq_zero_iff`; no division by `ω` or `m`, `ω = 0`, `m = 0` included).
Only `j = 0` is claimed: the `j`-dependent connection terms of III's system (1) are not derived here (V-02/V-03). -/

open Real
open scoped ComplexConjugate ContDiff
open ExactVacuumAtlas.EinsteinMaxwell.KN (Sig Del domReg domKN)

namespace ExactVacuumAtlas.EinsteinMaxwell.NP

attribute [-simp] Complex.ofReal_cos Complex.ofReal_sin

/-! ### Definitions -/

/-- `(r, θ)` of `x = (t, r, θ, φ)`, in III's coordinate order. -/
def toRT (x : Pt 4) : Fin 2 → ℝ := ![x 1, x 2]

/-- Mode phase `P(t, φ) = exp(−iωt + imφ)`. -/
noncomputable def phaseP (om mm : ℝ) (x : Pt 4) : ℂ :=
  Complex.exp (-(Complex.I * om * x 0) + Complex.I * mm * x 3)

/-- Single-mode field `P(t, φ) u(r, θ)`. -/
noncomputable def modeField (om mm : ℝ) (u : (Fin 2 → ℝ) → ℂ) (x : Pt 4) : ℂ :=
  phaseP om mm x * u (toRT x)

/-! ### Coordinate bookkeeping -/

section Coord
variable (om mm : ℝ) (x : Pt 4) (s : ℝ)

end Coord

/-! ### The four coordinate derivatives of a mode field (arbitrary `u`) -/

section Partials
variable (om mm : ℝ) (u : (Fin 2 → ℝ) → ℂ) (x : Pt 4)

end Partials

/-! ### The four frame directions on a mode field (every real `M a Q`) -/

section Directions
variable (M a Q om mm : ℝ) (u : (Fin 2 → ℝ) → ℂ) (x : Pt 4)

end Directions

/-! ### Identification with III's objects (`p : Hintz2026.SubextremalKN`) -/

section III
variable (p : Hintz2026.SubextremalKN)

end III

/-! ### The four directions are III's `j = 0` operators -/

section Bridge
variable (p : Hintz2026.SubextremalKN) (om mm : ℝ) (u : (Fin 2 → ℝ) → ℂ) (x : Pt 4)

/-! The mode factor and the frame prefactors never vanish on the exterior, so each frame derivative vanishes iff the
III operator does (`ω = 0`, `m = 0` included; nothing is divided by `ω` or `m`). -/

end Bridge

/-! ### Regularity: `C^∞` mode fields and genuine derivatives -/

section Smooth

variable (p : Hintz2026.SubextremalKN) (om mm : ℝ) {u : (Fin 2 → ℝ) → ℂ}

end Smooth

end ExactVacuumAtlas.EinsteinMaxwell.NP

• Endorsed by Shuze Chen · Oct 24, 2026

  Confirmed by the moderator at approval.

• Endorsed by He Wang · Oct 24, 2026

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