VI-02 ReducedSystem and evaluation point

-- Generated by scripts/release06/gen_platform_tree.py (RELEASE06; copy of release05, header only) by skeleton subtraction from Atlas/EinsteinMaxwell/ES5/Generic/Cert.lean
-- definition bundle: kept ExactVacuumAtlas.EinsteinMaxwell.ES5.Generic.ReducedSystem, ExactVacuumAtlas.EinsteinMaxwell.ES5.Generic.ptR
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_ES5_Defs
import Definitions.Def_Atlas_EinsteinMaxwell_ES5_Generic_Data
import Definitions.Def_Atlas_EinsteinMaxwell_ES5_Generic_Reduced
import Definitions.Def_Atlas_EinsteinMaxwell_ES5_Generic_Tables
/-! # Equal-spin D = 5: certificate-level completeness of the reduced system (ATLAS-VI-02/02, D)

For arbitrary radial data `ESData R B D A H W Φ Ψ` (C^∞ on an open set of radii `R`,
`B, D, A, H ≠ 0` there) the Einstein–Maxwell certificate of the candidate's own fields
`esMetric`, `esInverse`, `esFaraday = d(esPotential)` on `esDomain R` holds **iff** the seven
reduced radial equations hold on `R` — given only the explicit signature assumption
`A > 0, H > 0, B D > 0` (used for the `lorentz` field and nothing else). Both directions are
proved; nothing about the field equations is assumed. -/

open scoped ContDiff
open ExactVacuumAtlas ExactVacuumAtlas.EinsteinMaxwell ExactVacuumAtlas.EinsteinMaxwell.D
open ExactVacuumAtlas.EinsteinMaxwell.ES5

namespace ExactVacuumAtlas.EinsteinMaxwell.ES5.Generic

variable {R : Set ℝ} {B D A H W Φ Ψ : ℝ → ℝ}

/-- The point `(t, r, u, φ, ψ) = (0, r, 1/2, 0, 0)`. -/
noncomputable def ptR (r : ℝ) : Pt 5 := fun i => if i.val = 1 then r else if i.val = 2 then 1 / 2 else 0

/-- The seven reduced radial equations on `R`. -/
def ReducedSystem (B D A H W Φ Ψ : ℝ → ℝ) (R : Set ℝ) : Prop :=
  ∀ r ∈ R, redE_tt B D A H W Φ Ψ r = 0 ∧ redE_tσ B D A H W Φ Ψ r = 0 ∧
    redE_rr B D A H W Φ Ψ r = 0 ∧ redE_uu B D A H W Φ Ψ r = 0 ∧ redE_σσ B D A H W Φ Ψ r = 0 ∧
    redJ_t B D A H W Φ Ψ r = 0 ∧ redJ_σ B D A H W Φ Ψ r = 0

end ExactVacuumAtlas.EinsteinMaxwell.ES5.Generic

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