Atlas VII definitions: PolynomialJet

-- 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/PolynomialJet.lean
-- definition bundle: kept ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.FiniteJet.aJet, ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.FiniteJet.deltaR, ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.FiniteJet.ePart, ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.FiniteJet.fJet, ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.FiniteJet.gammaHigh, ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.FiniteJet.gammaJet, ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.FiniteJet.gammaLow, ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.FiniteJet.gammaWith, ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.FiniteJet.mBarJet
import Mathlib
import Definitions.Def_Atlas_EinsteinMaxwell_ES5_KerrSchild_ScalarCertificate
/-
Atlas VII-00/01 (F1): actual `Polynomial ℝ` coefficient bridge for the finite-jet obstruction.

Ported from the launch seed `seed/PolynomialJetDefs.lean` (sha256 a85552443…, 2026-10-29).
`fJet`, `aJet`, `mBarJet`, `deltaR` are the seed definitions unchanged (seed import path
`Mathlib.Data.Polynomial.Derivative` replaced by the pinned `Mathlib.Algebra.Polynomial.Derivative`).
The seed body of `gammaJet` is moved verbatim into `gammaWith`, which takes the a-jet as an
argument (needed for the wrong-input control); `gammaJet_eq_seed` records that `gammaJet` is
definitionally the seed expression.

Coordinates and variables: `x = 1/(R - r₋²)`, `R = 𝗋²` the paper's radial variable,
`δ = d/dR = -x² d/dx` (`deltaR`), `h = r₊² - r₋²`, `c = a_φ^{(-1)}`; `M J Q` as in
`ScalarCertificate.lean`. The jets `fJet` (f through x³), `aJet` (a_φ through x⁴) and `mBarJet`
(m̄ = x m through x¹) transcribe Fröb–Khavkine–Málek–Pravda 2022, Eq. 36.

`gammaJet` is an honest real polynomial. In the formal-series sense it represents `(1 - h x)² G`
for the geodesic defect `G = a' a₀'' - a₀' a''` after eliminating `a₀'` and `ϖ'` by Eqs. 23b/c;
that interpretation is NOT formalised here. Only the x⁶, x⁷, x⁸ coefficients are meaningful for
the truncated jets; higher coefficients depend on omitted jet orders.

Boundary (see notes/VII_BRIDGE_STATUS.md): nothing in this file proves that a solution of the
five-dimensional Einstein–Maxwell equations has these jets (F2), nor any Kerr–Schild geometry (F3).
-/

set_option autoImplicit false
open Polynomial

namespace ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.FiniteJet

/-! ### Seed definitions (unchanged) -/

noncomputable def fJet (M h J Q c : ℝ) : Polynomial ℝ :=
  C ((1 : ℝ)) +
    C ((-1 : ℝ) * M) * X ^ 1 +
    C (((1 : ℝ) / 2) * M ^ 2 + ((-1 : ℝ) / 2) * M * h + ((4 : ℝ) / 3) * Q ^ 2) * X ^ 2 +
    C (((-1 : ℝ) / 6) * M ^ 3 + ((1 : ℝ) / 2) * M ^ 2 * h + ((-1 : ℝ) / 3) * M * h ^ 2 + ((-16 : ℝ) / 9) * M * Q ^ 2 + ((4 : ℝ) / 3) * h * Q ^ 2 + ((2 : ℝ) / 3) * J ^ 2 + ((4 : ℝ) / 9) * c ^ 2) * X ^ 3

noncomputable def aJet (M h J Q c : ℝ) : Polynomial ℝ :=
  C ((1 : ℝ) * c) * X ^ 1 +
    C (((1 : ℝ) / 6) * M * c + ((1 : ℝ) / 2) * h * c + ((2 : ℝ) / 3) * J * Q) * X ^ 2 +
    C (((1 : ℝ) / 12) * M ^ 2 * c + ((1 : ℝ) / 6) * M * h * c + ((-1 : ℝ) / 6) * M * J * Q + ((1 : ℝ) / 4) * h ^ 2 * c + ((2 : ℝ) / 3) * h * J * Q) * X ^ 3 +
    C (((1 : ℝ) / 60) * M ^ 3 * c + ((1 : ℝ) / 8) * M ^ 2 * h * c + ((1 : ℝ) / 12) * M ^ 2 * J * Q + ((2 : ℝ) / 15) * M * h ^ 2 * c + ((-1 : ℝ) / 4) * M * h * J * Q + ((-34 : ℝ) / 135) * M * Q ^ 2 * c + ((1 : ℝ) / 8) * h ^ 3 * c + ((17 : ℝ) / 30) * h ^ 2 * J * Q + ((-7 : ℝ) / 30) * J ^ 2 * c + ((8 : ℝ) / 135) * J * Q ^ 3 + ((-2 : ℝ) / 45) * c ^ 3) * X ^ 4

noncomputable def mBarJet (M h _J _Q _c : ℝ) : Polynomial ℝ :=
  C ((1 : ℝ)) +
    C (((-1 : ℝ) / 2) * M + ((-1 : ℝ) / 2) * h) * X ^ 1

/-- `δ = d/dR = -x² d/dx` acting on polynomials in `x`. -/
noncomputable def deltaR (p : Polynomial ℝ) : Polynomial ℝ :=
  -(X ^ 2) * p.derivative

/-- The seed body of Γ with the a-jet as a free argument. -/
noncomputable def gammaWith (M h J Q c : ℝ) (a : Polynomial ℝ) : Polynomial ℝ :=
  let f := fJet M h J Q c
  let mbar := mBarJet M h J Q c
  let u := 1 - C h * X
  C Q * (u * X ^ 2 * f * deltaR (deltaR a)
    - u * deltaR (X ^ 2 * f) * deltaR a
    + C h * X ^ 4 * f * deltaR a)
    + C 2 * (C J + C (2 * Q) * a) * f * X ^ 3 * mbar * (deltaR a) ^ 2

/-- Γ for the transcribed jets. -/
noncomputable def gammaJet (M h J Q c : ℝ) : Polynomial ℝ :=
  gammaWith M h J Q c (aJet M h J Q c)

/-! ### Structural factorisation Γ = X⁵ K₁ + X⁷ K₂ -/

/-- `E p = -(2 p + x p')`, so that `δ(x² p) = x³ E p`. -/
noncomputable def ePart (p : Polynomial ℝ) : Polynomial ℝ :=
  -(C 2 * p + X * derivative p)

/-- The x⁵-part of Γ divided by x⁵. -/
noncomputable def gammaLow (M h J Q c : ℝ) (a : Polynomial ℝ) : Polynomial ℝ :=
  C Q * ((1 - C h * X) * (fJet M h J Q c * ePart (-derivative a)
      - ePart (fJet M h J Q c) * (-derivative a))
    + C h * X * fJet M h J Q c * (-derivative a))

/-- The x⁷-part of Γ divided by x⁷. -/
noncomputable def gammaHigh (M h J Q c : ℝ) (a : Polynomial ℝ) : Polynomial ℝ :=
  C 2 * (C J + C (2 * Q) * a) * fJet M h J Q c * mBarJet M h J Q c *
    (derivative a * derivative a)

/-! ### Low-index coefficients of products (factors kept abstract) -/

/-! ### Coefficient bridge: `[x^k] Γ` for the transcribed jets -/

/-! ### Wrong-input control: a₄ ↦ a₄ + 1 -/

end ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.FiniteJet