Vacuum certificate for a coordinate metric on an open domain

Definition

Atlas_Core_Certificate

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

coordinate-geometryexact-vacuum-atlasgeneral-relativityricci-flatnessvacuum-certificate

For coordinate metrics $g,\hat g$ on $\mathbb R^{n+1}$ and a set $U\subseteq\mathbb R^{n+1}$ , the proposition $\mathrm{VacuumCertificate}(g,\hat g,U)$ is the conjunction of eight obligations: (1) $U$ is open; (2) $U$ is nonempty; (3) $g_{ij}(x)=g_{ji}(x)$ for all $x\in U$ ; (4) $\hat g(x)\,g(x)=I$ for all $x\in U$ ; (5) every $g_{ij}$ is $C^\infty$ on $U$ ; (6) every $\hat g^{ij}$ is $C^\infty$ on $U$ ; (7) $g(x)$ is Lorentzian for all $x\in U$ ; (8) $R_{bd}(x)=0$ for all $x\in U$ and all $b,d$ , where $R$ is the coordinate Ricci tensor of $(g,\hat g)$ from bundle Atlas_Core_Basic. The data $g,\hat g,U$ are supplied independently of any proof, so a certificate is never vacuous by construction.

The acceptance criterion of every row of the atlas; each field is discharged by a separate theorem. Obligation (4) rules out a trivialising wrong inverse, (5)–(6) make every slice derivative in $R_{bd}$ a genuine derivative.

Formalization Note Definition bundle generated by skeleton subtraction from the source module Atlas.Core.Certificate; declarations: ExactVacuumAtlas.VacuumCertificate. 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/Certificate.lean
-- definition bundle: kept ExactVacuumAtlas.VacuumCertificate
import Mathlib
import Definitions.Def_Atlas_Core_Basic
/-! # Vacuum certificate for a coordinate metric on an open domain

`VacuumCertificate g ginv U` packages everything a catalogue row must establish:
open, nonempty domain; symmetric metric; `ginv` a genuine (left, hence two-sided) inverse;
`C^∞` components; Lorentzian signature through an explicit invertible frame; vanishing of all
components of the coordinate Ricci tensor. `g`, `ginv`, `U` are data supplied independently of
any proof, so the certificate is never vacuous by construction.
-/

open Filter Topology
open scoped ContDiff

namespace ExactVacuumAtlas

structure VacuumCertificate {n : ℕ} (g ginv : Metric (n + 1)) (U : Set (Pt (n + 1))) : Prop where
  isOpen : IsOpen U
  nonempty : U.Nonempty
  symm : ∀ x ∈ U, ∀ i j, g i j x = g j i x
  inv : ∀ x ∈ U, metricMatrix ginv x * metricMatrix g x = 1
  smooth : ∀ i j, ContDiffOn ℝ ∞ (g i j) U
  smooth_inv : ∀ i j, ContDiffOn ℝ ∞ (ginv i j) U
  lorentz : ∀ x ∈ U, IsLorentzian (metricMatrix g x)
  ricci_flat : ∀ x ∈ U, ∀ b d, ricciOf g ginv b d x = 0

namespace VacuumCertificate

variable {n : ℕ} {g ginv : Metric (n + 1)} {U : Set (Pt (n + 1))}

end VacuumCertificate

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/Certificate.lean (source module Atlas.Core.Certificate, file sha256 c714a637b0dab5004e0072ce4fd3c4e7033c9c1289d2e934626cb506d5eaefe3; uploaded bundle = platform_mirror/Definitions/Def_Atlas_Core_Certificate.lean, sha256 60db27e9c08b5a69aeb72325a7828deaff4b97d9e5cb7de02240f9fd47738db5)

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