VI-02 normalised generic tables

-- Generated by scripts/release06/gen_platform_tree.py (RELEASE06; copy of release05, header only) by skeleton subtraction from Atlas/EinsteinMaxwell/ES5/Generic/Tables.lean
-- definition bundle: kept ExactVacuumAtlas.EinsteinMaxwell.ES5.Generic.FG, ExactVacuumAtlas.EinsteinMaxwell.ES5.Generic.gG, ExactVacuumAtlas.EinsteinMaxwell.ES5.Generic.giG
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
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`. Normalised closed forms `gG`, `giG`, `FG` of the generic ansatz, bound to `esMetric`, `esInverse`, `esFaraday` on `esDomain R`; `pd` of their components. -/

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

noncomputable def gG (B D A H W : ℝ → ℝ) : Metric 5
  | 0, 0 => liftRU (fun r u => ((-1:ℝ) * B r + (1:ℝ) * H r * W r ^ 2) : ℝ → ℝ → ℝ)
  | 0, 3 => liftRU (fun r u => ((-1:ℝ) * H r * W r * u) : ℝ → ℝ → ℝ)
  | 0, 4 => liftRU (fun r u => ((1:ℝ) * H r * W r * u + (-1:ℝ) * H r * W r) : ℝ → ℝ → ℝ)
  | 1, 1 => liftRU (fun r u => ((1:ℝ) * D r) : ℝ → ℝ → ℝ)
  | 2, 2 => liftRU (fun r u => ((1:ℝ) * A r) / ((4:ℝ) * u * (1 - u)) : ℝ → ℝ → ℝ)
  | 3, 0 => liftRU (fun r u => ((-1:ℝ) * H r * W r * u) : ℝ → ℝ → ℝ)
  | 3, 3 => liftRU (fun r u => ((-1:ℝ) * A r * u ^ 2 + (1:ℝ) * A r * u + (1:ℝ) * H r * u ^ 2) : ℝ → ℝ → ℝ)
  | 3, 4 => liftRU (fun r u => ((1:ℝ) * A r * u ^ 2 + (-1:ℝ) * A r * u + (-1:ℝ) * H r * u ^ 2 + (1:ℝ) * H r * u) : ℝ → ℝ → ℝ)
  | 4, 0 => liftRU (fun r u => ((1:ℝ) * H r * W r * u + (-1:ℝ) * H r * W r) : ℝ → ℝ → ℝ)
  | 4, 3 => liftRU (fun r u => ((1:ℝ) * A r * u ^ 2 + (-1:ℝ) * A r * u + (-1:ℝ) * H r * u ^ 2 + (1:ℝ) * H r * u) : ℝ → ℝ → ℝ)
  | 4, 4 => liftRU (fun r u => ((-1:ℝ) * A r * u ^ 2 + (1:ℝ) * A r * u + (1:ℝ) * H r * u ^ 2 + (-2:ℝ) * H r * u + (1:ℝ) * H r) : ℝ → ℝ → ℝ)
  | _, _ => liftRU (fun _ _ => (0:ℝ))

noncomputable def giG (B D A H W : ℝ → ℝ) : Metric 5
  | 0, 0 => liftRU (fun r u => ((-1:ℝ)) / ((1:ℝ) * B r) : ℝ → ℝ → ℝ)
  | 0, 3 => liftRU (fun r u => ((-1:ℝ) * W r) / ((1:ℝ) * B r) : ℝ → ℝ → ℝ)
  | 0, 4 => liftRU (fun r u => ((-1:ℝ) * W r) / ((1:ℝ) * B r) : ℝ → ℝ → ℝ)
  | 1, 1 => liftRU (fun r u => ((1:ℝ)) / ((1:ℝ) * D r) : ℝ → ℝ → ℝ)
  | 2, 2 => liftRU (fun r u => ((-4:ℝ) * u ^ 2 + (4:ℝ) * u) / ((1:ℝ) * A r) : ℝ → ℝ → ℝ)
  | 3, 0 => liftRU (fun r u => ((-1:ℝ) * W r) / ((1:ℝ) * B r) : ℝ → ℝ → ℝ)
  | 3, 3 => liftRU (fun r u => ((1:ℝ) * B r * A r * u + (-1:ℝ) * B r * H r * u + (1:ℝ) * B r * H r + (-1:ℝ) * A r * H r * W r ^ 2 * u) / ((1:ℝ) * B r * A r * H r * u) : ℝ → ℝ → ℝ)
  | 3, 4 => liftRU (fun r u => ((1:ℝ) * B r * A r + (-1:ℝ) * B r * H r + (-1:ℝ) * A r * H r * W r ^ 2) / ((1:ℝ) * B r * A r * H r) : ℝ → ℝ → ℝ)
  | 4, 0 => liftRU (fun r u => ((-1:ℝ) * W r) / ((1:ℝ) * B r) : ℝ → ℝ → ℝ)
  | 4, 3 => liftRU (fun r u => ((1:ℝ) * B r * A r + (-1:ℝ) * B r * H r + (-1:ℝ) * A r * H r * W r ^ 2) / ((1:ℝ) * B r * A r * H r) : ℝ → ℝ → ℝ)
  | 4, 4 => liftRU (fun r u => ((-1:ℝ) * B r * A r * u + (1:ℝ) * B r * A r + (1:ℝ) * B r * H r * u + (1:ℝ) * A r * H r * W r ^ 2 * u + (-1:ℝ) * A r * H r * W r ^ 2) / ((1:ℝ) * B r * A r * H r * (1 - u)) : ℝ → ℝ → ℝ)
  | _, _ => liftRU (fun _ _ => (0:ℝ))

noncomputable def FG (Φ Ψ : ℝ → ℝ) : TwoForm 5
  | 0, 1 => liftRU (fun r u => ((-1:ℝ) * deriv Φ r) : ℝ → ℝ → ℝ)
  | 1, 0 => liftRU (fun r u => ((1:ℝ) * deriv Φ r) : ℝ → ℝ → ℝ)
  | 1, 3 => liftRU (fun r u => ((1:ℝ) * deriv Ψ r * u) : ℝ → ℝ → ℝ)
  | 1, 4 => liftRU (fun r u => ((-1:ℝ) * deriv Ψ r * u + (1:ℝ) * deriv Ψ r) : ℝ → ℝ → ℝ)
  | 2, 3 => liftRU (fun r u => ((1:ℝ) * Ψ r) : ℝ → ℝ → ℝ)
  | 2, 4 => liftRU (fun r u => ((-1:ℝ) * Ψ r) : ℝ → ℝ → ℝ)
  | 3, 1 => liftRU (fun r u => ((-1:ℝ) * deriv Ψ r * u) : ℝ → ℝ → ℝ)
  | 3, 2 => liftRU (fun r u => ((-1:ℝ) * Ψ r) : ℝ → ℝ → ℝ)
  | 4, 1 => liftRU (fun r u => ((1:ℝ) * deriv Ψ r * u + (-1:ℝ) * deriv Ψ r) : ℝ → ℝ → ℝ)
  | 4, 2 => liftRU (fun r u => ((1:ℝ) * Ψ r) : ℝ → ℝ → ℝ)
  | _, _ => liftRU (fun _ _ => (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).