Atlas Transport Connection

-- Generated by scripts/release01/gen_platform_tree.py (ATLAS-RELEASE-01) by skeleton subtraction from Atlas/Transport/Connection.lean
-- definition bundle: kept ExactVacuumAtlas.CoordChange, ExactVacuumAtlas.MetricData, ExactVacuumAtlas.chr1, ExactVacuumAtlas.connMat, ExactVacuumAtlas.curv, ExactVacuumAtlas.pullC
import Mathlib
import Definitions.Def_Atlas_Core_Basic
import Definitions.Def_Atlas_Core_Certificate
import Definitions.Def_Atlas_Transport_MatrixCalc
/-!
# Transport layer II.c: transformation of the Christoffel symbols (ATLAS-II)

Setting (dimension `n`, everything coordinate-level on open subsets of `ℝⁿ`):

* `CoordChange U V Φ J K`: `Φ` is `C^∞` on the open set `U`, maps `U` into the open set `V`, `J y` is
  its genuine Jacobian (`HasDerivAt` of every coordinate slice, row = output component, column =
  input coordinate) and `K y` is a right inverse of `J y` on `U` (hence two-sided, and `C^∞`).
* `MetricData h hi V`: symmetric metric with genuine inverse and `C^∞` components on the open set
  `V` — **no curvature condition**.
* pull-back hypotheses `G(y) = J(y)ᵀ H(Φ y) J(y)` and `GI(y) = K(y) HI(Φ y) K(y)ᵀ` on `U`.

Main result `christoffel_transform`: with `(connMat Γ c) a b := Γ a c b` (first lower index = direction),

  `connMat (christoffel g gi) i y = Σ_e J y e i • (K y * connMat (christoffel h hi) e (Φ y) * J y) + K y * pdM i J y`,

i.e. componentwise `Γ[g]ᵏ_{ij}(y) = Σ_c Kᵏ_c (∂_i Jᶜ_j + Σ_{a b} Γ[h]ᶜ_{ab}(Φ y) Jᵃ_i Jᵇ_j)` — **with the
second-derivative term** `∂_i J`; the Christoffel symbols are not a `(1,2)` tensor. The proof uses only
the registered definitions `pd`, `christoffel` (through the first-kind symbols `chr1`, bridge
`christoffel_eq_sum_chr1`) and the calculus rules of `Atlas/Transport/{Calculus,MatrixCalc}.lean`.

Auxiliary definitions (B3 class B, transparent): `chr1`, `connMat`, `curv`, `CoordChange`, `MetricData`.
-/

open scoped ContDiff
open Matrix

namespace ExactVacuumAtlas

variable {n : ℕ}

/-! ### Definitions -/

/-- Christoffel symbols of the first kind `Γ_{l ij} = ½(∂_j g_{li} + ∂_i g_{lj} − ∂_l g_{ij})`. -/
noncomputable def chr1 (g : Metric n) (l i j : Fin n) (y : Pt n) : ℝ :=
  (pd j (g l i) y + pd i (g l j) y - pd l (g i j) y) / 2

/-- A connection as a family of matrices: `(connMat Γ c y) a b = Γ a c b y`. -/
def connMat (Γ : Fin n → Fin n → Fin n → Pt n → ℝ) (c : Fin n) (y : Pt n) :
    Matrix (Fin n) (Fin n) ℝ :=
  Matrix.of fun a b => Γ a c b y

/-- Curvature of a matrix-valued connection: `F_{cd} = ∂_c Γ_d − ∂_d Γ_c + Γ_c Γ_d − Γ_d Γ_c`. -/
noncomputable def curv (Γ : Fin n → Pt n → Matrix (Fin n) (Fin n) ℝ) (c d : Fin n) (y : Pt n) :
    Matrix (Fin n) (Fin n) ℝ :=
  pdM c (Γ d) y - pdM d (Γ c) y + Γ c y * Γ d y - Γ d y * Γ c y

/-- Coordinate change data: `Φ : U → V` smooth with genuine Jacobian `J` and right inverse `K`. -/
structure CoordChange (U V : Set (Pt n)) (Φ : Pt n → Pt n)
    (J K : Pt n → Matrix (Fin n) (Fin n) ℝ) : Prop where
  isOpen : IsOpen U
  isOpen_target : IsOpen V
  smooth : ContDiffOn ℝ ∞ Φ U
  mapsTo : Set.MapsTo Φ U V
  jacobian : ∀ y ∈ U, ∀ k i : Fin n,
    HasDerivAt (fun u : ℝ => Φ (Function.update y i u) k) (J y k i) (y i)
  mul_inv : ∀ y ∈ U, J y * K y = 1

/-- Regular metric data on an open set: symmetric, genuine inverse, `C^∞`; **no curvature condition**. -/
structure MetricData (g gi : Metric n) (U : Set (Pt n)) : Prop where
  isOpen : IsOpen U
  symm : ∀ x ∈ U, ∀ i j, g i j x = g j i x
  inv : ∀ x ∈ U, metricMatrix gi x * metricMatrix g x = 1
  smooth : ∀ i j, ContDiffOn ℝ ∞ (g i j) U
  smooth_inv : ∀ i j, ContDiffOn ℝ ∞ (gi i j) U

/-! ### Basic consequences -/

namespace CoordChange

variable {U V : Set (Pt n)} {Φ : Pt n → Pt n} {J K : Pt n → Matrix (Fin n) (Fin n) ℝ}

end CoordChange

namespace MetricData

variable {g gi : Metric n} {U : Set (Pt n)}

end MetricData

/-! ### Ricci as a contraction of the matrix curvature -/

/-! ### Algebraic cores of the Christoffel transformation (no calculus) -/

/-! ### Calculus assembly: the Christoffel transformation -/

section transform

variable {U V : Set (Pt n)} {Φ : Pt n → Pt n} {J K : Pt n → Matrix (Fin n) (Fin n) ℝ}
  {g gi h hi : Metric n}

/-- Proof-internal matrix `Cᵢ a j = Σ_{b e} J_{bi} J_{ej} Γ[h]_{a b e}(Φ y)` (pulled-back first-kind symbols). -/
noncomputable def pullC (h : Metric n) (Φ : Pt n → Pt n) (J : Pt n → Matrix (Fin n) (Fin n) ℝ)
    (y : Pt n) (i : Fin n) : Matrix (Fin n) (Fin n) ℝ :=
  Matrix.of fun a j => ∑ b, ∑ e, J y b i * J y e j * chr1 h a b e (Φ y)

end transform

end ExactVacuumAtlas

• Endorsed by Shuze Chen · Oct 18, 2026

  Confirmed by the moderator at approval.

• Endorsed by He Wang · Oct 18, 2026

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