VI-02 seven reduced radial functions

-- Generated by scripts/release06/gen_platform_tree.py (RELEASE06; copy of release05, header only) by skeleton subtraction from Atlas/EinsteinMaxwell/ES5/Generic/Reduced.lean
-- definition bundle: kept ExactVacuumAtlas.EinsteinMaxwell.ES5.Generic.redE_rr, ExactVacuumAtlas.EinsteinMaxwell.ES5.Generic.redE_tt, ExactVacuumAtlas.EinsteinMaxwell.ES5.Generic.redE_tσ, ExactVacuumAtlas.EinsteinMaxwell.ES5.Generic.redE_uu, ExactVacuumAtlas.EinsteinMaxwell.ES5.Generic.redE_σσ, ExactVacuumAtlas.EinsteinMaxwell.ES5.Generic.redJ_t, ExactVacuumAtlas.EinsteinMaxwell.ES5.Generic.redJ_σ
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_Tables
set_option maxHeartbeats 8000000
set_option maxRecDepth 100000
set_option linter.unusedVariables false
set_option linter.unusedSimpArgs false
set_option linter.unusedTactic false
set_option linter.unreachableTactic false

/-! Generated by `scripts/vi02_02/es5generic.py`. Reduced (frame, `u`-free) residuals of the generic ansatz and the completeness theorems: the full 5D system `einsteinMaxwellD = 0`, `maxwellDiv = 0`, `faradayCyclic = 0` of the candidate's own fields is equivalent, at every point, to seven radial equations. -/

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 Φ Ψ : ℝ → ℝ}

/-- Reduced Einstein–Maxwell residual `E^t_t` (frame components, `u`-free). -/
noncomputable def redE_tt (B D A H W Φ Ψ : ℝ → ℝ) (r : ℝ) : ℝ :=
  ((-16:ℝ) * B r * D r ^ 2 * A r * H r ^ 2 + (4:ℝ) * B r * D r ^ 2 * H r ^ 3 + (16:ℝ) * B r * D r ^ 2 * H r ^ 2 * Ψ r ^ 2 + (2:ℝ) * B r * D r * A r ^ 2 * H r * deriv (deriv H) r + (4:ℝ) * B r * D r * A r ^ 2 * H r * deriv Ψ r ^ 2 + (-1:ℝ) * B r * D r * A r ^ 2 * deriv H r ^ 2 + (2:ℝ) * B r * D r * A r * deriv A r * H r * deriv H r + (4:ℝ) * B r * D r * A r * deriv (deriv A) r * H r ^ 2 + (-1:ℝ) * B r * D r * deriv A r ^ 2 * H r ^ 2 + (-1:ℝ) * B r * deriv D r * A r ^ 2 * H r * deriv H r + (-2:ℝ) * B r * deriv D r * A r * deriv A r * H r ^ 2 + (1:ℝ) * D r * A r ^ 2 * H r ^ 3 * deriv W r ^ 2 + (4:ℝ) * D r * A r ^ 2 * H r ^ 2 * W r ^ 2 * deriv Ψ r ^ 2 + (8:ℝ) * D r * A r ^ 2 * H r ^ 2 * W r * deriv Φ r * deriv Ψ r + (4:ℝ) * D r * A r ^ 2 * H r ^ 2 * deriv Φ r ^ 2) / ((4:ℝ) * B r * D r ^ 2 * A r ^ 2 * H r ^ 2)
/-- Reduced Einstein–Maxwell residual `E^t_σ` (frame components, `u`-free). -/
noncomputable def redE_tσ (B D A H W Φ Ψ : ℝ → ℝ) (r : ℝ) : ℝ :=
  ((-2:ℝ) * B r * D r * A r * H r * deriv (deriv W) r + (-3:ℝ) * B r * D r * A r * deriv H r * deriv W r + (8:ℝ) * B r * D r * A r * W r * deriv Ψ r ^ 2 + (8:ℝ) * B r * D r * A r * deriv Φ r * deriv Ψ r + (-2:ℝ) * B r * D r * deriv A r * H r * deriv W r + (1:ℝ) * B r * deriv D r * A r * H r * deriv W r + (1:ℝ) * deriv B r * D r * A r * H r * deriv W r) / ((4:ℝ) * B r ^ 2 * D r ^ 2 * A r)
/-- Reduced Einstein–Maxwell residual `E^r_r` (frame components, `u`-free). -/
noncomputable def redE_rr (B D A H W Φ Ψ : ℝ → ℝ) (r : ℝ) : ℝ :=
  ((-16:ℝ) * B r * D r * A r * H r + (4:ℝ) * B r * D r * H r ^ 2 + (16:ℝ) * B r * D r * H r * Ψ r ^ 2 + (-4:ℝ) * B r * A r ^ 2 * deriv Ψ r ^ 2 + (2:ℝ) * B r * A r * deriv A r * deriv H r + (1:ℝ) * B r * deriv A r ^ 2 * H r + (1:ℝ) * deriv B r * A r ^ 2 * deriv H r + (2:ℝ) * deriv B r * A r * deriv A r * H r + (1:ℝ) * A r ^ 2 * H r ^ 2 * deriv W r ^ 2 + (4:ℝ) * A r ^ 2 * H r * W r ^ 2 * deriv Ψ r ^ 2 + (8:ℝ) * A r ^ 2 * H r * W r * deriv Φ r * deriv Ψ r + (4:ℝ) * A r ^ 2 * H r * deriv Φ r ^ 2) / ((4:ℝ) * B r * D r * A r ^ 2 * H r)
/-- Reduced Einstein–Maxwell residual `E^u_u` (frame components, `u`-free). -/
noncomputable def redE_uu (B D A H W Φ Ψ : ℝ → ℝ) (r : ℝ) : ℝ :=
  ((-4:ℝ) * B r ^ 2 * D r ^ 2 * H r ^ 3 + (-16:ℝ) * B r ^ 2 * D r ^ 2 * H r ^ 2 * Ψ r ^ 2 + (2:ℝ) * B r ^ 2 * D r * A r ^ 2 * H r * deriv (deriv H) r + (4:ℝ) * B r ^ 2 * D r * A r ^ 2 * H r * deriv Ψ r ^ 2 + (-1:ℝ) * B r ^ 2 * D r * A r ^ 2 * deriv H r ^ 2 + (1:ℝ) * B r ^ 2 * D r * A r * deriv A r * H r * deriv H r + (2:ℝ) * B r ^ 2 * D r * A r * deriv (deriv A) r * H r ^ 2 + (-1:ℝ) * B r ^ 2 * D r * deriv A r ^ 2 * H r ^ 2 + (-1:ℝ) * B r ^ 2 * deriv D r * A r ^ 2 * H r * deriv H r + (-1:ℝ) * B r ^ 2 * deriv D r * A r * deriv A r * H r ^ 2 + (1:ℝ) * B r * deriv B r * D r * A r ^ 2 * H r * deriv H r + (1:ℝ) * B r * deriv B r * D r * A r * deriv A r * H r ^ 2 + (-1:ℝ) * B r * deriv B r * deriv D r * A r ^ 2 * H r ^ 2 + (2:ℝ) * B r * deriv (deriv B) r * D r * A r ^ 2 * H r ^ 2 + (-1:ℝ) * B r * D r * A r ^ 2 * H r ^ 3 * deriv W r ^ 2 + (-4:ℝ) * B r * D r * A r ^ 2 * H r ^ 2 * W r ^ 2 * deriv Ψ r ^ 2 + (-8:ℝ) * B r * D r * A r ^ 2 * H r ^ 2 * W r * deriv Φ r * deriv Ψ r + (-4:ℝ) * B r * D r * A r ^ 2 * H r ^ 2 * deriv Φ r ^ 2 + (-1:ℝ) * deriv B r ^ 2 * D r * A r ^ 2 * H r ^ 2) / ((4:ℝ) * B r ^ 2 * D r ^ 2 * A r ^ 2 * H r ^ 2)
/-- Reduced Einstein–Maxwell residual `E^σ_σ` (frame components, `u`-free). -/
noncomputable def redE_σσ (B D A H W Φ Ψ : ℝ → ℝ) (r : ℝ) : ℝ :=
  ((-16:ℝ) * B r ^ 2 * D r ^ 2 * A r * H r + (12:ℝ) * B r ^ 2 * D r ^ 2 * H r ^ 2 + (16:ℝ) * B r ^ 2 * D r ^ 2 * H r * Ψ r ^ 2 + (-4:ℝ) * B r ^ 2 * D r * A r ^ 2 * deriv Ψ r ^ 2 + (4:ℝ) * B r ^ 2 * D r * A r * deriv (deriv A) r * H r + (-1:ℝ) * B r ^ 2 * D r * deriv A r ^ 2 * H r + (-2:ℝ) * B r ^ 2 * deriv D r * A r * deriv A r * H r + (2:ℝ) * B r * deriv B r * D r * A r * deriv A r * H r + (-1:ℝ) * B r * deriv B r * deriv D r * A r ^ 2 * H r + (2:ℝ) * B r * deriv (deriv B) r * D r * A r ^ 2 * H r + (-3:ℝ) * B r * D r * A r ^ 2 * H r ^ 2 * deriv W r ^ 2 + (-4:ℝ) * B r * D r * A r ^ 2 * H r * W r ^ 2 * deriv Ψ r ^ 2 + (-8:ℝ) * B r * D r * A r ^ 2 * H r * W r * deriv Φ r * deriv Ψ r + (-4:ℝ) * B r * D r * A r ^ 2 * H r * deriv Φ r ^ 2 + (-1:ℝ) * deriv B r ^ 2 * D r * A r ^ 2 * H r) / ((4:ℝ) * B r ^ 2 * D r ^ 2 * A r ^ 2 * H r)
/-- Reduced Maxwell residual `θ^t(J)`, `J^b = maxwellDiv … b`. -/
noncomputable def redJ_t (B D A H W Φ Ψ : ℝ → ℝ) (r : ℝ) : ℝ :=
  ((-2:ℝ) * B r * D r * A r * H r * W r * deriv (deriv Ψ) r + (-2:ℝ) * B r * D r * A r * H r * deriv W r * deriv Ψ r + (-2:ℝ) * B r * D r * A r * H r * deriv (deriv Φ) r + (-1:ℝ) * B r * D r * A r * deriv H r * W r * deriv Ψ r + (-1:ℝ) * B r * D r * A r * deriv H r * deriv Φ r + (-2:ℝ) * B r * D r * deriv A r * H r * W r * deriv Ψ r + (-2:ℝ) * B r * D r * deriv A r * H r * deriv Φ r + (1:ℝ) * B r * deriv D r * A r * H r * W r * deriv Ψ r + (1:ℝ) * B r * deriv D r * A r * H r * deriv Φ r + (1:ℝ) * deriv B r * D r * A r * H r * W r * deriv Ψ r + (1:ℝ) * deriv B r * D r * A r * H r * deriv Φ r) / ((2:ℝ) * B r ^ 2 * D r ^ 2 * A r * H r)
/-- Reduced Maxwell residual `θ^σ(J)`, `J^b = maxwellDiv … b`. -/
noncomputable def redJ_σ (B D A H W Φ Ψ : ℝ → ℝ) (r : ℝ) : ℝ :=
  ((-8:ℝ) * B r * D r ^ 2 * H r ^ 2 * Ψ r + (2:ℝ) * B r * D r * A r ^ 2 * H r * deriv (deriv Ψ) r + (-1:ℝ) * B r * D r * A r ^ 2 * deriv H r * deriv Ψ r + (2:ℝ) * B r * D r * A r * deriv A r * H r * deriv Ψ r + (-1:ℝ) * B r * deriv D r * A r ^ 2 * H r * deriv Ψ r + (1:ℝ) * deriv B r * D r * A r ^ 2 * H r * deriv Ψ r + (-2:ℝ) * D r * A r ^ 2 * H r ^ 2 * W r * deriv W r * deriv Ψ r + (-2:ℝ) * D r * A r ^ 2 * H r ^ 2 * deriv W r * deriv Φ r) / ((2:ℝ) * B r * D r ^ 2 * A r ^ 2 * H r ^ 2)

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