V-03 named Maxwell sources

Definition

Atlas_EinsteinMaxwell_NP_V03LinMx

by He Wang · Oct 23, 2026 · Mathlib 0df444a (Lean v4.33.1)

einstein-maxwellexact-spacetime-atlas-vexact-vacuum-atlasgeneral-relativitynewman-penrose

mxS1 … mxS4 (V-02 inline Maxwell sources) and their KN variations srcS1 … srcS4.

中文摘要 V-03 命名的 Maxwell 源项。

Registry: PHYSICS_BOUNDARY §M (V-03) M11.

Definition code

-- Generated by scripts/release05/gen_platform_tree.py (ATLAS-RELEASE-05) by skeleton subtraction from Atlas/EinsteinMaxwell/NP/V03LinMx.lean
-- definition bundle: kept ExactVacuumAtlas.EinsteinMaxwell.NP.mxS1, ExactVacuumAtlas.EinsteinMaxwell.NP.mxS2, ExactVacuumAtlas.EinsteinMaxwell.NP.mxS3, ExactVacuumAtlas.EinsteinMaxwell.NP.mxS4, ExactVacuumAtlas.EinsteinMaxwell.NP.srcS1, ExactVacuumAtlas.EinsteinMaxwell.NP.srcS2, ExactVacuumAtlas.EinsteinMaxwell.NP.srcS3, ExactVacuumAtlas.EinsteinMaxwell.NP.srcS4
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_Bianchi
import Definitions.Def_Atlas_EinsteinMaxwell_NP_CCalc
import Definitions.Def_Atlas_EinsteinMaxwell_NP_FrameConn
import Definitions.Def_Atlas_EinsteinMaxwell_NP_FrameNull
import Definitions.Def_Atlas_EinsteinMaxwell_NP_KNComm
import Definitions.Def_Atlas_EinsteinMaxwell_NP_KNFaraday
import Definitions.Def_Atlas_EinsteinMaxwell_NP_KNFrame
import Definitions.Def_Atlas_EinsteinMaxwell_NP_KNSpin
import Definitions.Def_Atlas_EinsteinMaxwell_NP_KNWeyl
import Definitions.Def_Atlas_EinsteinMaxwell_NP_ModeOperators
import Definitions.Def_Atlas_EinsteinMaxwell_NP_NPBianchi
import Definitions.Def_Atlas_EinsteinMaxwell_NP_NPMaxwell
import Definitions.Def_Atlas_EinsteinMaxwell_NP_NPRicci
import Definitions.Def_Atlas_EinsteinMaxwell_NP_NPScalars
import Definitions.Def_Atlas_EinsteinMaxwell_NP_Riemann
import Definitions.Def_Atlas_EinsteinMaxwell_NP_V03Family
import Definitions.Def_Atlas_EinsteinMaxwell_NP_V03LinKN
import Definitions.Def_Atlas_EinsteinMaxwell_NP_V03Realize
import Definitions.Def_Atlas_EinsteinMaxwell_NP_V03Var
import Definitions.Def_Atlas_EinsteinMaxwell_Variation_Defs
import Definitions.Def_Atlas_Kerr_InAtoms
import Definitions.Def_Atlas_Transport_Connection
import Definitions.Def_Atlas_Transport_MatrixCalc
import Definitions.Def_Hintz2026_Core
import Definitions.Def_Hintz2026_Domain
import Definitions.Def_Hintz2026_System1
import Definitions.Def_Hintz2026_System4
/-!
# Atlas V-03 (block C): linearised Maxwell combinations around Kerr–Newman (sources of `res1d`, `res1dN`)

V-02's `np_maxwell_combo` (`np_maxwell_combo_neg`) holds for every null frame and every antisymmetric `C^∞` field, with
the right-hand sides of the NP Maxwell equations (sources `J`, `H`, `Φ₀`, `Φ₂` kept) written as
`mxS1, mxS2` (`mxS4, mxS3` for the negative branch; class-B notation for V-02's inline expressions). At KN these
source combinations vanish on the open slice (`certReg`: `J = 0`, `dF = 0`; `Φ₀ = Φ₂ = κ = σ = λ = ν = 0`), so the
frame-variation terms of their frame derivatives vanish (proved), and their first variations are the explicit
`srcS1 … srcS4` (Maxwell residual variations `HfrVar`, `JfrVar` and the `Φ₀` / `Φ₂` variation `FfrFVar`, kept). -/

open Complex Filter Topology
open scoped ComplexConjugate Matrix ContDiff
open ExactVacuumAtlas.EinsteinMaxwell ExactVacuumAtlas.Variation
open ExactVacuumAtlas.EinsteinMaxwell.KN (Sig Del gKN giKN domReg domKN faradayKN)

namespace ExactVacuumAtlas.EinsteinMaxwell.NP

attribute [-simp] Complex.ofReal_cos Complex.ofReal_sin

/-! ### The four Maxwell source combinations (V-02's inline expressions, named) -/

section src
variable (g gi : Metric 4) (F : TwoForm 4) (E Θ : Fin 4 → Fin 4 → Pt 4 → ℂ) (z : Pt 4)

/-- `(H(l,m̄,m) − θ^n(J))/2 + δ̄Φ₀ + (π − 2α)Φ₀ − κΦ₂` (NP Maxwell equation 1 for `(D − 2ρ)Φ₁`). -/
noncomputable def mxS1 : ℂ :=
  (Hfr F E 0 3 2 z - Jfr g gi F Θ 1 z) / 2 + fdir E 3 (FfrF F E 0 2) z
    + (npPi g gi E Θ z - 2 * npAlpha g gi E Θ z) * phi0 E z F - npKappa g gi E Θ z * phi2 E z F
/-- `(θ^{m̄}(J) + H(n,m,l))/2 + ΔΦ₀ + (μ − 2γ)Φ₀ − σΦ₂` (NP Maxwell equation 3 for `(δ − 2τ)Φ₁`). -/
noncomputable def mxS2 : ℂ :=
  (Jfr g gi F Θ 3 z + Hfr F E 1 2 0 z) / 2 + fdir E 1 (FfrF F E 0 2) z
    + (npMu g gi E Θ z - 2 * npGamma g gi E Θ z) * phi0 E z F - npSigma g gi E Θ z * phi2 E z F
/-- `δΦ₂ + νΦ₀ − (τ − 2β)Φ₂ − (H(n,m,m̄) − θ^l(J))/2` (NP Maxwell equation 4, negative branch). -/
noncomputable def mxS4 : ℂ :=
  fdir E 2 (FfrF F E 3 1) z + npNu g gi E Θ z * phi0 E z F
    - (npTau g gi E Θ z - 2 * npBeta g gi E Θ z) * phi2 E z F - (Hfr F E 1 2 3 z - Jfr g gi F Θ 0 z) / 2
/-- `DΦ₂ + λΦ₀ − (ρ − 2ε)Φ₂ − (θ^m(J) − H(l,n,m̄))/2` (NP Maxwell equation 2, negative branch). -/
noncomputable def mxS3 : ℂ :=
  fdir E 0 (FfrF F E 3 1) z + npLambda g gi E Θ z * phi0 E z F
    - (npRho g gi E Θ z - 2 * npEps g gi E Θ z) * phi2 E z F - (Jfr g gi F Θ 2 z - Hfr F E 0 1 3 z) / 2

end src

section srclin
variable (F f : TwoForm 4) (g gi h : Metric 4) (E Θ B : Fin 4 → Fin 4 → Pt 4 → ℂ) (z : Pt 4)

/-- First variation of `mxS1` at a background with `Φ₀ = Φ₂ = κ = 0` near `z` (explicit). -/
noncomputable def srcS1 : ℂ :=
  (HfrVar F f E B 0 3 2 z - JfrVar g gi F h f Θ B 1 z) / 2 + fdir E 3 (FfrFVar F f E B 0 2) z
    + (npPi g gi E Θ z - 2 * npAlpha g gi E Θ z) * FfrFVar F f E B 0 2 z
/-- First variation of `mxS2` at a background with `Φ₀ = Φ₂ = σ = 0` near `z` (explicit). -/
noncomputable def srcS2 : ℂ :=
  (JfrVar g gi F h f Θ B 3 z + HfrVar F f E B 1 2 0 z) / 2 + fdir E 1 (FfrFVar F f E B 0 2) z
    + (npMu g gi E Θ z - 2 * npGamma g gi E Θ z) * FfrFVar F f E B 0 2 z
/-- First variation of `mxS4` at a background with `Φ₀ = Φ₂ = ν = 0` near `z` (explicit). -/
noncomputable def srcS4 : ℂ :=
  fdir E 2 (FfrFVar F f E B 3 1) z - (npTau g gi E Θ z - 2 * npBeta g gi E Θ z) * FfrFVar F f E B 3 1 z
    - (HfrVar F f E B 1 2 3 z - JfrVar g gi F h f Θ B 0 z) / 2
/-- First variation of `mxS3` at a background with `Φ₀ = Φ₂ = λ = 0` near `z` (explicit). -/
noncomputable def srcS3 : ℂ :=
  fdir E 0 (FfrFVar F f E B 3 1) z - (npRho g gi E Θ z - 2 * npEps g gi E Θ z) * FfrFVar F f E B 3 1 z
    - (JfrVar g gi F h f Θ B 2 z - HfrVar F f E B 0 1 3 z) / 2

end srclin

section kn
variable {M a Q : ℝ}

local notation "gK" => gKN M a Q
local notation "giK" => giKN M a Q
local notation "EK" => knE M a Q
local notation "ΘK" => knTh M a Q
local notation "FK" => faradayKN a Q

end kn

namespace NPFamily

variable {g gi : ℝ → Metric 4} {F : ℝ → TwoForm 4} {E Θ : ℝ → Fin 4 → Fin 4 → Pt 4 → ℂ} {W : Set (ℝ × Pt 4)}

end NPFamily

section lin

variable {M a Q : ℝ} {g gi : ℝ → Metric 4} {F : ℝ → TwoForm 4} {E Θ : ℝ → Fin 4 → Fin 4 → Pt 4 → ℂ}
  {W : Set (ℝ × Pt 4)} {h : Metric 4} {f : TwoForm 4} {B : Fin 4 → Fin 4 → Pt 4 → ℂ}

local notation "gK" => gKN M a Q
local notation "giK" => giKN M a Q
local notation "EK" => knE M a Q
local notation "ΘK" => knTh M a Q
local notation "FK" => faradayKN a Q

end lin

end ExactVacuumAtlas.EinsteinMaxwell.NP

Source

He Wang, Exact Spacetime Atlas V: From Linearized Einstein–Maxwell Equations to Kerr–Newman Radiation Systems. Local source, no public repository; commit b8cd107a558e153ed41fb4972ac5315499d14778; Atlas/EinsteinMaxwell/NP/V03LinMx.lean; SHA-256 70faf22e9e83692c79cdd87754cd04e53ebf59f983c055f9a9013fa7752bb600. Registered definitions: mission/PHYSICS_BOUNDARY.md (§K–§M); literature: P. Hintz, arXiv:2609.33661 (v1); Mark–Yang–Zimmerman–Chen, arXiv:1409.5800 (v1).

Human review

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).

View graph