V-03 complex KN tangent

-- Generated by scripts/release05/gen_platform_tree.py (ATLAS-RELEASE-05) by skeleton subtraction from Atlas/EinsteinMaxwell/NP/V03Tan.lean
-- definition bundle: kept ExactVacuumAtlas.EinsteinMaxwell.NP.KNCTan
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_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 C2'): regularity of the tangent and of its NP variations; KN realisation; complex tangents

* `contDiffOn_var_of`: a function that is, at every point of the open slice `ε = 0`, the genuine `ε`-derivative of a
  jointly `C^∞` family is `C^∞` on the slice (`contDiffOn_deriv_slice` + uniqueness of derivatives).
* Hence, for every `NPFamily`/`NPTangent`: `h` and all NP variation functions (`weylFVar`, `omLVar`, `ricFVar`,
  `FfrFVar`, `HfrVar`, `JfrVar`; at KN also `srcS1 … srcS4`) are `C^∞` on the slice. These are theorems, not
  hypotheses.
* `NullFrameData.restrict`, `knRealize`: every compatible real tangent `(h, f, B)` on an open `U ⊆ domReg` (KN
  background, `RealFrameTangent`) is the genuine tangent of a `KNFam` whose slice is exactly `U` (via `realize`;
  kinematic only: the family is **not** required to solve the field equations).
* `RealFrameTangent.lcomb`: compatible real tangents form a real vector space.
* `KNCTan`: a complex tangent `τ = τ_R + i τ_I` whose two real parts are compatible real tangents on `U`; closed
  under complex scalar multiplication and addition (`KNCTan.smul`, `KNCTan.add`). -/

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

namespace NPFamily

variable {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 → ℂ}

variable (hF : NPFamily g gi F E Θ W) (ht : NPTangent g F E W h f B)
include hF ht

end NPFamily

section knsmooth

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

variable (hK : KNFam M a Q g gi F E Θ W) (ht : NPTangent g F E W h f B)
include hK ht

end knsmooth

/-! ### Kerr–Newman realisation of compatible real tangents -/

section knreal

variable {M a Q : ℝ}

end knreal

/-! ### Linear structure of compatible real tangents; complex tangents at KN -/

section lin

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

end lin

/-- **A complex first-order tangent at Kerr–Newman** on an open `U ⊆ domReg`: both real parts are compatible real
tangents (`C^∞` `f`, `B`, antisymmetric `f`, real pattern of `B`, first-order Gram relation; class B). -/
structure KNCTan (M a Q : ℝ) (U : Set (Pt 4)) (τ : CTan) : Prop where
  isOpen : IsOpen U
  sub : U ⊆ domReg M a Q
  re : RealFrameTangent (gKN M a Q) (knE M a Q) U τ.hR τ.fR τ.BR
  im : RealFrameTangent (gKN M a Q) (knE M a Q) U τ.hI τ.fI τ.BI

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