V-03 frame projection of L_E

-- Generated by scripts/release05/gen_platform_tree.py (ATLAS-RELEASE-05) by skeleton subtraction from Atlas/EinsteinMaxwell/NP/V03Src.lean
-- definition bundle: kept ExactVacuumAtlas.EinsteinMaxwell.NP.LEfr
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_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): the sources of the linearised identities in IV's residuals `L_E`, `L_J`, `L_H`

* `ricF_src_eta0`: for a frame pair with `η_{AK} = 0`, V-02's `ricF_eq_source` and `emStressF_eq` give
  `Ric(e_A,e_K) = 2 Σ_{CD} F(e_A,e_C) η^{CD} F(e_K,e_D) + E(e_A,e_K)` (every null frame, every `F`, off shell).
* `NPFamily.ricFVar_eta0`: its genuine first variation along a family (derivative uniqueness on the open slice):
  `δRic(e_A,e_K) = 2 Σ (δF_{AC} η^{CD} F_{KD} + F_{AC} η^{CD} δF_{KD}) + L_E(e_A,e_K) + E(b_A,e_K) + E(e_A,b_K)`.
* At Kerr–Newman (`KNFam`): `E = 0` (`certReg`), the background frame Faraday matrix has only `F_{ln}`, `F_{m m̄}`,
  and `F_{ln} + F_{m m̄} = Q / q²` (`q = r + i a cos θ`), so
  `δRic_{02} = L_E(l,m) + (2Q/q²) δΦ₀`, `δRic_{13} = L_E(n,m̄) + (2Q/q²) δΦ₂`, and `δRic_{AA} = L_E(e_A,e_A)`
  (`A = 0,1,2,3`); `HfrVar` is the three-frame contraction of `L_H` and `JfrVar` the coframe applied to `L_J`
  (`dF = 0`, `J = 0` at KN). No new stress tensor or residual is introduced. -/

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

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

end NPFamily

section kn

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

/-- Shorthand for the frame projection `L_E(e_A, e_K)` of IV's linearised Einstein residual at KN (class B). -/
noncomputable abbrev LEfr (M a Q : ℝ) (h : Metric 4) (f : TwoForm 4) (A K : Fin 4) (y : Pt 4) : ℂ :=
  ccontr (linEinstein (gKN M a Q) (giKN M a Q) (faradayKN a Q) h f) y (fvec (knE M a Q) A y) (fvec (knE M a Q) K y)

end kn

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