R1/R2 data: Jacobian of the standard-to-Eddington–Finkelstein map

Definition

Atlas_Schwarzschild_EFRelation

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

coordinate-geometrycoordinate-transformationeddington-finkelsteinexact-vacuum-atlasgeneral-relativityschwarzschild-metric

The Jacobian matrix of $\Phi_{M,\varepsilon}(t,r,\theta,\varphi)=(t+\varepsilon(r+2M\log\lvert r-2M\rvert),r,\theta,\varphi)$ :

J(x)=\begin{pmatrix}1&\varepsilon\big(1+\frac{2M}{r-2M}\big)&0&0\\0&1&0&0\\0&0&1&0\\0&0&0&1\end{pmatrix},

row $k$ = output component, column $i$ = input coordinate; $\det J=1$ .

Jacobian data of relations R1 ( $\varepsilon=1$ ) and R2 ( $\varepsilon=-1$ ).

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

Formalization Note (logarithm). $\log\lvert r-2M\rvert$ stands for Mathlib's Real.log (r - 2M), which equals $\log\lvert r-2M\rvert$ for every $r\neq2M$ (Real.log_abs); the Lean expression is unchanged and the domain is not restricted to $r>2M$ .

Definition code

-- Generated by scripts/release01/gen_platform_tree.py (ATLAS-RELEASE-01) by skeleton subtraction from Atlas/Schwarzschild/EFRelation.lean
-- definition bundle: kept ExactVacuumAtlas.Schwarzschild.EFRelation.jac
import Mathlib
import Definitions.Def_Atlas_Core_Basic
import Definitions.Def_Atlas_Core_Lift
import Definitions.Def_Atlas_Schwarzschild_Defs
import Definitions.Def_Atlas_Schwarzschild_Domain
import Definitions.Def_Atlas_Schwarzschild_EFCertParts
import Definitions.Def_Atlas_Schwarzschild_StdParts
import Definitions.Def_KerrBL_CoordGeometry
import Definitions.Def_KerrBL_Kerr_Metric
set_option maxHeartbeats 4000000

/-!
# Standard ↔ Eddington–Finkelstein: the actual coordinate map on the overlap

On the overlap `domStd M` (`r > 0`, `r ≠ 2M`, `0 < θ < π`; both the exterior and, for `M > 0`, the
interior component) we prove, for `ε = ±1`:

* `toEF M ε` and `fromEF M ε` are `C^∞` on `domStd M`, map `domStd M` into itself (⊆ `domEF`) and
  are mutually inverse (globally on the overlap, hence a diffeomorphism of `domStd M` onto itself);
* the Jacobian of `toEF` is the explicit matrix `jac`, its entries are the genuine partial
  derivatives (`HasDerivAt`, not junk values), and `det jac = 1`;
* pull-back identity: `gStd = jacᵀ · (gEF ∘ toEF) · jac` componentwise.

Statements on `r = 2M` are **not** obtained from this relation; they come from the direct EF
certificate on the larger domain `domEF` (`EF.cert`).
-/

open Real
open scoped ContDiff
open ExactVacuumAtlas ExactVacuumAtlas.Schwarzschild

namespace ExactVacuumAtlas.Schwarzschild.EFRelation

variable (M ε : ℝ)

/-- Jacobian `∂(toEF)ᵏ/∂xⁱ`; row `k`, column `i`. -/
noncomputable def jac (x : Pt 4) : Matrix (Fin 4) (Fin 4) ℝ :=
  !![1, ε * (1 + 2 * M / (x 1 - 2 * M)), 0, 0;
     0, 1, 0, 0;
     0, 0, 1, 0;
     0, 0, 0, 1]

end ExactVacuumAtlas.Schwarzschild.EFRelation

Source

Müller–Grave catalogue eq. eddFinkel: ds² = −(1−r_s/r) dv² + 2 dv dr + r² dΩ², v = t + r + r_s ln(r − r_s); outgoing form with u = t − r − r_s ln|r − r_s|; Lean source: repository ExactVacuumAtlas (private repository, not publicly accessible; GitHub remote pending (no GitHub identity on the build server)), commit 35f26e6a22f5d72380094fa94edc72dea667df53, Atlas/Schwarzschild/EFRelation.lean (source module Atlas.Schwarzschild.EFRelation, file sha256 c34cc5912defa1555f6c1fdc81e737294b0daaf9458bcb4fed544daf7d174e70; uploaded bundle = platform_mirror/Definitions/Def_Atlas_Schwarzschild_EFRelation.lean, sha256 394321c00a3d13ed48aee5de7dfe06d5e78086628cdef6ed12ec4d6e9f69994e)

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