V-03 frame families and tangents

-- Generated by scripts/release05/gen_platform_tree.py (ATLAS-RELEASE-05) by skeleton subtraction from Atlas/EinsteinMaxwell/NP/V03Family.lean
-- definition bundle: kept ExactVacuumAtlas.EinsteinMaxwell.NP.FrameCompat, ExactVacuumAtlas.EinsteinMaxwell.NP.NPFamily, ExactVacuumAtlas.EinsteinMaxwell.NP.NPTangent, ExactVacuumAtlas.EinsteinMaxwell.NP.coVar
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_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): real one-parameter families of metrics, Maxwell fields and complex null frames

B3 class-B data (registered in `mission/PHYSICS_BOUNDARY.md` §M):

* `NPFamily g gi F E Θ W`: IV's `FamilyData` (jointly `C^∞` real metric and real field with a true inverse on an open
  `W ⊆ ℝ × ℝ⁴`), a jointly `C^∞` complex frame `E` and coframe `Θ`, a **null frame** on every slice
  `{y | (ε, y) ∈ W}` (V-02's `NullFrameData`: symmetric metric, true inverse, dual coframe, Gram matrix `etaNull`), and
  an antisymmetric field. No field equation, no Petrov type and no gauge condition is assumed for any `ε`.
* `NPTangent g F E W h f B`: `(h, f)` are the genuine parameter derivatives of `(g, F)` (IV's `IsTangent`) and `B` that
  of the frame, at `ε = 0` on the slice.
* `FrameCompat g h E B U`: the first-order normalisation `h(e_A,e_C) + g(b_A,e_C) + g(e_A,b_C) = 0`.
* `coVar Θ B`: `δθ = −Θ B Θ` (matrix form), the first variation of the dual coframe.

Proved (genuine derivatives, no jets): the tangent of every `NPFamily` has `h` symmetric, `f` antisymmetric, satisfies
`FrameCompat` (derivative of the constant Gram matrix) and has coframe variation `coVar` (derivative of the duality
relation). The converse (every compatible real tangent is realised by a family) is `V03Realize.lean`. -/

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

namespace ExactVacuumAtlas.EinsteinMaxwell.NP

/-- A real one-parameter family `(g_ε, gi_ε, F_ε)` with a complex null frame `(E_ε, Θ_ε)` on every slice (class B). -/
structure NPFamily (g gi : ℝ → Metric 4) (F : ℝ → TwoForm 4) (E Θ : ℝ → Fin 4 → Fin 4 → Pt 4 → ℂ)
    (W : Set (ℝ × Pt 4)) : Prop where
  fam : FamilyData g gi F W
  smooth_E : ∀ A μ, ContDiffOn ℝ ∞ (fun p : ℝ × Pt 4 => E p.1 A μ p.2) W
  smooth_Θ : ∀ A μ, ContDiffOn ℝ ∞ (fun p : ℝ × Pt 4 => Θ p.1 A μ p.2) W
  null : ∀ ε, NullFrameData (g ε) (gi ε) (E ε) (Θ ε) {y | (ε, y) ∈ W}
  antisymm : ∀ p ∈ W, ∀ i j, F p.1 i j p.2 = -F p.1 j i p.2

/-- `(h, f, B)` are the genuine parameter derivatives at `ε = 0` of `(g, F, E)` on the slice (class B). -/
structure NPTangent (g : ℝ → 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 → ℂ) : Prop where
  tangent : IsTangent g F W h f
  frame : ∀ y, ((0 : ℝ), y) ∈ W → ∀ A μ, HasDerivAt (fun ε => E ε A μ y) (B A μ y) 0

/-- First-order normalisation of a frame tangent (class B): `h(e_A,e_C) + g(b_A,e_C) + g(e_A,b_C) = 0` on `U`. -/
def FrameCompat (g h : Metric 4) (E B : Fin 4 → Fin 4 → Pt 4 → ℂ) (U : Set (Pt 4)) : Prop :=
  ∀ y ∈ U, ∀ A C, ccontr h y (fvec E A y) (fvec E C y) + ccontr g y (fvec B A y) (fvec E C y)
    + ccontr g y (fvec E A y) (fvec B C y) = 0

/-- First variation of the dual coframe, `δθ^C_ν = −Σ_{A,μ} θ^C_μ b_A^μ θ^A_ν` (class B notation). -/
noncomputable def coVar (Θ B : Fin 4 → Fin 4 → Pt 4 → ℂ) (C ν : Fin 4) (y : Pt 4) : ℂ :=
  -∑ A, ∑ μ, Θ C μ y * B A μ y * Θ A ν y

/-! ### Generic tools -/

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

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