Eddington–Finkelstein Schwarzschild: explicit Lorentz frame valid across $r=2M$

Definition

Atlas_Schwarzschild_EFCertParts

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

coordinate-geometryeddington-finkelsteinexact-vacuum-atlasgeneral-relativitylorentzian-signatureschwarzschild-metric

The frame matrix of the Eddington–Finkelstein metric $g^{\rm EF}_{M,\varepsilon}$ , with $f=1-2M/r$ :

\mathrm{frame}(x)=\begin{pmatrix}1&1&0&0\\\varepsilon\tfrac{f-1}{2}&\varepsilon\tfrac{f+1}{2}&0&0\\0&0&1/r&0\\0&0&0&1/(r\sin\theta)\end{pmatrix}

(frameE as a function of indices, frame as a matrix), which satisfies $\mathrm{frame}^{\mathsf T}g^{\rm EF}\,\mathrm{frame}=\mathrm{diag}(-1,1,1,1)$ on $U^{\rm EF}$ when $\varepsilon^2=1$ ; it contains no square root of $f$ , hence is valid at $r=2M$ .

Frame data for the signature obligation of rows 4–5 (generated file, kernel-checked).

Formalization Note Definition bundle generated by skeleton subtraction from the source module Atlas.Schwarzschild.EFCertParts; declarations: ExactVacuumAtlas.Schwarzschild.EF.frame, ExactVacuumAtlas.Schwarzschild.EF.frameE. 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/Schwarzschild/EFCertParts.lean
-- definition bundle: kept ExactVacuumAtlas.Schwarzschild.EF.frame, ExactVacuumAtlas.Schwarzschild.EF.frameE
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
set_option maxHeartbeats 4000000
set_option linter.unusedVariables false
set_option linter.unusedSimpArgs false
set_option linter.unusedTactic false
set_option linter.unreachableTactic false

/-! Generated by `scripts/gen_ef_cert.py`. Do not edit by hand. -/

open Real
open scoped ContDiff
open ExactVacuumAtlas ExactVacuumAtlas.Schwarzschild
namespace ExactVacuumAtlas.Schwarzschild.EF
variable (M ε : ℝ)

/-- Explicit orthonormal frame for `gEF` (valid on all of `domEF`, including `r = 2M`). -/
noncomputable def frameE (x : Pt 4) : Fin 4 → Fin 4 → ℝ
  | 0, 0 => 1
  | 0, 1 => 1
  | 1, 0 => ε * ((1 - 2*M/(x 1)) - 1) / 2
  | 1, 1 => ε * ((1 - 2*M/(x 1)) + 1) / 2
  | 2, 2 => 1 / (x 1)
  | 3, 3 => 1 / ((x 1) * sin (x 2))
  | _, _ => 0

noncomputable def frame (x : Pt 4) : Matrix (Fin 4) (Fin 4) ℝ := Matrix.of (frameE M ε x)

end ExactVacuumAtlas.Schwarzschild.EF

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|; Sylvester's law of inertia (standard linear algebra); Mathlib LinearAlgebra/QuadraticForm/Signature.lean (pinned 0df444a3) for sigPos/sigNeg; Lean source: repository ExactVacuumAtlas (private repository, not publicly accessible; GitHub remote pending (no GitHub identity on the build server)), commit 35f26e6a22f5d72380094fa94edc72dea667df53, Atlas/Schwarzschild/EFCertParts.lean (source module Atlas.Schwarzschild.EFCertParts, file sha256 8a44f231b1b9bd5a31d5108cac0d4264b2f52f6b68599414a2a595716064f871; uploaded bundle = platform_mirror/Definitions/Def_Atlas_Schwarzschild_EFCertParts.lean, sha256 2e93209a80b8bb2c8d5f937101929afb41960b973700c5137342239c662aa297)

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

Eddington–Finkelstein Schwarzschild: explicit Lorentz frame valid across r=2Mr=2Mr=2M

Eddington–Finkelstein Schwarzschild: explicit Lorentz frame valid across $r=2M$