Atlas Transport Curvature
DefinitionAtlas_Transport_Curvatureexact-vacuum-atlasgeneral-relativitylean4mathlib
pullConn J Γ Φ d z = Σ_f J z f d • Γ f (Φ z): the pulled-back connection forms A_d used inside the proof of the curvature tensoriality curv_transform. No other definition; the theorem is a separate node.
Definition code
-- Generated by scripts/release01/gen_platform_tree.py (ATLAS-RELEASE-01) by skeleton subtraction from Atlas/Transport/Curvature.lean
-- definition bundle: kept ExactVacuumAtlas.pullConn
import Mathlib
import Definitions.Def_Atlas_Core_Basic
import Definitions.Def_Atlas_Core_Certificate
import Definitions.Def_Atlas_Transport_Connection
import Definitions.Def_Atlas_Transport_MatrixCalc
/-!
# Transport layer II.d: the matrix curvature is a tensor (ATLAS-II)
For a family of matrix fields `Γ e` (any connection, not necessarily metric) on the open set `V`, and
`Γ' i y = Σ_e J y e i • (K y * Γ e (Φ y) * J y) + K y * ∂ᵢJ y` on `U` (the transformation law proved for
the Christoffel symbols in `Connection.lean`), the curvature
`curv Γ c d = ∂_c Γ_d − ∂_d Γ_c + Γ_c Γ_d − Γ_d Γ_c` transforms as
`curv Γ' c d y = Σ_{e f} (J y e c * J y f d) • (K y * curv Γ e f (Φ y) * J y)`.
The second-derivative term `K ∂J` and all derivatives of `K` cancel: the algebraic core `curv_core` is an
identity in the noncommutative ring of matrices using only `J K = 1`; the calculus part uses the product
rule, the chain rule, `∂K = −K ∂J K` and the symmetry of the second derivatives of `Φ` (`∂_c ∂_d J = ∂_d ∂_c J`
and `∂_c J_{·d} = ∂_d J_{·c}`).
-/
open scoped ContDiff
open Matrix
namespace ExactVacuumAtlas
variable {n : ℕ}
/-- The pulled-back connection forms `A_d z = Σ_f J z f d • Γ f (Φ z)` (proof-internal). -/
noncomputable def pullConn (J : Pt n → Matrix (Fin n) (Fin n) ℝ) (Γ : Fin n → Pt n → Matrix (Fin n) (Fin n) ℝ)
(Φ : Pt n → Pt n) (d : Fin n) (z : Pt n) : Matrix (Fin n) (Fin n) ℝ :=
∑ f, J z f d • Γ f (Φ z)
section
variable {U V : Set (Pt n)} {Φ : Pt n → Pt n} {J K : Pt n → Matrix (Fin n) (Fin n) ℝ}
end
end ExactVacuumAtlas
Source
He Wang, Exact Vacuum Atlas II, local source snapshot (public Git repository not yet available), commit 11fb317259353b71a41d6daed466c495cffd7db4; Atlas/Transport/Curvature.lean; SHA-256 858c500b5613da0b7365f52bf082c6d59235ecb04152a0bc11669cac412050f2. Mathematical background: See mission/PHYSICS_BOUNDARY.md §A-F for registered definitions and literature references (Wald, Müller-Grave arXiv:0904.4184, Visser arXiv:0706.0622, Martel-Poisson gr-qc/0001069).
Human review
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.