Atlas VII definitions: ScalarCertificate

Definition

Atlas_EinsteinMaxwell_ES5_KerrSchild_ScalarCertificate

by He Wang · Nov 4, 2026 · Mathlib 0df444a (Lean v4.33.1)

einstein-maxwellexact-spacetime-atlas-viiexact-vacuum-atlasfive-dimensional-gravitygeneral-relativitykerr-schild

Definitions of the Atlas VII module Atlas.EinsteinMaxwell.ES5.KerrSchild.ScalarCertificate (kept exactly as in the accepted source, skeleton subtraction).

Atlas VII-00/01 (F1): scalar elimination certificate for the finite-jet obstruction.

Ported from the launch seed seed/ScalarCertificate.lean (sha256 86179aa0…, 2026-10-29). Changes against the seed: targeted Mathlib imports, linear_combination in place of nlinarith, and the scalar controls below. The formulas of C6, C7, C8, elimA, elimS are unchanged.

Variables (all real, no sign or nonvanishing assumption): M = M̂, J = Ĵ, Q = Q̂ (Fröb–Khavkine–Málek–Pravda 2022), c = a_φ^{(-1)}, h = r₊² - r₋² (a difference of squared radii, not a radius).

C6, C7, C8 are the x⁶, x⁷, x⁸ coefficients of the geodesic defect G computed from the transcribed asymptotic jet (paper Eq. 36), see PolynomialJet.lean for the Lean bridge to an actual polynomial. This file is pure scalar algebra: it is NOT a statement about solutions of the Einstein–Maxwell equations and NOT the geometric Kerr–Schild no-go.

Constants in this bundle: C6, C7, C8, elimA, elimS.

Registered B3 definition layer (Mathlib at the pinned revision has no Lorentzian metric / Ricci API): mission/PHYSICS_BOUNDARY.md, Atlas VII sections P–XVII.

Definition code

-- Generated by scripts/vii24r/publish/gen_platform_tree_unitA.py (Atlas VII Unit A; copy of the RELEASE06 generator, header only) by skeleton subtraction from Atlas/EinsteinMaxwell/ES5/KerrSchild/ScalarCertificate.lean
-- definition bundle: kept ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.FiniteJet.C6, ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.FiniteJet.C7, ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.FiniteJet.C8, ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.FiniteJet.elimA, ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.FiniteJet.elimS
import Mathlib
/-
Atlas VII-00/01 (F1): scalar elimination certificate for the finite-jet obstruction.

Ported from the launch seed `seed/ScalarCertificate.lean` (sha256 86179aa0…, 2026-10-29).
Changes against the seed: targeted Mathlib imports, `linear_combination` in place of
`nlinarith`, and the scalar controls below. The formulas of `C6`, `C7`, `C8`, `elimA`,
`elimS` are unchanged.

Variables (all real, no sign or nonvanishing assumption):
`M = M̂`, `J = Ĵ`, `Q = Q̂` (Fröb–Khavkine–Málek–Pravda 2022), `c = a_φ^{(-1)}`,
`h = r₊² - r₋²` (a difference of squared radii, not a radius).

`C6`, `C7`, `C8` are the x⁶, x⁷, x⁸ coefficients of the geodesic defect G computed from the
transcribed asymptotic jet (paper Eq. 36), see `PolynomialJet.lean` for the Lean bridge to an
actual polynomial. This file is pure scalar algebra: it is NOT a statement about solutions of the
Einstein–Maxwell equations and NOT the geometric Kerr–Schild no-go.
-/

set_option autoImplicit false

namespace ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.FiniteJet

/-- `[x⁶] G = (4/3) Q (M c + J Q)`. The argument `h` is unused; it is kept so that all
coefficients share the parameter list `(M h J Q c)`. -/
noncomputable def C6 (M _h J Q c : ℝ) : ℝ :=
  ((4 : ℝ) / 3) * M * Q * c +
    ((4 : ℝ) / 3) * J * Q ^ 2

/-- `[x⁷] G`. -/
noncomputable def C7 (M h J Q c : ℝ) : ℝ :=
  ((-1 : ℝ) / 2) * M ^ 2 * Q * c +
    (4 : ℝ) * M * h * Q * c +
    (-1 : ℝ) * M * J * Q ^ 2 +
    ((-1 : ℝ) / 2) * h ^ 2 * Q * c +
    (4 : ℝ) * h * J * Q ^ 2 +
    (2 : ℝ) * J * c ^ 2 +
    ((-8 : ℝ) / 3) * Q ^ 3 * c

/-- `[x⁸] G`. -/
noncomputable def C8 (M h J Q c : ℝ) : ℝ :=
  ((17 : ℝ) / 60) * M ^ 3 * Q * c +
    ((-7 : ℝ) / 4) * M ^ 2 * h * Q * c +
    ((5 : ℝ) / 6) * M ^ 2 * J * Q ^ 2 +
    ((481 : ℝ) / 60) * M * h ^ 2 * Q * c +
    ((-7 : ℝ) / 2) * M * h * J * Q ^ 2 +
    ((-5 : ℝ) / 3) * M * J * c ^ 2 +
    ((28 : ℝ) / 15) * M * Q ^ 3 * c +
    ((-7 : ℝ) / 4) * h ^ 3 * Q * c +
    ((112 : ℝ) / 15) * h ^ 2 * J * Q ^ 2 +
    (7 : ℝ) * h * J * c ^ 2 +
    ((-28 : ℝ) / 3) * h * Q ^ 3 * c +
    ((8 : ℝ) / 15) * J ^ 2 * Q * c +
    ((-16 : ℝ) / 15) * J * Q ^ 4 +
    ((32 : ℝ) / 15) * Q * c ^ 3

/-- Elimination multiplier `A = (7/2) h - (11/10) M`. -/
noncomputable def elimA (M h _J _Q _c : ℝ) : ℝ :=
  ((-11 : ℝ) / 10) * M +
    ((7 : ℝ) / 2) * h

/-- Elimination multiplier `S`. -/
noncomputable def elimS (M h J Q c : ℝ) : ℝ :=
  ((-4 : ℝ) / 15) * M ^ 5 * Q +
    ((22 : ℝ) / 5) * M ^ 4 * h * Q +
    ((-98 : ℝ) / 15) * M ^ 3 * h ^ 2 * Q +
    ((8 : ℝ) / 15) * M ^ 3 * J * c +
    ((-16 : ℝ) / 15) * M ^ 3 * Q ^ 3 +
    ((32 : ℝ) / 15) * M ^ 2 * Q * c ^ 2 +
    ((-32 : ℝ) / 15) * M * J * Q ^ 2 * c +
    ((32 : ℝ) / 15) * J ^ 2 * Q ^ 3

/-! ### Scalar controls -/

end ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.FiniteJet

Source

He Wang, Exact Spacetime Atlas VII, Unit A (restricted Kerr–Schild obstruction on the actual asymptotic branch, VII17). Local source, no public repository; commit f64ba9c823ec; Atlas/EinsteinMaxwell/ES5/KerrSchild/ScalarCertificate.lean; SHA-256 6e06b7677a26754185da742190085eabc3c481a0af205fea36919f37bc3498e7. Registered definitions: mission/PHYSICS_BOUNDARY.md (Atlas VII sections P–XVII). Physical Kerr–Schild obstruction: Fröb–Khavkine–Málek–Pravda, Eur. Phys. J. C 82 (2022) 215, arXiv:2112.13266 (Eqs. 23–25, 33, 59–60).

View graph