Standard Schwarzschild: diagonal frames for the exterior and interior components

Definition

Atlas_Schwarzschild_StdParts

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

coordinate-geometryexact-vacuum-atlasgeneral-relativitylorentzian-signatureschwarzschild-metric

Two diagonal-type frame matrices depending on a real parameter $s$ (in use, $s=\sqrt{|1-2M/r|}$ ): the exterior frame $\mathrm{frameX}=\mathrm{diag}(1/s,\ s,\ 1/r,\ 1/(r\sin\theta))$ (frameXE/frameX) and the interior frame $\mathrm{frameI}$ with the same entries but the first two columns swapped (frameIE/frameI), used where $\partial_r$ is timelike ( $0<r<2M$ ).

Frame data for the signature obligation of row 3 on both components of the standard domain (generated file, kernel-checked).

Formalization Note Definition bundle generated by skeleton subtraction from the source module Atlas.Schwarzschild.StdParts; declarations: ExactVacuumAtlas.Schwarzschild.Std.frameI, ExactVacuumAtlas.Schwarzschild.Std.frameIE, ExactVacuumAtlas.Schwarzschild.Std.frameX, ExactVacuumAtlas.Schwarzschild.Std.frameXE. 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/StdParts.lean
-- definition bundle: kept ExactVacuumAtlas.Schwarzschild.Std.frameI, ExactVacuumAtlas.Schwarzschild.Std.frameIE, ExactVacuumAtlas.Schwarzschild.Std.frameX, ExactVacuumAtlas.Schwarzschild.Std.frameXE
import Mathlib
import Definitions.Def_Atlas_Core_Basic
import Definitions.Def_Atlas_Schwarzschild_Defs
import Definitions.Def_Atlas_Schwarzschild_Domain
import Definitions.Def_KerrBL_CoordGeometry
import Definitions.Def_KerrBL_Kerr_Metric
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_std.py`. Do not edit by hand. -/

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

noncomputable def frameXE (s : ℝ) (x : Pt 4) : Fin 4 → Fin 4 → ℝ
  | 0, 0 => 1 / s
  | 1, 1 => s
  | 2, 2 => 1 / (x 1)
  | 3, 3 => 1 / ((x 1) * sin (x 2))
  | _, _ => 0
noncomputable def frameX (s : ℝ) (x : Pt 4) : Matrix (Fin 4) (Fin 4) ℝ := Matrix.of (frameXE s x)
noncomputable def frameIE (s : ℝ) (x : Pt 4) : Fin 4 → Fin 4 → ℝ
  | 1, 0 => s
  | 0, 1 => 1 / s
  | 2, 2 => 1 / (x 1)
  | 3, 3 => 1 / ((x 1) * sin (x 2))
  | _, _ => 0
noncomputable def frameI (s : ℝ) (x : Pt 4) : Matrix (Fin 4) (Fin 4) ℝ := Matrix.of (frameIE s x)

end ExactVacuumAtlas.Schwarzschild.Std

Source

Müller–Grave catalogue eq. schwarzschildSpherical (r_s = 2M, G = c = 1); 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/StdParts.lean (source module Atlas.Schwarzschild.StdParts, file sha256 3692d4bbcb9f2aa86cca6a8193a1f3ea469875059683caa2935a8099021a6bc4; uploaded bundle = platform_mirror/Definitions/Def_Atlas_Schwarzschild_StdParts.lean, sha256 7dfcb7e42cae9d77c0d3bdd16ea1d7b5605b117ab46ac11b38d73a29d00a3935)

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