V-03 reality pattern and realisation family

-- Generated by scripts/release05/gen_platform_tree.py (ATLAS-RELEASE-05) by skeleton subtraction from Atlas/EinsteinMaxwell/NP/V03Realize.lean
-- definition bundle: kept ExactVacuumAtlas.EinsteinMaxwell.NP.RealFrameTangent, ExactVacuumAtlas.EinsteinMaxwell.NP.RealPattern, ExactVacuumAtlas.EinsteinMaxwell.NP.rzE, ExactVacuumAtlas.EinsteinMaxwell.NP.rzF, ExactVacuumAtlas.EinsteinMaxwell.NP.rzG, ExactVacuumAtlas.EinsteinMaxwell.NP.rzGI, ExactVacuumAtlas.EinsteinMaxwell.NP.rzGIc, ExactVacuumAtlas.EinsteinMaxwell.NP.rzGc, ExactVacuumAtlas.EinsteinMaxwell.NP.rzTh, ExactVacuumAtlas.EinsteinMaxwell.NP.rzW, ExactVacuumAtlas.EinsteinMaxwell.NP.swap23Perm
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_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 A): every compatible real frame tangent is the tangent of a real normalised family

Given a background null frame `(g₀, gi₀, E₀, Θ₀)` on an open `U` whose frame has the real pattern
`e_{swap23 A} = conj e_A` (`l`, `n` real, `m̄ = conj m`), a field `F₀`, and a real tangent `(h, f, B)` with
`B` of the same pattern and the first-order normalisation `FrameCompat g₀ h E₀ B U`, the **realisation family**

* `T_ε = E₀ + ε B` (`rzE`), `Θ_ε = T_ε⁻¹` (`rzTh`), on `W = {(ε, y) | y ∈ U, det T_ε(y) ≠ 0}` (`rzW`),
* `G_ε = Θ_εᵀ η Θ_ε` (`rzGc`), `GI_ε = T_ε η T_εᵀ` (`rzGIc`) — proved **real** (`im = 0`) from the pattern, and the
  real metric / inverse are their real parts (`rzG`, `rzGI`),
* `F_ε = F₀ + ε f` (`rzF`)

is an `NPFamily` (true inverse, exact null Gram matrix on every slice, joint `C^∞`) whose tangent at `ε = 0` is exactly
`(h, f, B)` (`realize`). It is a kinematic realisation only: no `ε ≠ 0` member is claimed to solve any field equation.
Outside `U` the definitions fall back to the background (so that `ε = 0` gives the background as functions); only
points of `W` (where `y ∈ U`) are ever used. -/

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

namespace ExactVacuumAtlas.EinsteinMaxwell.NP

/-- Real pattern of a complex frame (or frame tangent): `l`, `n` real and `m̄ = conj m` on `U` (class B). -/
def RealPattern (E : Fin 4 → Fin 4 → Pt 4 → ℂ) (U : Set (Pt 4)) : Prop :=
  ∀ y ∈ U, ∀ A μ, E (swap23 A) μ y = conj (E A μ y)

/-- A real first-order tangent `(h, f, B)` at a background `(g, E)` on `U` (class B): `C^∞` field and frame tangents,
antisymmetric `f`, real pattern of `B`, and the first-order normalisation. (`h` symmetric and `C^∞` follow.) -/
structure RealFrameTangent (g : Metric 4) (E : Fin 4 → Fin 4 → Pt 4 → ℂ) (U : Set (Pt 4)) (h : Metric 4)
    (f : TwoForm 4) (B : Fin 4 → Fin 4 → Pt 4 → ℂ) : Prop where
  smooth_f : ∀ i j, ContDiffOn ℝ ∞ (f i j) U
  smooth_B : ∀ A μ, ContDiffOn ℝ ∞ (B A μ) U
  antisymm_f : ∀ y ∈ U, ∀ i j, f i j y = -f j i y
  real_B : RealPattern B U
  compat : FrameCompat g h E B U

/-! ### Matrix helpers -/

/-- The swap of `m` and `m̄` as a permutation. -/
def swap23Perm : Equiv.Perm (Fin 4) := Function.Involutive.toPerm swap23 swap23_swap23

section realization

variable (U : Set (Pt 4)) (g0 gi0 : Metric 4) (F0 f : TwoForm 4) (E0 Θ0 B : Fin 4 → Fin 4 → Pt 4 → ℂ)

/-- `T_ε = E₀ + ε B`. -/
def rzE (ε : ℝ) : Fin 4 → Fin 4 → Pt 4 → ℂ := fun A μ y => E0 A μ y + (ε : ℂ) * B A μ y

/-- `W = {(ε, y) | y ∈ U, det T_ε(y) ≠ 0}`. -/
def rzW : Set (ℝ × Pt 4) := {p | p.2 ∈ U ∧ (frMat (rzE E0 B p.1) p.2).det ≠ 0}

open Classical in
/-- `Θ_ε = T_ε⁻¹` on `U` (background coframe outside `U`). -/
noncomputable def rzTh (ε : ℝ) : Fin 4 → Fin 4 → Pt 4 → ℂ :=
  fun C μ y => if y ∈ U then (frMat (rzE E0 B ε) y)⁻¹ C μ else Θ0 C μ y

/-- `G_ε = Θ_εᵀ η Θ_ε` (complex; proved real on `W`). -/
noncomputable def rzGc (ε : ℝ) (μ ν : Fin 4) (y : Pt 4) : ℂ :=
  ∑ C, ∑ D, rzTh U E0 Θ0 B ε C μ y * etaNull C D * rzTh U E0 Θ0 B ε D ν y

open Classical in
/-- The real metric family `Re G_ε` on `U` (background metric outside `U`). -/
noncomputable def rzG (ε : ℝ) : Metric 4 :=
  fun μ ν y => if y ∈ U then (rzGc U E0 Θ0 B ε μ ν y).re else g0 μ ν y

/-- `GI_ε = T_ε η T_εᵀ` (complex; proved real on `W`). -/
noncomputable def rzGIc (ε : ℝ) (μ ν : Fin 4) (y : Pt 4) : ℂ :=
  ∑ C, ∑ D, rzE E0 B ε C μ y * etaNull C D * rzE E0 B ε D ν y

open Classical in
/-- The real inverse-metric family `Re GI_ε` on `U` (background inverse outside `U`). -/
noncomputable def rzGI (ε : ℝ) : Metric 4 :=
  fun μ ν y => if y ∈ U then (rzGIc E0 B ε μ ν y).re else gi0 μ ν y

/-- `F_ε = F₀ + ε f`. -/
def rzF (ε : ℝ) : TwoForm 4 := fun i j y => F0 i j y + ε * f i j y

end realization

section props

variable {U : Set (Pt 4)} {g0 gi0 : Metric 4} {F0 f : TwoForm 4} {E0 Θ0 B : Fin 4 → Fin 4 → Pt 4 → ℂ}
  {h : Metric 4}

variable (hN : NullFrameData g0 gi0 E0 Θ0 U)
include hN

end props

section family

variable {U : Set (Pt 4)} {g0 gi0 : Metric 4} {F0 f : TwoForm 4} {E0 Θ0 B : Fin 4 → Fin 4 → Pt 4 → ℂ}
  {h : Metric 4}

variable (hN : NullFrameData g0 gi0 E0 Θ0 U) (ht : RealFrameTangent g0 E0 U h f B)
include hN ht

end family

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