Prove2Me

V-03 explicit first variations

Definition
Atlas_EinsteinMaxwell_NP_V03Var

by He Wang · Oct 23, 2026 · Mathlib 0df444a (Lean v4.33.1)

einstein-maxwellexact-spacetime-atlas-vexact-vacuum-atlasgeneral-relativitynewman-penrose

V-03 explicit first variations

riemVar, riemLowVar, weylVar, weylFVar, ricFVar, FfrFVar, brkVar, cLVar, omLVar, HfrVar, JfrVar and the named NP variations psi0/1/3/4Var, kappa/sigma/nu/lambdaVar, phi0/phi2Var (explicit sums; proved equal to genuine derivatives).

中文摘要 V-03 显式一阶变分（已证明等于真实导数）。

Registry: PHYSICS_BOUNDARY §M (V-03) M1–M4.

Definition code
-- Generated by scripts/release05/gen_platform_tree.py (ATLAS-RELEASE-05) by skeleton subtraction from Atlas/EinsteinMaxwell/NP/V03Var.lean
-- definition bundle: kept ExactVacuumAtlas.EinsteinMaxwell.NP.FfrFVar, ExactVacuumAtlas.EinsteinMaxwell.NP.HfrVar, ExactVacuumAtlas.EinsteinMaxwell.NP.JfrVar, ExactVacuumAtlas.EinsteinMaxwell.NP.brkVar, ExactVacuumAtlas.EinsteinMaxwell.NP.cLVar, ExactVacuumAtlas.EinsteinMaxwell.NP.kappaVar, ExactVacuumAtlas.EinsteinMaxwell.NP.lambdaVar, ExactVacuumAtlas.EinsteinMaxwell.NP.nuVar, ExactVacuumAtlas.EinsteinMaxwell.NP.omLVar, ExactVacuumAtlas.EinsteinMaxwell.NP.phi0Var, ExactVacuumAtlas.EinsteinMaxwell.NP.phi2Var, ExactVacuumAtlas.EinsteinMaxwell.NP.psi0Var, ExactVacuumAtlas.EinsteinMaxwell.NP.psi1Var, ExactVacuumAtlas.EinsteinMaxwell.NP.psi3Var, ExactVacuumAtlas.EinsteinMaxwell.NP.psi4Var, ExactVacuumAtlas.EinsteinMaxwell.NP.ricFVar, ExactVacuumAtlas.EinsteinMaxwell.NP.riemLowVar, ExactVacuumAtlas.EinsteinMaxwell.NP.riemVar, ExactVacuumAtlas.EinsteinMaxwell.NP.sigmaVar, ExactVacuumAtlas.EinsteinMaxwell.NP.weylFVar, ExactVacuumAtlas.EinsteinMaxwell.NP.weylVar
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_V03Realize
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 B): explicit first variations of the NP quantities and their genuine-derivative bridges

B3 local definitions (registered in `mission/PHYSICS_BOUNDARY.md` §M). Each is an **explicit formula** in the
background `(g, gi, F, E, Θ)` and the tangent `(h, f, B)`; none is defined as a derivative. IV's `chrVar`, `ricciVar`,
`scalarVar`, `invVar`, `linEinstein`, `linMaxwell`, `linFaraday` are reused unchanged.

* `riemVar`: `δR^a_{bcd} = ∂_c C^a_{db} − ∂_d C^a_{cb} + Σ_e (C^a_{ce}Γ^e_{db} + Γ^a_{ce}C^e_{db} − C^a_{de}Γ^e_{cb}
  − Γ^a_{de}C^e_{cb})` with `C = chrVar` (the expansion `riem_expand` of II's `curv`, varied);
* `riemLowVar`: `δR_{abcd} = Σ_e (h_{ae} R^e_{bcd} + g_{ae} δR^e_{bcd})` (lowering with `g` is varied);
* `weylVar`: variation of V-02's `weyl` keeping `h`, `δRic` (`ricciVar`) and `δR` (`scalarVar`) — no background
  value is used to drop terms;
* `weylFVar`, `ricFVar`, `FfrFVar`: variations of the frame contractions **including all frame factors**, e.g.
  `δ[F(e_A,e_B)] = f(e_A,e_B) + F(b_A,e_B) + F(e_A,b_B)`;
* `brkVar`, `cLVar`, `omLVar`: variations of the commutator `[e_A,e_B]`, of `cL = g(e_C,[e_A,e_B])` (metric varied),
  and of the connection components through the Koszul formula `omL_koszul` (valid for every null frame);
* `HfrVar`, `JfrVar`: variations of `H(e,e,e)` and of `θ^K(J)` (coframe varied by `coVar`).

Bridges (`NPFamily.hasDerivAt_*`): for every `NPFamily` with tangent `(h, f, B)`, the parameter derivative at
`ε = 0` of each registered quantity equals the explicit formula. -/

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

namespace ExactVacuumAtlas.EinsteinMaxwell.NP

section defs

variable {n : ℕ}

/-- First variation of `R^a_{bcd}` (explicit coordinate formula). -/
noncomputable def riemVar (g gi h : Metric n) (a b c d : Fin n) (x : Pt n) : ℝ :=
  pd c (chrVar g gi h a d b) x - pd d (chrVar g gi h a c b) x
    + ∑ e, (chrVar g gi h a c e x * christoffel g gi e d b x + christoffel g gi a c e x * chrVar g gi h e d b x
      - (chrVar g gi h a d e x * christoffel g gi e c b x + christoffel g gi a d e x * chrVar g gi h e c b x))

/-- First variation of `R_{abcd} = Σ_e g_{ae} R^e_{bcd}`. -/
noncomputable def riemLowVar (g gi h : Metric n) (a b c d : Fin n) (x : Pt n) : ℝ :=
  ∑ e, (h a e x * riem g gi e b c d x + g a e x * riemVar g gi h e b c d x)

end defs

/-- First variation of the 4D Weyl tensor `C_{abcd}` (all variations of `g`, `Ric`, `R` kept). -/
noncomputable def weylVar (g gi h : Metric 4) (a b c d : Fin 4) (x : Pt 4) : ℝ :=
  riemLowVar g gi h a b c d x
    - (h a c x * ricciOf g gi b d x + g a c x * ricciVar g gi h b d x
        - (h a d x * ricciOf g gi b c x + g a d x * ricciVar g gi h b c x)
        - (h b c x * ricciOf g gi a d x + g b c x * ricciVar g gi h a d x)
        + (h b d x * ricciOf g gi a c x + g b d x * ricciVar g gi h a c x)) / 2
    + (scalarVar g gi h x * (g a c x * g b d x - g a d x * g b c x)
        + ricciScalar g gi x * (h a c x * g b d x + g a c x * h b d x - (h a d x * g b c x + g a d x * h b c x))) / 6

/-- First variation of `C(e_I, e_J, e_A, e_K)` (Weyl variation plus the four frame-variation terms). -/
noncomputable def weylFVar (g gi h : Metric 4) (E B : Fin 4 → Fin 4 → Pt 4 → ℂ) (I J A K : Fin 4) (x : Pt 4) : ℂ :=
  ccontr4 (weylVar g gi h) x (fvec E I x) (fvec E J x) (fvec E A x) (fvec E K x)
    + ccontr4 (weyl g gi) x (fvec B I x) (fvec E J x) (fvec E A x) (fvec E K x)
    + ccontr4 (weyl g gi) x (fvec E I x) (fvec B J x) (fvec E A x) (fvec E K x)
    + ccontr4 (weyl g gi) x (fvec E I x) (fvec E J x) (fvec B A x) (fvec E K x)
    + ccontr4 (weyl g gi) x (fvec E I x) (fvec E J x) (fvec E A x) (fvec B K x)

/-- First variation of `Ric(e_A, e_K)`. -/
noncomputable def ricFVar (g gi h : Metric 4) (E B : Fin 4 → Fin 4 → Pt 4 → ℂ) (A K : Fin 4) (x : Pt 4) : ℂ :=
  ccontr (ricciVar g gi h) x (fvec E A x) (fvec E K x) + ccontr (ricciOf g gi) x (fvec B A x) (fvec E K x)
    + ccontr (ricciOf g gi) x (fvec E A x) (fvec B K x)

/-- First variation of `F(e_A, e_K)`: `f(e_A,e_K) + F(b_A,e_K) + F(e_A,b_K)`. -/
noncomputable def FfrFVar (F f : TwoForm 4) (E B : Fin 4 → Fin 4 → Pt 4 → ℂ) (A K : Fin 4) (x : Pt 4) : ℂ :=
  ccontr f x (fvec E A x) (fvec E K x) + ccontr F x (fvec B A x) (fvec E K x) + ccontr F x (fvec E A x) (fvec B K x)

/-- First variation of the commutator components `[e_A, e_K]^μ`. -/
noncomputable def brkVar (E B : Fin 4 → Fin 4 → Pt 4 → ℂ) (A K μ : Fin 4) (x : Pt 4) : ℂ :=
  fdir B A (E K μ) x + fdir E A (B K μ) x - (fdir B K (E A μ) x + fdir E K (B A μ) x)

/-- First variation of `cL C A K = g(e_C, [e_A, e_K])` (metric, frame vector and commutator varied). -/
noncomputable def cLVar (g h : Metric 4) (E B : Fin 4 → Fin 4 → Pt 4 → ℂ) (C A K : Fin 4) (x : Pt 4) : ℂ :=
  ccontr h x (fvec E C x) (fun μ => brk E A K μ x) + ccontr g x (fvec B C x) (fun μ => brk E A K μ x)
    + ccontr g x (fvec E C x) (fun μ => brkVar E B A K μ x)

/-- First variation of the connection components `omL C A K = g(e_C, ∇_{e_A} e_K)` (Koszul form). -/
noncomputable def omLVar (g h : Metric 4) (E B : Fin 4 → Fin 4 → Pt 4 → ℂ) (C A K : Fin 4) (x : Pt 4) : ℂ :=
  (cLVar g h E B C A K x - cLVar g h E B A K C x + cLVar g h E B K C A x) / 2

/-- First variation of `H(e_A, e_K, e_C)`. -/
noncomputable def HfrVar (F f : TwoForm 4) (E B : Fin 4 → Fin 4 → Pt 4 → ℂ) (A K C : Fin 4) (x : Pt 4) : ℂ :=
  ∑ μ, ∑ ν, ∑ l, ((linFaraday f μ ν l x : ℂ) * E A μ x * E K ν x * E C l x
    + (faradayCyclic F μ ν l x : ℂ) * B A μ x * E K ν x * E C l x
    + (faradayCyclic F μ ν l x : ℂ) * E A μ x * B K ν x * E C l x
    + (faradayCyclic F μ ν l x : ℂ) * E A μ x * E K ν x * B C l x)

/-- First variation of `θ^K(J)` (coframe varied by `coVar`, `J` by IV's `linMaxwell`). -/
noncomputable def JfrVar (g gi : Metric 4) (F : TwoForm 4) (h : Metric 4) (f : TwoForm 4)
    (Θ B : Fin 4 → Fin 4 → Pt 4 → ℂ) (K : Fin 4) (x : Pt 4) : ℂ :=
  ∑ b, (coVar Θ B K b x * (maxwellDiv g gi F b x : ℂ) + Θ K b x * (linMaxwell g gi F h f b x : ℂ))

/-! ### Named NP variations (readability of the final statements) -/

/-- `δΨ₀`. -/ noncomputable def psi0Var (g gi h : Metric 4) (E B : Fin 4 → Fin 4 → Pt 4 → ℂ) (x : Pt 4) : ℂ :=
  weylFVar g gi h E B 0 2 0 2 x
/-- `δΨ₁`. -/ noncomputable def psi1Var (g gi h : Metric 4) (E B : Fin 4 → Fin 4 → Pt 4 → ℂ) (x : Pt 4) : ℂ :=
  weylFVar g gi h E B 0 1 0 2 x
/-- `δΨ₃`. -/ noncomputable def psi3Var (g gi h : Metric 4) (E B : Fin 4 → Fin 4 → Pt 4 → ℂ) (x : Pt 4) : ℂ :=
  weylFVar g gi h E B 0 1 3 1 x
/-- `δΨ₄`. -/ noncomputable def psi4Var (g gi h : Metric 4) (E B : Fin 4 → Fin 4 → Pt 4 → ℂ) (x : Pt 4) : ℂ :=
  weylFVar g gi h E B 1 3 1 3 x
/-- `δκ`. -/ noncomputable def kappaVar (g h : Metric 4) (E B : Fin 4 → Fin 4 → Pt 4 → ℂ) (x : Pt 4) : ℂ :=
  omLVar g h E B 0 0 2 x
/-- `δσ`. -/ noncomputable def sigmaVar (g h : Metric 4) (E B : Fin 4 → Fin 4 → Pt 4 → ℂ) (x : Pt 4) : ℂ :=
  omLVar g h E B 0 2 2 x
/-- `δν`. -/ noncomputable def nuVar (g h : Metric 4) (E B : Fin 4 → Fin 4 → Pt 4 → ℂ) (x : Pt 4) : ℂ :=
  -omLVar g h E B 1 1 3 x
/-- `δλ`. -/ noncomputable def lambdaVar (g h : Metric 4) (E B : Fin 4 → Fin 4 → Pt 4 → ℂ) (x : Pt 4) : ℂ :=
  -omLVar g h E B 1 3 3 x
/-- `δΦ₀ = δ[F(l,m)]`. -/ noncomputable def phi0Var (F f : TwoForm 4) (E B : Fin 4 → Fin 4 → Pt 4 → ℂ)
    (x : Pt 4) : ℂ := FfrFVar F f E B 0 2 x
/-- `δΦ₂ = δ[F(m̄,n)]`. -/ noncomputable def phi2Var (F f : TwoForm 4) (E B : Fin 4 → Fin 4 → Pt 4 → ℂ)
    (x : Pt 4) : ℂ := FfrFVar F f E B 3 1 x

/-! ### Bridges -/

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) {x : Pt 4} (hx : ((0 : ℝ), x) ∈ W)
include hF ht hx

end NPFamily

end ExactVacuumAtlas.EinsteinMaxwell.NP
Source
He Wang, Exact Spacetime Atlas V: From Linearized Einstein–Maxwell Equations to Kerr–Newman Radiation Systems. Local source, no public repository; commit b8cd107a558e153ed41fb4972ac5315499d14778; Atlas/EinsteinMaxwell/NP/V03Var.lean; SHA-256 208236fc7bbbf59f60939aacdcc4f56b54f83656fb1b932f24ef4e179bf07389. Registered definitions: mission/PHYSICS_BOUNDARY.md (§K–§M); literature: P. Hintz, arXiv:2609.33661 (v1); Mark–Yang–Zimmerman–Chen, arXiv:1409.5800 (v1).
Human review

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

View graph