VI-02 equal-spin ansatz

-- Generated by scripts/release06/gen_platform_tree.py (RELEASE06; copy of release05, header only) by skeleton subtraction from Atlas/EinsteinMaxwell/ES5/Defs.lean
-- definition bundle: kept ExactVacuumAtlas.EinsteinMaxwell.ES5.esDomain, ExactVacuumAtlas.EinsteinMaxwell.ES5.esFaraday, ExactVacuumAtlas.EinsteinMaxwell.ES5.esFrame, ExactVacuumAtlas.EinsteinMaxwell.ES5.esFrameSwap, ExactVacuumAtlas.EinsteinMaxwell.ES5.esInverse, ExactVacuumAtlas.EinsteinMaxwell.ES5.esMetric, ExactVacuumAtlas.EinsteinMaxwell.ES5.esPotential, ExactVacuumAtlas.EinsteinMaxwell.ES5.liftRU
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
/-! # Equal-spin D = 5 ansatz: notation layer and generic identities (ATLAS-VI-02/02)

B3 class-B layer (`mission/PHYSICS_BOUNDARY.md` §VI-02). Coordinates `x = (t, r, u, φ, ψ) =
(x 0, …, x 4)`, total dimension 5, on `esDomain R = {x | x 1 ∈ R ∧ 0 < x 2 ∧ x 2 < 1}` for a set
of radii `R`. With `σ = u dφ + (1-u) dψ`, `χ = dφ - dψ`, `h = du²/(4u(1-u)) + u(1-u) χ²`:

* `esMetric B D A H W = -B dt² + D dr² + A h + H (σ - W dt)²` (components written out);
* `esInverse` = `Σ_A η_A⁻¹ E_A ⊗ E_A`, frame `E_A` dual to `(dt, dr, du, σ - W dt, χ)`,
  `η = (-B, D, A/(4u(1-u)), H, A u(1-u))`;
* `esPotential Φ Ψ = Φ dt + Ψ σ`, and `esFaraday Φ Ψ = extD (esPotential Φ Ψ)` (`F = d𝒜`).

Nothing here is a manifold statement; the geometric objects are the registered class-A
`christoffel`/`ricciOf` and the D-generic Einstein–Maxwell layer, unchanged. Proved here, for
arbitrary radial functions: symmetry, `g⁻¹ g = 1` where `B, D, A, H ≠ 0`, Lorentz signature
`(-,+,+,+,+)` where `A > 0`, `H > 0`, `B D > 0`, and `C^∞` transfer from the radial functions. -/

set_option maxHeartbeats 8000000

open scoped ContDiff
open ExactVacuumAtlas ExactVacuumAtlas.EinsteinMaxwell

namespace ExactVacuumAtlas.EinsteinMaxwell.ES5

/-- The field `x ↦ F (x 1) (x 2)` on `ℝ⁵` (depends on `r` and `u` only). -/
def liftRU (F : ℝ → ℝ → ℝ) : Pt 5 → ℝ := fun x => F (x 1) (x 2)

/-- Coordinate domain over a set of radii `R`: `x 1 ∈ R`, `0 < u < 1`. -/
def esDomain (R : Set ℝ) : Set (Pt 5) := {x | x 1 ∈ R ∧ 0 < x 2 ∧ x 2 < 1}

/-- Equal-spin metric `-B dt² + D dr² + A h + H (σ - W dt)²`, components `g_ij`. -/
noncomputable def esMetric (B D A H W : ℝ → ℝ) : Metric 5
  | 0, 0 => fun x => -B (x 1) + H (x 1) * W (x 1) ^ 2
  | 0, 3 => fun x => -(H (x 1) * W (x 1) * x 2)
  | 3, 0 => fun x => -(H (x 1) * W (x 1) * x 2)
  | 0, 4 => fun x => -(H (x 1) * W (x 1) * (1 - x 2))
  | 4, 0 => fun x => -(H (x 1) * W (x 1) * (1 - x 2))
  | 1, 1 => fun x => D (x 1)
  | 2, 2 => fun x => A (x 1) / (4 * x 2 * (1 - x 2))
  | 3, 3 => fun x => A (x 1) * x 2 * (1 - x 2) + H (x 1) * x 2 ^ 2
  | 3, 4 => fun x => (H (x 1) - A (x 1)) * x 2 * (1 - x 2)
  | 4, 3 => fun x => (H (x 1) - A (x 1)) * x 2 * (1 - x 2)
  | 4, 4 => fun x => A (x 1) * x 2 * (1 - x 2) + H (x 1) * (1 - x 2) ^ 2
  | _, _ => fun _ => 0

/-- Frame-form inverse `Σ_A η_A⁻¹ E_A ⊗ E_A`, components `g^ij`. -/
noncomputable def esInverse (B D A H W : ℝ → ℝ) : Metric 5
  | 0, 0 => fun x => -1 / B (x 1)
  | 0, 3 => fun x => -W (x 1) / B (x 1)
  | 3, 0 => fun x => -W (x 1) / B (x 1)
  | 0, 4 => fun x => -W (x 1) / B (x 1)
  | 4, 0 => fun x => -W (x 1) / B (x 1)
  | 1, 1 => fun x => 1 / D (x 1)
  | 2, 2 => fun x => 4 * x 2 * (1 - x 2) / A (x 1)
  | 3, 3 => fun x => -W (x 1) ^ 2 / B (x 1) + 1 / H (x 1) + (1 - x 2) / (A (x 1) * x 2)
  | 3, 4 => fun x => -W (x 1) ^ 2 / B (x 1) + 1 / H (x 1) - 1 / A (x 1)
  | 4, 3 => fun x => -W (x 1) ^ 2 / B (x 1) + 1 / H (x 1) - 1 / A (x 1)
  | 4, 4 => fun x => -W (x 1) ^ 2 / B (x 1) + 1 / H (x 1) + x 2 / (A (x 1) * (1 - x 2))
  | _, _ => fun _ => 0

/-- Potential `𝒜 = Φ dt + Ψ σ`, `σ = u dφ + (1-u) dψ` (gauge `𝒜_r = 0`). -/
noncomputable def esPotential (Φ Ψ : ℝ → ℝ) : CoVec 5
  | 0 => fun x => Φ (x 1)
  | 3 => fun x => Ψ (x 1) * x 2
  | 4 => fun x => Ψ (x 1) * (1 - x 2)
  | _ => fun _ => 0

/-- Field strength `F = d𝒜` (by definition, through the registered `extD`). -/
noncomputable def esFaraday (Φ Ψ : ℝ → ℝ) : TwoForm 5 := extD (esPotential Φ Ψ)

variable (B D A H W : ℝ → ℝ)

/-- Columns: the frame `E_0 = ∂t + W(∂φ + ∂ψ)`, `E_1 = ∂r`, `E_2 = ∂u`, `E_3 = ∂φ + ∂ψ`,
`E_4 = (1-u)∂φ - u∂ψ`. -/
noncomputable def esFrame (x : Pt 5) : Matrix (Fin 5) (Fin 5) ℝ :=
  !![1, 0, 0, 0, 0;
     0, 1, 0, 0, 0;
     0, 0, 1, 0, 0;
     W (x 1), 0, 0, 1, 1 - x 2;
     W (x 1), 0, 0, 1, -x 2]

/-- The same frame with `E_0` and `E_1` exchanged (used where `B < 0`, `D < 0`). -/
noncomputable def esFrameSwap (x : Pt 5) : Matrix (Fin 5) (Fin 5) ℝ :=
  !![0, 1, 0, 0, 0;
     1, 0, 0, 0, 0;
     0, 0, 1, 0, 0;
     0, W (x 1), 0, 1, 1 - x 2;
     0, W (x 1), 0, 1, -x 2]

/-! ## Smoothness transfer from the radial functions -/

end ExactVacuumAtlas.EinsteinMaxwell.ES5

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