Local coordinate family for the diffeomorphism gauge

-- Generated by scripts/release04/gen_platform_tree.py (ATLAS-RELEASE-04) by skeleton subtraction from Atlas/EinsteinMaxwell/Variation/Gauge.lean
-- definition bundle: kept ExactVacuumAtlas.Variation.pullCov, ExactVacuumAtlas.Variation.pullInv, ExactVacuumAtlas.Variation.shiftDom, ExactVacuumAtlas.Variation.shiftJac, ExactVacuumAtlas.Variation.shiftMap
import Mathlib
import Definitions.Def_Atlas_Core_Basic
import Definitions.Def_Atlas_Core_Certificate
import Definitions.Def_Atlas_EinsteinMaxwell_Basic
import Definitions.Def_Atlas_EinsteinMaxwell_Certificate
import Definitions.Def_Atlas_EinsteinMaxwell_Variation_Defs
import Definitions.Def_Atlas_EinsteinMaxwell_Variation_Local
import Definitions.Def_Atlas_Transport_Connection
import Definitions.Def_Atlas_Transport_MatrixCalc
/-! # Gauge directions of the linearised Einstein–Maxwell operator (ATLAS-IV-03)

**Diffeomorphism gauge** (`linearized_lie_eq_zero`). Background `(g, gi, F)` with a full
`EinsteinMaxwellCertificate` on an open `U` (4D); `ξ` an **arbitrary** coordinate vector field with
`C^∞` components on `U` (not Killing, not constant, not zero). Then for the coordinate Lie derivatives

  `h = L_ξ g`, `f = L_ξ F`  (`lieCov2`, `(L_ξ T)_{ab} = Σ_c (ξ^c ∂_c T_{ab} + T_{cb} ∂_a ξ^c + T_{ac} ∂_b ξ^c)`)

`LE = 0`, `LJ = 0`, `LH = 0` at every point of `U`. Route: the genuine real family of coordinate changes
`Φ_ε(y) = y + ε ξ(y)` (class B `shiftMap`) with Jacobian `J_ε = 1 + ε Dξ` and inverse `K_ε = J_ε⁻¹`, on the
open set `shiftDom U ξ = {(ε, y) | y ∈ U, Φ_ε y ∈ U, det J_ε(y) ≠ 0}` (it contains `{0} × U`; no uniform
`ε`-interval over `U` is claimed). The pulled-back family `(J_εᵀ g(Φ_ε) J_ε, K_ε gi(Φ_ε) K_εᵀ, J_εᵀ F(Φ_ε) J_ε)`
is jointly `C^∞`, has a true inverse, solves `E = J = H = 0` on `shiftDom` by the covariance laws of
`Covariance.lean` (proved, not assumed), and its genuine tangent at `ε = 0` is `(L_ξ g, L_ξ F)`; the off-shell
bridge then gives the claim.

**Electromagnetic-potential gauge** (`extD_gradCo`, `linEinstein_potential_gauge`, …): for a `C^∞` scalar `χ`
on an open `U`, `d(dχ) = 0` on `U`, so the field variation `f = d(dχ)` changes none of `LE`, `LJ`, `LH`
(for any background and any `(h, f)`); in particular `L(0, d(dχ)) = 0`. -/

open Filter Topology
open scoped ContDiff
open Matrix
open ExactVacuumAtlas.EinsteinMaxwell

namespace ExactVacuumAtlas.Variation

variable {n : ℕ}

/-! ## The coordinate-change family -/

/-- `Φ_ε(y) = y + ε ξ(y)` (class B). -/
def shiftMap (ξ : Fin n → Pt n → ℝ) (ε : ℝ) (y : Pt n) : Pt n := fun k => y k + ε * ξ k y

/-- `J_ε(y) = 1 + ε Dξ(y)`, `(Dξ)^k_i = ∂_i ξ^k` (class B). -/
noncomputable def shiftJac (ξ : Fin n → Pt n → ℝ) (ε : ℝ) (y : Pt n) : Matrix (Fin n) (Fin n) ℝ :=
  1 + ε • Matrix.of (fun k i => pd i (ξ k) y)

/-- Pull-back of a covariant 2-tensor along `Φ_ε` (class B). -/
noncomputable def pullCov (ξ : Fin n → Pt n → ℝ) (T : Fin n → Fin n → Pt n → ℝ) (ε : ℝ) :
    Fin n → Fin n → Pt n → ℝ :=
  fun a b y => ((shiftJac ξ ε y)ᵀ * metricMatrix T (shiftMap ξ ε y) * shiftJac ξ ε y) a b

/-- Push-forward of the inverse metric along `Φ_ε`: `K_ε gi(Φ_ε) K_εᵀ`, `K_ε = J_ε⁻¹` (class B). -/
noncomputable def pullInv (ξ : Fin n → Pt n → ℝ) (gi : Metric n) (ε : ℝ) : Metric n :=
  fun a b y => ((shiftJac ξ ε y)⁻¹ * metricMatrix gi (shiftMap ξ ε y) * ((shiftJac ξ ε y)⁻¹)ᵀ) a b

/-- The open parameter/coordinate domain of the family (class B). -/
def shiftDom (U : Set (Pt n)) (ξ : Fin n → Pt n → ℝ) : Set (ℝ × Pt n) :=
  {p | p.2 ∈ U ∧ shiftMap ξ p.1 p.2 ∈ U ∧ (shiftJac ξ p.1 p.2).det ≠ 0}

section regularity

variable {U : Set (Pt n)} (hU : IsOpen U) {ξ : Fin n → Pt n → ℝ} (hξ : ∀ k, ContDiffOn ℝ ∞ (ξ k) U)
include hU hξ

end regularity

/-! ## The tangent of the family is the Lie derivative -/

/-! ## Diffeomorphism gauge -/

/-! ## Electromagnetic-potential gauge -/

section potential

variable {U : Set (Pt 4)} (hU : IsOpen U) {χ : Pt 4 → ℝ} (hχ : ContDiffOn ℝ ∞ χ U)
  {g gi : Metric 4} {F : TwoForm 4} {h : Metric 4} {f : TwoForm 4} {x : Pt 4} (hx : x ∈ U)
include hU hχ hx

end potential

/-! ### `L(0, d(dχ)) = 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).