First-variation operators and family contracts

-- Generated by scripts/release04/gen_platform_tree.py (ATLAS-RELEASE-04) by skeleton subtraction from Atlas/EinsteinMaxwell/Variation/Defs.lean
-- definition bundle: kept ExactVacuumAtlas.Variation.FamilyData, ExactVacuumAtlas.Variation.IsTangent, ExactVacuumAtlas.Variation.chrVar, ExactVacuumAtlas.Variation.emStressVar, ExactVacuumAtlas.Variation.fieldSqVar, ExactVacuumAtlas.Variation.gradCo, ExactVacuumAtlas.Variation.invVar, ExactVacuumAtlas.Variation.lieCov2, ExactVacuumAtlas.Variation.linEinstein, ExactVacuumAtlas.Variation.linFaraday, ExactVacuumAtlas.Variation.linMaxwell, ExactVacuumAtlas.Variation.paramTangent, ExactVacuumAtlas.Variation.raise2Var, ExactVacuumAtlas.Variation.ricciLin, ExactVacuumAtlas.Variation.ricciVar, ExactVacuumAtlas.Variation.scalarVar
import Mathlib
import Definitions.Def_Atlas_Core_Basic
import Definitions.Def_Atlas_EinsteinMaxwell_Basic
/-! # Explicit first-variation operators of the Einstein–Maxwell residual (ATLAS-IV-03)

B3 local definition layer (`mission/PHYSICS_BOUNDARY.md` §I). Every operator below is an **explicit
finite-coordinate formula** in the background `(g, ginv, F)` and the perturbation `(h, f)`; none of them
is defined as a derivative. That they *are* the first variations of the registered nonlinear objects
(`christoffel`, `ricciOf`, `raise2`, `fieldSq`, `ricciScalar`, `emStress`, `einsteinMaxwell`,
`maxwellDiv`, `faradayCyclic`, unchanged) is proved in `Atlas/EinsteinMaxwell/Variation/Bridge.lean`.

Index conventions are those of the nonlinear layer: `christoffel g ginv a b c = Γ^a_{bc}`; all sums are
explicit `Fin` sums; `F`, `f`, `h` carry lower indices. `ginv` is the background inverse (written
`G^{ab}` in the contract, never the Einstein tensor). Generic objects are stated for total dimension `n`;
the residual pieces `emStressVar`, `linEinstein` are 4-dimensional, like `emStress`, `einsteinMaxwell`.

* `invVar ginv h`: `K^{ab} = -Σ_{c,d} G^{ac} h_{cd} G^{db}`.
* `chrVar g ginv h`: `C^a_{bc} = ½ Σ_k [K^{ak}(∂_c g_{kb} + ∂_b g_{kc} - ∂_k g_{bc}) + G^{ak}(∂_c h_{kb} + ∂_b h_{kc} - ∂_k h_{bc})]`.
* `ricciLin Γ C`: linearisation of the registered `ricci` at a connection `Γ` along `C`:
  `Σ_i [∂_i C^i_{bd} - ∂_d C^i_{bi} + Σ_j (C^i_{ij}Γ^j_{bd} + Γ^i_{ij}C^j_{bd} - C^i_{dj}Γ^j_{bi} - Γ^i_{dj}C^j_{bi})]`;
  `ricciVar g ginv h = ricciLin (christoffel g ginv) (chrVar g ginv h)`.
* `scalarVar`: `δR = Σ_{a,b} (K^{ab} R_{ab} + G^{ab} δR_{ab})` (the `K·Ric` term is kept).
* `raise2Var`: `V^{ab} = Σ_{c,d} (K^{ac}G^{bd}F_{cd} + G^{ac}K^{bd}F_{cd} + G^{ac}G^{bd}f_{cd})`.
* `fieldSqVar`: `δ(F·F) = Σ_{a,b} (f_{ab}F^{ab} + F_{ab}V^{ab})`.
* `emStressVar`: `δS_{ab} = Σ_{c,d}(f_{ac}G^{cd}F_{bd} + F_{ac}K^{cd}F_{bd} + F_{ac}G^{cd}f_{bd}) - ¼(h_{ab} s + g_{ab} δs)`.
* `linEinstein`: `LE_{ab} = δR_{ab} - ½(h_{ab} R + g_{ab} δR) - 2 δS_{ab}`.
* `linMaxwell`: `LJ^b = Σ_a [∂_a V^{ab} + Σ_k (C^a_{ak}F^{kb} + Γ^a_{ak}V^{kb} + C^b_{ak}F^{ak} + Γ^b_{ak}V^{ak})]`.
* `linFaraday`: `LH_{abc} = ∂_a f_{bc} + ∂_b f_{ca} + ∂_c f_{ab}`.
* `lieCov2 ξ T`: coordinate Lie derivative of a covariant 2-tensor,
  `(L_ξ T)_{ab} = Σ_c (ξ^c ∂_c T_{ab} + T_{cb} ∂_a ξ^c + T_{ac} ∂_b ξ^c)`.

Class B: `FamilyData` (joint `C^∞` real parameter family with a true inverse on an open `W ⊆ ℝ × ℝⁿ`)
and `IsTangent` (genuine parameter derivatives at `ε = 0` on the slice). -/

open scoped ContDiff
open ExactVacuumAtlas.EinsteinMaxwell

namespace ExactVacuumAtlas.Variation

variable {n : ℕ}

/-- `K^{ab} = -Σ_{c,d} G^{ac} h_{cd} G^{db}` (first variation of the inverse metric). -/
noncomputable def invVar (ginv h : Metric n) : Metric n :=
  fun a b y => -∑ c : Fin n, ∑ d : Fin n, ginv a c y * h c d y * ginv d b y

/-- First variation `C^a_{bc}` of the Christoffel symbols (coordinate formula). -/
noncomputable def chrVar (g ginv h : Metric n) (a b c : Fin n) (y : Pt n) : ℝ :=
  (∑ k : Fin n, (invVar ginv h a k y * (pd c (g k b) y + pd b (g k c) y - pd k (g b c) y) +
    ginv a k y * (pd c (h k b) y + pd b (h k c) y - pd k (h b c) y))) / 2

/-- Linearisation of the registered `ricci` at the connection `Γ` along the variation `C`. -/
noncomputable def ricciLin (Γ C : Fin n → Fin n → Fin n → Pt n → ℝ) (b d : Fin n) (y : Pt n) : ℝ :=
  ∑ i : Fin n, (pd i (C i b d) y - pd d (C i b i) y +
    ∑ j : Fin n, ((C i i j y * Γ j b d y + Γ i i j y * C j b d y) -
      (C i d j y * Γ j b i y + Γ i d j y * C j b i y)))

/-- First variation of the Ricci tensor of `g`. -/
noncomputable def ricciVar (g ginv h : Metric n) : Fin n → Fin n → Pt n → ℝ :=
  ricciLin (christoffel g ginv) (chrVar g ginv h)

/-- First variation of the Ricci scalar: `Σ_{a,b} (K^{ab} R_{ab} + G^{ab} δR_{ab})`. -/
noncomputable def scalarVar (g ginv h : Metric n) (y : Pt n) : ℝ :=
  ∑ a : Fin n, ∑ b : Fin n, (invVar ginv h a b y * ricciOf g ginv a b y + ginv a b y * ricciVar g ginv h a b y)

/-- First variation `V^{ab}` of the doubly raised field (both raisings vary). -/
noncomputable def raise2Var (ginv h : Metric n) (F f : TwoForm n) (a b : Fin n) (y : Pt n) : ℝ :=
  ∑ c : Fin n, ∑ d : Fin n, (invVar ginv h a c y * ginv b d y * F c d y +
    ginv a c y * invVar ginv h b d y * F c d y + ginv a c y * ginv b d y * f c d y)

/-- First variation of the invariant `F_{ab}F^{ab}`. -/
noncomputable def fieldSqVar (ginv h : Metric n) (F f : TwoForm n) (y : Pt n) : ℝ :=
  ∑ a : Fin n, ∑ b : Fin n, (f a b y * raise2 ginv F a b y + F a b y * raise2Var ginv h F f a b y)

/-- First variation of the 4D Maxwell stress tensor `S_{ab}`. -/
noncomputable def emStressVar (g ginv h : Metric 4) (F f : TwoForm 4) (a b : Fin 4) (y : Pt 4) : ℝ :=
  (∑ c : Fin 4, ∑ d : Fin 4, (f a c y * ginv c d y * F b d y + F a c y * invVar ginv h c d y * F b d y +
    F a c y * ginv c d y * f b d y)) - (h a b y * fieldSq ginv F y + g a b y * fieldSqVar ginv h F f y) / 4

/-- **Linearised Einstein–Maxwell residual** `LE_{ab}(h, f)` (4D). -/
noncomputable def linEinstein (g ginv : Metric 4) (F : TwoForm 4) (h : Metric 4) (f : TwoForm 4)
    (a b : Fin 4) (y : Pt 4) : ℝ :=
  ricciVar g ginv h a b y - (h a b y * ricciScalar g ginv y + g a b y * scalarVar g ginv h y) / 2 -
    2 * emStressVar g ginv h F f a b y

/-- **Linearised Maxwell divergence** `LJ^b(h, f)`. -/
noncomputable def linMaxwell (g ginv : Metric n) (F : TwoForm n) (h : Metric n) (f : TwoForm n)
    (b : Fin n) (y : Pt n) : ℝ :=
  ∑ a : Fin n, (pd a (raise2Var ginv h F f a b) y +
    ∑ k : Fin n, ((chrVar g ginv h a a k y * raise2 ginv F k b y +
        christoffel g ginv a a k y * raise2Var ginv h F f k b y) +
      (chrVar g ginv h b a k y * raise2 ginv F a k y +
        christoffel g ginv b a k y * raise2Var ginv h F f a k y)))

/-- **Linearised closure residual** `LH_{abc}(f) = ∂_a f_{bc} + ∂_b f_{ca} + ∂_c f_{ab}`. -/
noncomputable def linFaraday (f : TwoForm n) (a b c : Fin n) (y : Pt n) : ℝ :=
  pd a (f b c) y + pd b (f c a) y + pd c (f a b) y

/-- Coordinate Lie derivative of a covariant 2-tensor along the vector field `ξ` (components `ξ^c`):
`(L_ξ T)_{ab} = Σ_c (ξ^c ∂_c T_{ab} + T_{cb} ∂_a ξ^c + T_{ac} ∂_b ξ^c)`. -/
noncomputable def lieCov2 (ξ : Fin n → Pt n → ℝ) (T : Fin n → Fin n → Pt n → ℝ) (a b : Fin n) (y : Pt n) : ℝ :=
  ∑ c : Fin n, (ξ c y * pd c (T a b) y + T c b y * pd a (ξ c) y + T a c y * pd b (ξ c) y)

/-- Gradient covector `α_a = ∂_a χ` of a scalar `χ` (the potential gauge direction `α = dχ`). -/
noncomputable def gradCo (χ : Pt n → ℝ) : CoVec n := fun a => pd a χ

/-! ## Real parameter families -/

/-- A real one-parameter family `(g_ε, ginv_ε, F_ε)` on an open set `W ⊆ ℝ × ℝⁿ` (class B):
jointly `C^∞` metric and field in `(ε, y)` and a true (left) inverse at every point of `W`.
No field equation, symmetry, signature or antisymmetry is assumed. -/
structure FamilyData (g ginv : ℝ → Metric n) (F : ℝ → TwoForm n) (W : Set (ℝ × Pt n)) : Prop where
  isOpen : IsOpen W
  smooth : ∀ i j, ContDiffOn ℝ ∞ (fun p : ℝ × Pt n => g p.1 i j p.2) W
  smooth_F : ∀ i j, ContDiffOn ℝ ∞ (fun p : ℝ × Pt n => F p.1 i j p.2) W
  inv : ∀ p ∈ W, metricMatrix (ginv p.1) p.2 * metricMatrix (g p.1) p.2 = 1

/-- `(h, f)` are the genuine parameter derivatives at `ε = 0` of the family, on the slice
`{y | (0, y) ∈ W}` (class B). -/
structure IsTangent (g : ℝ → Metric n) (F : ℝ → TwoForm n) (W : Set (ℝ × Pt n)) (h : Metric n)
    (f : TwoForm n) : Prop where
  metric : ∀ y, ((0 : ℝ), y) ∈ W → ∀ i j, HasDerivAt (fun ε => g ε i j y) (h i j y) 0
  field : ∀ y, ((0 : ℝ), y) ∈ W → ∀ i j, HasDerivAt (fun ε => F ε i j y) (f i j y) 0

/-- The tangent of a family at `ε = 0`: componentwise parameter derivative (class B notation for the
*family's* tangent; the operators above are never defined through derivatives). -/
noncomputable def paramTangent (T : ℝ → Fin n → Fin n → Pt n → ℝ) : Fin n → Fin n → Pt n → ℝ :=
  fun i j y => deriv (fun ε => T ε i j y) 0

end ExactVacuumAtlas.Variation

• Endorsed by Shuze Chen · Oct 21, 2026

  Confirmed by the moderator at approval.

• Endorsed by He Wang · Oct 21, 2026

  Confirmed by the mission captain (proposal self-audit).