VI-01 Ricci closed-form table

-- Generated by scripts/release06/gen_platform_tree.py (RELEASE06; copy of release05, header only) by skeleton subtraction from Atlas/EinsteinMaxwell/EF5/RicciOffDiag.lean
-- definition bundle: kept ExactVacuumAtlas.EinsteinMaxwell.EF5.ricciTableEF5
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
set_option maxHeartbeats 400000000
set_option linter.unusedVariables false
set_option linter.unusedSimpArgs false
set_option linter.unusedTactic false

/-! # EF5: off-diagonal Ricci components, Ricci scalar, 25-component coverage (ATLAS-VI-01)

Generated by `scratch/vi01_gen/gen_offdiag.py`. Every partial derivative that occurs in an
off-diagonal component `ricciOf … a b` is shown to vanish on `domU5` through the registered
Christoffel EqOn bridges of `Ricci.lean` (the bridged closed form does not depend on the
differentiated coordinate); the remaining quadratic Christoffel terms are rewritten pointwise
with the same bridges and closed by `ring`. No new definitions. -/

open scoped ContDiff
open ExactVacuumAtlas ExactVacuumAtlas.EinsteinMaxwell ExactVacuumAtlas.EinsteinMaxwell.D
open ExactVacuumAtlas.EinsteinMaxwell.EF5

namespace ExactVacuumAtlas.EinsteinMaxwell.EF5

variable (mu beta : ℝ)

/-! ## pd lemmas for the off-diagonal components -/

/-! ## Off-diagonal Ricci components -/

/-! ## Ricci scalar R = -2β/r⁶ -/

/-- Closed-form table of all 25 Ricci components on `domU5` (`r = x 1`, `u = x 2`). -/
noncomputable def ricciTableEF5 (x : Pt 5) : Fin 5 → Fin 5 → ℝ := fun a b =>
  match a, b with
  | 0, 0 => 4 * beta * (1 - mu / x 1 ^ 2 + beta / x 1 ^ 4) / x 1 ^ 6
  | 0, 1 => -4 * beta / x 1 ^ 6
  | 1, 0 => -4 * beta / x 1 ^ 6
  | 2, 2 => beta / (2 * x 1 ^ 4 * x 2 * (1 - x 2))
  | 3, 3 => 2 * beta * x 2 / x 1 ^ 4
  | 4, 4 => 2 * beta * (1 - x 2) / x 1 ^ 4
  | _, _ => 0

end ExactVacuumAtlas.EinsteinMaxwell.EF5

• 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).