V-02 frame Maxwell objects

-- Generated by scripts/release05/gen_platform_tree.py (ATLAS-RELEASE-05) by skeleton subtraction from Atlas/EinsteinMaxwell/NP/NPMaxwell.lean
-- definition bundle: kept ExactVacuumAtlas.EinsteinMaxwell.NP.Fup, ExactVacuumAtlas.EinsteinMaxwell.NP.Hfr, ExactVacuumAtlas.EinsteinMaxwell.NP.Jfr
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_KNFrame
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_Kerr_InAtoms
import Definitions.Def_Atlas_Transport_Connection
import Definitions.Def_Atlas_Transport_MatrixCalc
/-!
# Atlas V-02 (D): Maxwell sources in a null frame, NP Maxwell equations, the Maxwell combination

General, **off shell** (no Maxwell or Einstein equation assumed; IV's residuals `J = maxwellDiv`, a vector, and
`H = faradayCyclic`, a 3-form, appear as source terms with their own transformation laws):

* `frame_dF`: `H(e_A,e_B,e_C) = Σ_cyc D_A F_{BC} − Σ_K (c^K_{AB} F_{KC} + c^K_{BC} F_{KA} + c^K_{CA} F_{KB})`
  (3-form: all three slots contracted with frame vectors; no metric, no Christoffel symbol);
* `frame_divF`: `θ^B(J) = Σ_P D_P F^{PB} + Σ_{P,K} Ω_K^K_P F^{PB} + Σ_{P,R} Ω_P^B_R F^{PR}` (vector: the frame
  component is taken with the dual coframe `θ^B`; `F^{PR}` = frame components raised with `η`);
* NP Maxwell equations with sources (`np_maxwell_1`, `np_maxwell_3`, and the primed `np_maxwell_4`,
  `np_maxwell_2`), e.g. `DΦ₁ − δ̄Φ₀ − (π − 2α)Φ₀ − 2ρΦ₁ + κΦ₂ = ½(H(l,m̄,m) − θ^n(J))`;
* **Maxwell combination** (`np_maxwell_combo_core`): for every `C^∞` `f`,
  `(δ + X)(D − 2ρ)f − (D + Y)(δ − 2τ)f = 2f [2Ψ₁ + Δκ − δ̄σ + (τ̄ + π + 3α − β̄)σ − (3γ + γ̄ + μ − μ̄)κ] + κΔf − σδ̄f`,
  `X = π̄ − β − ᾱ − 2τ`, `Y = ε̄ − ε − ρ̄ − 2ρ` — the Ricci-tensor terms cancel identically (no field equation).
  Applied to `f = Φ₁` together with `np_maxwell_1/3` it is the geometric source of III's `res1d`; the primed
  version (`np_maxwell_combo_core_neg`) is the source of `res1dN`.
-/

open scoped ContDiff Matrix
open Complex

namespace ExactVacuumAtlas.EinsteinMaxwell.NP

variable {g gi : Metric 4} {E Θ : Fin 4 → Fin 4 → Pt 4 → ℂ} {U : Set (Pt 4)}

/-! ### Frame-derivative calculus -/

section fdircalc

variable {n : ℕ} {E' : Fin n → Fin n → Pt n → ℂ} {V : Set (Pt n)} (hV : IsOpen V) {y : Pt n} (hy : y ∈ V)
include hV hy

end fdircalc

/-! ### The 3-form `H = dF` in the frame -/

/-- `H(e_A, e_B, e_C)` (all three slots with frame vectors). -/
noncomputable def Hfr (F : TwoForm 4) (E : Fin 4 → Fin 4 → Pt 4 → ℂ) (A B C : Fin 4) (x : Pt 4) : ℂ :=
  ∑ μ, ∑ ν, ∑ l, (faradayCyclic F μ ν l x : ℂ) * E A μ x * E B ν x * E C l x

/-! ### The vector `J = ∇·F` in the frame -/

/-- Frame components raised with `η`: `F^{PR} = Σ η^{PS} η^{RT} F_{ST}` (`η⁻¹ = η`). -/
noncomputable def Fup (F : TwoForm 4) (E : Fin 4 → Fin 4 → Pt 4 → ℂ) (P R : Fin 4) (x : Pt 4) : ℂ :=
  ∑ S, ∑ T, etaNull P S * etaNull R T * FfrF F E S T x

/-- Frame component of the vector `J^b = maxwellDiv g gi F b` along `e_B`, taken with the dual coframe. -/
noncomputable def Jfr (g gi : Metric 4) (F : TwoForm 4) (Θ : Fin 4 → Fin 4 → Pt 4 → ℂ) (B : Fin 4) (x : Pt 4) : ℂ :=
  ∑ b, Θ B b x * (maxwellDiv g gi F b x : ℂ)

/-! ### NP Maxwell equations with the `J`, `H` sources -/

section npmax

variable {F : TwoForm 4}

end npmax

/-! ### The Maxwell combination (geometric source of `res1d`) -/

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