V-03 complexification

-- Generated by scripts/release05/gen_platform_tree.py (ATLAS-RELEASE-05) by skeleton subtraction from Atlas/EinsteinMaxwell/NP/V03Cplx.lean
-- definition bundle: kept ExactVacuumAtlas.EinsteinMaxwell.NP.CTan, ExactVacuumAtlas.EinsteinMaxwell.NP.cplx, ExactVacuumAtlas.EinsteinMaxwell.NP.cplxR, ExactVacuumAtlas.EinsteinMaxwell.NP.lcombC
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_V03LinMx
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_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 B): real linearity of the NP variations and their proved complex-linear extension

* Real linearity (`*_lcomb`): on the admissible `C^∞` class, `weylVar`, `weylFVar`, `brkVar`, `cLVar`, `omLVar`,
  `FfrFVar` (hence `psi*Var`, `kappaVar`, `sigmaVar`, `nuVar`, `lambdaVar`, `phi0Var`, `phi2Var`) are real-linear in the
  tangent `(h, f, B)` (IV's `lcomb` for `h`, `f`; `lcombC` for `B`). IV's `chrVar_lcomb`, `pd_chrVar_lcomb`,
  `ricciVar_lcomb`, `scalarVar_lcomb` are reused.
* Complexification (`CTan`, `cplx`): a complex tangent is a pair of real tangents `τ_R + i τ_I`; a real-linear
  variation `V` extends by `V_ℂ(τ) = V(τ_R) + i V(τ_I)`, which is proved additive and **complex**-homogeneous
  (`cplx_smul`) from real linearity. IV's real operators are complexified the same way (`LE_ℂ = LE(τ_R) + i LE(τ_I)`),
  and `LE_ℂ = 0 ↔ LE(τ_R) = 0 ∧ LE(τ_I) = 0` (`cplx_eq_zero_iff`). No complex number is ever placed in IV's real
  metric type. The `B`-suffixed spin coefficients of V-02 are never replaced by complex conjugates of the
  complexified variations. -/

open Complex Filter Topology
open scoped ComplexConjugate Matrix ContDiff
open ExactVacuumAtlas.EinsteinMaxwell ExactVacuumAtlas.Variation

namespace ExactVacuumAtlas.EinsteinMaxwell.NP

/-- Real linear combination of two complex frame tangents (class B notation). -/
def lcombC (c₁ : ℝ) (B₁ : Fin 4 → Fin 4 → Pt 4 → ℂ) (c₂ : ℝ) (B₂ : Fin 4 → Fin 4 → Pt 4 → ℂ) :
    Fin 4 → Fin 4 → Pt 4 → ℂ :=
  fun A μ y => (c₁ : ℂ) * B₁ A μ y + (c₂ : ℂ) * B₂ A μ y

section lin

variable {U : Set (Pt 4)} {g gi h₁ h₂ : Metric 4} {F f₁ f₂ : TwoForm 4} {E B₁ B₂ : Fin 4 → Fin 4 → Pt 4 → ℂ}
  {c₁ c₂ : ℝ}

variable (hU : IsOpen U) (hg : ∀ i j, ContDiffOn ℝ ∞ (g i j) U) (hgi : ∀ i j, ContDiffOn ℝ ∞ (gi i j) U)
  (hh₁ : ∀ i j, ContDiffOn ℝ ∞ (h₁ i j) U) (hh₂ : ∀ i j, ContDiffOn ℝ ∞ (h₂ i j) U)
include hU hg hgi hh₁ hh₂

end lin

section lin2

variable {U : Set (Pt 4)} {g h₁ h₂ : Metric 4} {F f₁ f₂ : TwoForm 4} {E B₁ B₂ : Fin 4 → Fin 4 → Pt 4 → ℂ}
  {c₁ c₂ : ℝ}

variable (hU : IsOpen U) (hB₁ : ∀ A μ, ContDiffOn ℝ ∞ (B₁ A μ) U) (hB₂ : ∀ A μ, ContDiffOn ℝ ∞ (B₂ A μ) U)
include hU hB₁ hB₂

end lin2

/-! ### Complexification -/

/-- A complex first-order tangent `τ_R + i τ_I` given by two real tangents (class B). -/
structure CTan where
  hR : Metric 4
  hI : Metric 4
  fR : TwoForm 4
  fI : TwoForm 4
  BR : Fin 4 → Fin 4 → Pt 4 → ℂ
  BI : Fin 4 → Fin 4 → Pt 4 → ℂ

/-- Complex extension of a variation `V(h, f, B)`: `V_ℂ(τ) = V(τ_R) + i V(τ_I)`. -/
def cplx (V : Metric 4 → TwoForm 4 → (Fin 4 → Fin 4 → Pt 4 → ℂ) → Pt 4 → ℂ) (τ : CTan) (y : Pt 4) : ℂ :=
  V τ.hR τ.fR τ.BR y + I * V τ.hI τ.fI τ.BI y

/-- Complexification of a real-valued (IV) operator: `L_ℂ(τ) = L(τ_R) + i L(τ_I)`. -/
def cplxR (L : Metric 4 → TwoForm 4 → Pt 4 → ℝ) (τ : CTan) (y : Pt 4) : ℂ :=
  (L τ.hR τ.fR y : ℂ) + I * (L τ.hI τ.fI y : ℂ)

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