Fields depending only on $(r,\theta)$ in four dimensions

Definition

Atlas_Core_Lift

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

coordinate-geometryexact-vacuum-atlasgeneral-relativitynotation

For a function $F:\mathbb R\times\mathbb R\to\mathbb R$ , $\mathrm{liftRT}(F)$ is the field on $\mathbb R^4$ given by $x\mapsto F(x_1,x_2)$ , i.e. $F(r,\theta)$ in coordinates $(x_0,r,\theta,x_3)$ .

Notation wrapper for the stationary axisymmetric rows (every row except Cartesian), whose components depend only on $r$ and $\theta$ ; partial derivatives of lifted fields reduce to one-variable derivatives of $F$ .

Formalization Note Definition bundle generated by skeleton subtraction from the source module Atlas.Core.Lift; declarations: ExactVacuumAtlas.liftRT. 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/Lift.lean
-- definition bundle: kept ExactVacuumAtlas.liftRT
import Mathlib
import Definitions.Def_Atlas_Core_Basic
/-! # Fields depending only on `(x₁, x₂) = (r, θ)` in four dimensions

Stationary axisymmetric metrics (Schwarzschild, Kerr, Minkowski spherical, in every coordinate
system of release 0.1 except Cartesian) have components that depend only on `r = x₁` and
`θ = x₂`. `liftRT F` is the field `x ↦ F (x₁) (x₂)`; its partial derivatives reduce to ordinary
one-variable derivatives of `F`.
-/

namespace ExactVacuumAtlas

/-- The field `x ↦ F (x 1) (x 2)` on `ℝ⁴`. -/
def liftRT (F : ℝ → ℝ → ℝ) : Pt 4 → ℝ := fun x => F (x 1) (x 2)

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/Lift.lean (source module Atlas.Core.Lift, file sha256 d1f8adc96523c6e39e8aadf01a51de77d82c7f6d88441c517181debea157727f; uploaded bundle = platform_mirror/Definitions/Def_Atlas_Core_Lift.lean, sha256 b8d25acc56f7258ec5c665333f50d0e467f8263107aa07578ff8f4f9aacbbb44)

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

Fields depending only on (r,θ)(r,\theta)(r,θ) in four dimensions

Fields depending only on $(r,\theta)$ in four dimensions