Prove2Me

V-03 complexified NP variations, sources, CLinEM

Definition
Atlas_EinsteinMaxwell_NP_V03C3

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

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

V-03 complexified NP variations, sources, CLinEM

cPsi0 … cPhi2 (complexified named variations), cRicF, cSrc1 … cSrc4, CLinEM (IV's L_E = L_J = L_H = 0, complexified, on U).

中文摘要 V-03 复化 NP 变分、源项与 CLinEM。

Registry: PHYSICS_BOUNDARY §M (V-03) M5, M6, M14.

Definition code
-- Generated by scripts/release05/gen_platform_tree.py (ATLAS-RELEASE-05) by skeleton subtraction from Atlas/EinsteinMaxwell/NP/V03C3.lean
-- definition bundle: kept ExactVacuumAtlas.EinsteinMaxwell.NP.CLinEM, ExactVacuumAtlas.EinsteinMaxwell.NP.cKappa, ExactVacuumAtlas.EinsteinMaxwell.NP.cLambda, ExactVacuumAtlas.EinsteinMaxwell.NP.cNu, ExactVacuumAtlas.EinsteinMaxwell.NP.cPhi0, ExactVacuumAtlas.EinsteinMaxwell.NP.cPhi2, ExactVacuumAtlas.EinsteinMaxwell.NP.cPsi0, ExactVacuumAtlas.EinsteinMaxwell.NP.cPsi1, ExactVacuumAtlas.EinsteinMaxwell.NP.cPsi3, ExactVacuumAtlas.EinsteinMaxwell.NP.cPsi4, ExactVacuumAtlas.EinsteinMaxwell.NP.cRicF, ExactVacuumAtlas.EinsteinMaxwell.NP.cSigma, ExactVacuumAtlas.EinsteinMaxwell.NP.cSrc1, ExactVacuumAtlas.EinsteinMaxwell.NP.cSrc2, ExactVacuumAtlas.EinsteinMaxwell.NP.cSrc3, ExactVacuumAtlas.EinsteinMaxwell.NP.cSrc4
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_V03Cplx
import Definitions.Def_Atlas_EinsteinMaxwell_NP_V03Family
import Definitions.Def_Atlas_EinsteinMaxwell_NP_V03LinKN
import Definitions.Def_Atlas_EinsteinMaxwell_NP_V03LinMx
import Definitions.Def_Atlas_EinsteinMaxwell_NP_V03Realize
import Definitions.Def_Atlas_EinsteinMaxwell_NP_V03Src
import Definitions.Def_Atlas_EinsteinMaxwell_NP_V03Tan
import Definitions.Def_Atlas_EinsteinMaxwell_NP_V03Var
import Definitions.Def_Atlas_EinsteinMaxwell_Variation_Defs
import Definitions.Def_Atlas_EinsteinMaxwell_Variation_Local
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 C3): complexified identities; the sources vanish under IV's `L = 0` and the phantom gauge

Order of the argument (no step is skipped):
1. each real part `τ_R`, `τ_I` of a complex KN tangent (`KNCTan`) is realised by a `KNFam` (`knRealize`), so V-03's
   eight linearised identities hold for it **with their sources kept** (`lin_*`);
2. they are combined into complex identities (`c_*_src`) by `V_ℂ = V(τ_R) + i V(τ_I)`; frame derivatives commute with
   the combination because every variation function is `C^∞` on `U` (proved, `RealFrameTangent.kn_*`, `fdir_cplx`);
3. the Ricci and Maxwell sources are written through IV's real residuals (`V03Src`); the hypothesis `CLinEM` is the
   **complexified** IV system `L_E^ℂ = L_J^ℂ = L_H^ℂ = 0` on `U`, which for the real operators is equivalent to both
   real parts vanishing (`cplx_eq_zero_iff`);
4. the remaining `δΦ₀` (positive branch) / `δΦ₂` (negative branch) terms are removed by the **complex** phantom gauge
   `δΦ₀^ℂ = 0` resp. `δΦ₂^ℂ = 0` on the open set `U`. This gauge is a condition on the complex combination only: it is
   **not** split into conditions on the two real tangents (`δΦ₀` is complex-valued), and it is not `δF = 0`,
   not `δΦ₁ = 0`, and contains no target equation.

All zero statements used under a frame derivative hold on the open set `U`. The `B`-suffixed background coefficients
stay the index-swapped components of V-02; no conjugation of the complexified variations is used. -/

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

/-! ### Regularity of the variation functions of a compatible real tangent at KN -/

section rft

variable {M a Q : ℝ} {U : 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

variable (hU : IsOpen U) (hUD : U ⊆ domReg M a Q) (ht : RealFrameTangent (gKN M a Q) (knE M a Q) U h f B)
include hU hUD ht

end rft

/-! ### Complexified NP variations at KN (class B notation) -/

section cdefs

variable (M a Q : ℝ) (τ : CTan)

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

/-- `δΨ₀^ℂ`. -/ noncomputable def cPsi0 : Pt 4 → ℂ := cplx (fun h _ B => psi0Var gK giK h EK B) τ
/-- `δΨ₁^ℂ`. -/ noncomputable def cPsi1 : Pt 4 → ℂ := cplx (fun h _ B => psi1Var gK giK h EK B) τ
/-- `δΨ₃^ℂ`. -/ noncomputable def cPsi3 : Pt 4 → ℂ := cplx (fun h _ B => psi3Var gK giK h EK B) τ
/-- `δΨ₄^ℂ`. -/ noncomputable def cPsi4 : Pt 4 → ℂ := cplx (fun h _ B => psi4Var gK giK h EK B) τ
/-- `δκ^ℂ`. -/ noncomputable def cKappa : Pt 4 → ℂ := cplx (fun h _ B => kappaVar gK h EK B) τ
/-- `δσ^ℂ`. -/ noncomputable def cSigma : Pt 4 → ℂ := cplx (fun h _ B => sigmaVar gK h EK B) τ
/-- `δν^ℂ`. -/ noncomputable def cNu : Pt 4 → ℂ := cplx (fun h _ B => nuVar gK h EK B) τ
/-- `δλ^ℂ`. -/ noncomputable def cLambda : Pt 4 → ℂ := cplx (fun h _ B => lambdaVar gK h EK B) τ
/-- `δΦ₀^ℂ`. -/ noncomputable def cPhi0 : Pt 4 → ℂ := cplx (fun _ f B => phi0Var FK f EK B) τ
/-- `δΦ₂^ℂ`. -/ noncomputable def cPhi2 : Pt 4 → ℂ := cplx (fun _ f B => phi2Var FK f EK B) τ
/-- `δRic(e_A,e_K)^ℂ` (source terms). -/
noncomputable def cRicF (A K : Fin 4) : Pt 4 → ℂ := cplx (fun h _ B => ricFVar gK giK h EK B A K) τ
/-- Complexified Maxwell source combinations `srcS1 … srcS4`. -/
noncomputable def cSrc1 : Pt 4 → ℂ := cplx (fun h f B => srcS1 FK f gK giK h EK ΘK B) τ
noncomputable def cSrc2 : Pt 4 → ℂ := cplx (fun h f B => srcS2 FK f gK giK h EK ΘK B) τ
noncomputable def cSrc3 : Pt 4 → ℂ := cplx (fun h f B => srcS3 FK f gK giK h EK ΘK B) τ
noncomputable def cSrc4 : Pt 4 → ℂ := cplx (fun h f B => srcS4 FK f gK giK h EK ΘK B) τ

end cdefs

/-- **IV's linearised Einstein–Maxwell system, complexified**, on `U`: `L_E^ℂ = L_J^ℂ = L_H^ℂ = 0` (class B; the
real residuals `linEinstein`, `linMaxwell`, `linFaraday` of IV, extended by `cplxR`). -/
structure CLinEM (M a Q : ℝ) (U : Set (Pt 4)) (τ : CTan) : Prop where
  einstein : ∀ y ∈ U, ∀ i j, cplxR (fun h f => linEinstein (gKN M a Q) (giKN M a Q) (faradayKN a Q) h f i j) τ y = 0
  maxwell : ∀ y ∈ U, ∀ j, cplxR (fun h f => linMaxwell (gKN M a Q) (giKN M a Q) (faradayKN a Q) h f j) τ y = 0
  faraday : ∀ y ∈ U, ∀ i j k, cplxR (fun _ f => linFaraday f i j k) τ y = 0

section main

variable {M a Q : ℝ} {U : Set (Pt 4)} {τ : CTan} {x : 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

variable (hτ : KNCTan M a Q U τ)
include hτ

/-! #### Frame derivatives commute with the complex combination -/

/-! #### Step 2: complexified identities with the sources kept -/

/-! #### Step 3–4: the sources vanish on `U` -/

variable (hL : CLinEM M a Q U τ)
include hL

/-! #### The eight source-free complex identities -/

end main

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/V03C3.lean; SHA-256 1dcdc9f162705ee0e0c400be0d5f68321e834819244eb6f5b14fb12b2d5c0da3. 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