Coordinate relation between two rows: map, inverse, smoothness, Jacobian, pull-back

Definition

Atlas_Core_Relation

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

coordinate-geometrycoordinate-relationcoordinate-transformationexact-vacuum-atlasgeneral-relativity

For coordinate metrics $g_1,g_2$ on $\mathbb R^4$ , sets $U,V\subseteq\mathbb R^4$ , maps $\Phi,\Psi:\mathbb R^4\to\mathbb R^4$ and a matrix-valued function $J$ , the proposition $\mathrm{CoordRelation}(g_1,g_2,U,V,\Phi,\Psi,J)$ is the conjunction of: $\Psi(\Phi(x))=x$ for $x\in U$ ; $\Phi(\Psi(y))=y$ for $y\in V$ ; $\Phi$ maps $U$ bijectively onto $V$ ; $\Phi$ is $C^\infty$ on $U$ ; $\Psi$ is $C^\infty$ on $V$ ; for all $x\in U$ and indices $k,i$ the slice $u\mapsto\Phi(x[x_i:=u])_k$ has derivative $J(x)_{ki}$ at $u=x_i$ ; and

J(x)^{\mathsf T}\,g_2(\Phi(x))\,J(x)=g_1(x)\quad(x\in U).

Row $k$ of $J$ is the output component, column $i$ the input coordinate.

The acceptance criterion for the relations R1–R4: a change of coordinates is certified by an explicit map with explicit inverse and Jacobian, never by an existence statement; Ricci-flatness of the rows is not part of it.

Formalization Note Definition bundle generated by skeleton subtraction from the source module Atlas.Core.Relation; declarations: ExactVacuumAtlas.CoordRelation. No theorem is proved inside the bundle; it imports only Mathlib and other Definitions.Def_* bundles.

Definition code

-- Generated by scripts/release01/gen_platform_tree.py (ATLAS-RELEASE-01) by skeleton subtraction from Atlas/Core/Relation.lean
-- definition bundle: kept ExactVacuumAtlas.CoordRelation
import Mathlib
import Definitions.Def_Atlas_Core_Basic
/-!
# Coordinate relation between two catalogue rows

`CoordRelation g₁ g₂ U V Φ Ψ J` packages exactly the obligations that `mission/RELEASE01_SPEC.md` §1
requires of a coordinate relation between two rows with metrics `g₁` (on the overlap `U`) and `g₂`
(on the image `V`):

* an explicit map `Φ` together with its inverse `Ψ` (`left_inv`, `right_inv`);
* `C^∞` regularity of `Φ` on `U` and of `Ψ` on `V`;
* `Φ` maps `U` bijectively onto `V` (`bijOn`);
* an explicit Jacobian `J` whose entries are proved to be genuine partial derivatives of the
  components of `Φ` (`jacobian`: `HasDerivAt` of every coordinate slice, never a junk `deriv` value);
* the pull-back identity `J(x)ᵀ · g₂(Φ x) · J(x) = g₁(x)` on `U` (`pullback`).

Like `VacuumCertificate` this is a `Prop`-valued bundle of obligations (B3 class B); each field is
discharged by a separate theorem. Ricci-flatness of the two rows is *not* part of it. Everything is
coordinate-level on `ℝ⁴`: no manifold, chart gluing or `φ ∼ φ + 2π` identification is modelled.
-/

open scoped ContDiff

namespace ExactVacuumAtlas

/-- Coordinate relation between the row `(g₁, U)` and the row `(g₂, V)` through the map `Φ : U → V`
with inverse `Ψ`, Jacobian `J` (row `k` = output component, column `i` = input coordinate). -/
structure CoordRelation (g₁ g₂ : Metric 4) (U V : Set (Pt 4)) (Φ Ψ : Pt 4 → Pt 4)
    (J : Pt 4 → Matrix (Fin 4) (Fin 4) ℝ) : Prop where
  left_inv : ∀ x ∈ U, Ψ (Φ x) = x
  right_inv : ∀ y ∈ V, Φ (Ψ y) = y
  bijOn : Set.BijOn Φ U V
  smooth : ContDiffOn ℝ ∞ Φ U
  smooth_inv : ContDiffOn ℝ ∞ Ψ V
  jacobian : ∀ x ∈ U, ∀ k i : Fin 4,
    HasDerivAt (fun u : ℝ => Φ (Function.update x i u) k) (J x k i) (x i)
  pullback : ∀ x ∈ U, (J x).transpose * metricMatrix g₂ (Φ x) * J x = metricMatrix g₁ x

namespace CoordRelation

variable {g₁ g₂ : Metric 4} {U V : Set (Pt 4)} {Φ Ψ : Pt 4 → Pt 4}
  {J : Pt 4 → Matrix (Fin 4) (Fin 4) ℝ}

end CoordRelation

end ExactVacuumAtlas

Source

coordinate Christoffel symbols and Ricci tensor: Müller–Grave catalogue.tex lines 277–281 (eq. ChristoffelSymbols), 287–290 (eq. RiemannTensor), 305–307 (R_{μν}=R^ρ_{μρν}), verified by the independent review 2026-10-13; R. M. Wald, General Relativity (1984) eqs. (3.1.30), (3.4.4)–(3.4.5) author-cited (not reviewer-verified); same formulas as platform definition KerrBL_CoordGeometry (id bbec007a-159a-4623-916d-f1cafab3e353); Lean source: repository ExactVacuumAtlas (private repository, not publicly accessible; GitHub remote pending (no GitHub identity on the build server)), commit 35f26e6a22f5d72380094fa94edc72dea667df53, Atlas/Core/Relation.lean (source module Atlas.Core.Relation, file sha256 50610a7c5f69638625b007bf090d4b7b21afd215bc79961e1376f68cf8813fb1; uploaded bundle = platform_mirror/Definitions/Def_Atlas_Core_Relation.lean, sha256 65c4b1606464395b1a671b2f61c39a0a352aae5ec23dffd2d2ca147faf78116e)

Human review

Endorsed by Shuze Chen · Oct 14, 2026
Confirmed by the moderator at approval.
Endorsed by He Wang · Oct 14, 2026
Confirmed by the mission captain (proposal self-audit).

View graph