Prove2Me

VI-01 explicit EF5 frame

Definition
Atlas_EinsteinMaxwell_EF5_Frame

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

einstein-maxwellexact-spacetime-atlas-viexact-vacuum-atlasfive-dimensional-gravitygeneral-relativity

VI-01 explicit EF5 frame

frameEF5 (explicit frame) and diagEF5 = (−1, 1, r²/(4u(1−u)), r²u, r²(1−u)) with Eᵀ g E = diag (proved in frameEF5_diag_spec).

中文摘要 VI-01 EF5 显式标架。

Registry: PHYSICS_BOUNDARY §N (VI-01) N5.

Definition code
-- Generated by scripts/release06/gen_platform_tree.py (RELEASE06; copy of release05, header only) by skeleton subtraction from Atlas/EinsteinMaxwell/EF5/Frame.lean
-- definition bundle: kept ExactVacuumAtlas.EinsteinMaxwell.EF5.diagEF5, ExactVacuumAtlas.EinsteinMaxwell.EF5.frameEF5
import Mathlib
import Definitions.Def_Atlas_Core_Basic
import Definitions.Def_Atlas_Core_Certificate
import Definitions.Def_Atlas_EinsteinMaxwell_Basic
import Definitions.Def_Atlas_EinsteinMaxwell_D_Basic
import Definitions.Def_Atlas_EinsteinMaxwell_EF5_Defs
/-! # Lorentz signature for the 5D EF static family (ATLAS-VI-01, class B)

We prove `IsLorentzian (metricMatrix (gEF5 mu beta) x)` on `U5` by exhibiting a
diagonalising frame `E` with `Eᵀ G E = diagonal d` where `d 0 < 0` and `d i > 0`
for `i ≠ 0`, then applying `isLorentzian_of_diag` (Atlas.Core.Lorentz).

The frame (columns = frame vectors, `f = 1 - μ/r² + β/r⁴`):

  e₀ = ∂_v + ((f-1)/2) ∂_r   (timelike)
  e₁ = ∂_v + ((f+1)/2) ∂_r   (spacelike)
  e₂ = ∂_u,  e₃ = ∂_φ,  e₄ = ∂_ψ

This brings `G` to `diag(-1, 1, r²/(4u(1-u)), r²u, r²(1-u))`. No square roots
appear in the identity, so every entry closes by `ring` (or `field_simp; ring`
for the rational entries). The signature is `(-,+,+,+,+)` = `sigPos = 4`,
`sigNeg = 1` on `U5` including `f = 0`. -/

set_option maxHeartbeats 4000000

open ExactVacuumAtlas ExactVacuumAtlas.EinsteinMaxwell ExactVacuumAtlas.EinsteinMaxwell.EF5

namespace ExactVacuumAtlas.EinsteinMaxwell.EF5

/-- Diagonalising frame for the 5D EF metric (no square roots in the identity).

    Columns are the frame vectors in the coordinate basis `(v, r, u, φ, ψ)`.
    Defined by pattern matching (same style as `gEF5`); `metricMatrix_frameEF5`
    exposes the explicit matrix literal. -/
noncomputable def frameEF5 (mu beta : ℝ) : Metric 5
  | 0, 0 => fun _ => 1
  | 0, 1 => fun _ => 1
  | 1, 0 => fun x => (-mu / x 1 ^ 2 + beta / x 1 ^ 4) / 2
  | 1, 1 => fun x => 1 + (-mu / x 1 ^ 2 + beta / x 1 ^ 4) / 2
  | 2, 2 => fun _ => 1
  | 3, 3 => fun _ => 1
  | 4, 4 => fun _ => 1
  | _, _ => fun _ => 0

/-- The diagonal `d` such that `Eᵀ G E = diagonal d` on `U5`. -/
noncomputable def diagEF5 (mu beta : ℝ) (x : Pt 5) : Fin 5 → ℝ
  | 0 => -1
  | 1 => 1
  | 2 => x 1 ^ 2 / (4 * x 2 * (1 - x 2))
  | 3 => x 1 ^ 2 * x 2
  | 4 => x 1 ^ 2 * (1 - x 2)
  | _ => 0

end ExactVacuumAtlas.EinsteinMaxwell.EF5
Source
He Wang, Exact Spacetime Atlas VI: Five-Dimensional Einstein–Maxwell Certificates and Equal-Spin Radial Reduction. Local source, no public repository; commit 4a4048a; Atlas/EinsteinMaxwell/EF5/Frame.lean; SHA-256 ebaa68d722fd05664bf7ac50f56351f249f3836d963a5684a125adab0dff5509. Registered definitions: mission/PHYSICS_BOUNDARY.md (§N–§O); literature: R. C. Myers, M. J. Perry, Ann. Phys. 172 (1986) 304; F. R. Tangherlini, Nuovo Cimento 27 (1963) 636.
Human review

  • Endorsed by Shuze Chen · Oct 29, 2026

    Confirmed by the moderator at approval.

  • Endorsed by He Wang · Oct 29, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph