-- 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/CompactifiedResiduals.lean
-- definition bundle: kept ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.Compact.deltaFun, ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.Compact.gammaCore, ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.Compact.gammaGen, ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.Compact.paE, ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.Compact.paW, ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.Compact.pcE, ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.Compact.pcW, ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.Compact.pfE, ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.Compact.pmE, ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.Compact.pmW, ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.Compact.polyPA, ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.Compact.polyPC, ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.Compact.polyPM, ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.Compact.realGamma, ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.Compact.realPA, ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.Compact.realPC, ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.Compact.realPF, ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.Compact.realPM, ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.Compact.theta2P, ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.Compact.thetaP, ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.Compact.uP, ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.Compact.coeff_theta2P, ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.Compact.coeff_thetaP
import Mathlib
import Definitions.Def_Atlas_EinsteinMaxwell_ES5_KerrSchild_PolynomialJet
import Definitions.Def_Atlas_EinsteinMaxwell_ES5_KerrSchild_ScalarCertificate

/-! # VII-04 (F2c1): compactified residual expressions — one algebraic body, two instantiations

Factorized-N branch (an explicit branch choice, not a consequence of `N'' = 2`): real `s, h` and
`N(R) = (R - s)(R - s - h)`. Coordinates `x = 1/(R - s)`, `u = 1 - h x`, `f(R) = F(x)`,
`m(R) = b(x)/x`, `a(R) = A(x)`, `δ = d/dR = -x² d/dx`; primes below are `d/dx`.

`pfE pmE paE pcE` are the clear-denominator compactified residuals of the paper's Eqs. 24a, 24b,
24c and 25 (Fröb et al., EPJC 82:215 (2022)), written once over an arbitrary commutative ring with
the values `F F' F'' b b' b'' A A' A''` as arguments:

* `PF = 3 F u² · (24a)`, `PM = (3 x b u²/F) · (24b)`, `PA = u² · (24c)`, `PC = 4 x b F² u² · (25)`.

The *same* body is instantiated at real functions of `x` with genuine `deriv` (`realPF …`,
identities with the actual paper residuals in `CompactifiedBridge.lean`) and at `Polynomial ℝ` with
the formal derivative (`polyPF …`); `eval_polyPF` etc. prove that evaluating the polynomial version
is the real version of the polynomial functions. `gammaGen` is F1's Γ body with the jets `fJet`,
`mBarJet` replaced by arbitrary `F`, `b`; `realGamma` is its real-function version.

For coefficient extraction only, `pfW …` are the same expressions in the weighted variables
`x F'`, `x² F''` (`pfE_eq_pfW` etc., pure `ring`). Nothing here is evaluated at `x = 0` as a
statement about infinity. -/

open Polynomial

namespace ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.Compact

section Expr

variable {R : Type*} [CommRing R]

/-- `PF = 3 F u² · (Eq. 24a residual)`, compactified and cleared of denominators. -/
def pfE (x u h Q _J F F₁ F₂ b b₁ _b₂ A A₁ _A₂ : R) : R :=
  3 * F * u ^ 2 * (x * b * (b + x * b₁) * F₁ + x ^ 2 * b ^ 2 * F₂ - F * (b - x * b₁) ^ 2 + F ^ 2)
    - 6 * x ^ 2 * b ^ 2 * u ^ 2 * F₁ ^ 2
    + 6 * F ^ 2 * b * (b - x * b₁) * (2 - h * x) * u - 12 * F ^ 2 * b ^ 2 * u
    - 8 * F ^ 2 * b * x * u * (2 * b ^ 2 * x ^ 2 * A₁ ^ 2 - F * A ^ 2)
    + 4 * Q ^ 2 * F ^ 3 * b ^ 2 * x ^ 2

/-- `PM = (3 x b u²/F) · (Eq. 24b residual)`. -/
def pmE (x u h Q J F _F₁ _F₂ b b₁ b₂ A A₁ _A₂ : R) : R :=
  3 * u ^ 2 * (F * u - b ^ 2 + x ^ 2 * (u * b * b₂ - u * b₁ ^ 2 - h * b * b₁))
    - 4 * x * b * u ^ 2 * (2 * b ^ 2 * x ^ 2 * A₁ ^ 2 - F * A ^ 2)
    - 4 * Q ^ 2 * F * b ^ 2 * x ^ 2 * u
    - 12 * F * b ^ 3 * x ^ 3 * (J + 2 * Q * A) ^ 2

/-- `PA = u² · (Eq. 24c, left minus right)`. -/
def paE (x u _h Q J F _F₁ _F₂ b b₁ _b₂ A A₁ A₂ : R) : R :=
  u ^ 2 * (x * b * (b + x * b₁) * A₁ + x ^ 2 * b ^ 2 * A₂ - F * A)
    - 2 * Q * F * b ^ 2 * x ^ 2 * (J + 2 * Q * A)

/-- `PC = 4 x b F² u² · (Eq. 25 residual)`. -/
def pcE (x u _h Q J F F₁ _F₂ b b₁ _b₂ A A₁ _A₂ : R) : R :=
  F ^ 2 * u ^ 2 * ((2 - u) * b ^ 2 + 2 * x * b * b₁ + u * x ^ 2 * b₁ ^ 2)
    - F ^ 3 * u ^ 3
    - x * b * F * u ^ 2 * (b + u * x * b₁) * F₁
    + x ^ 2 * b ^ 2 * u ^ 3 * F₁ ^ 2
    + 4 * x ^ 3 * b ^ 3 * F ^ 2 * u ^ 2 * A₁ ^ 2
    - 4 * x * b * F ^ 3 * u ^ 2 * A ^ 2
    - 4 * Q ^ 2 * F ^ 3 * b ^ 2 * x ^ 2 * u
    - 4 * F ^ 3 * b ^ 3 * x ^ 3 * (J + 2 * Q * A) ^ 2

/-! Weighted forms (`dF = x F'`, `ddF = x² F''`, …), used only for coefficient extraction. -/

def pmW (x u h Q J F _dF _ddF b db ddb A dA _ddA : R) : R :=
  3 * (u * u * (F * u - b * b + u * b * ddb - u * db * db - h * (x * (b * db))))
    - 4 * (x * (b * u * u * (2 * (b * b * dA * dA) - F * A * A)))
    - 4 * (Q * (Q * (x * (x * (F * b * b * u)))))
    - 12 * (x * (x * (x * (F * b * b * b * (J + 2 * Q * A) * (J + 2 * Q * A)))))

def paW (x u _h Q J F _dF _ddF b db _ddb A dA ddA : R) : R :=
  u * u * (b * (b + db) * dA + b * b * ddA - F * A)
    - 2 * (Q * (x * (x * (F * b * b * (J + 2 * Q * A)))))

def pcW (x u _h Q J F dF _ddF b db _ddb A dA _ddA : R) : R :=
  F * F * u * u * ((2 - u) * b * b + 2 * (b * db) + u * db * db)
    - F * F * F * u * u * u
    - b * F * u * u * (b + u * db) * dF
    + b * b * u * u * u * dF * dF
    + 4 * (x * (b * b * b * F * F * u * u * dA * dA))
    - 4 * (x * (b * F * F * F * u * u * A * A))
    - 4 * (Q * (Q * (x * (x * (F * F * F * b * b * u)))))
    - 4 * (x * (x * (x * (F * F * F * b * b * b * (J + 2 * Q * A) * (J + 2 * Q * A)))))

variable {S : Type*} [CommRing S]

end Expr

/-! ## `Polynomial ℝ` atoms and their coefficients (all orders `n`) -/

/-- Euler operator `θ p = x p'`. -/
noncomputable def thetaP (p : ℝ[X]) : ℝ[X] := X * derivative p
/-- `θ₂ p = x² p''`. -/
noncomputable def theta2P (p : ℝ[X]) : ℝ[X] := X ^ 2 * derivative (derivative p)
/-- `u = 1 - h x`. -/
noncomputable def uP (h : ℝ) : ℝ[X] := 1 - C h * X

theorem coeff_thetaP (p : ℝ[X]) (n : ℕ) : (thetaP p).coeff n = (n : ℝ) * p.coeff n := by
  rcases n with _ | k
  · simp [thetaP]
  · rw [thetaP, coeff_X_mul, coeff_derivative]; push_cast; ring

theorem coeff_theta2P (p : ℝ[X]) (n : ℕ) :
    (theta2P p).coeff n = (n : ℝ) * ((n : ℝ) - 1) * p.coeff n := by
  rcases n with _ | _ | k
  · simp [theta2P]
  · simp [theta2P, coeff_X_pow_mul']
  · rw [theta2P, mul_comm, show k + 1 + 1 = k + 2 from rfl, coeff_mul_X_pow, coeff_derivative,
      coeff_derivative]
    push_cast; ring

/-! Literal-index forms (decided by the default `Nat` simprocs at numeral indices). -/

/-! ## The polynomial residuals (formal derivative) and their weighted forms -/

noncomputable def polyPM (h Q J : ℝ) (F b A : ℝ[X]) : ℝ[X] :=
  pmE X (uP h) (C h) (C Q) (C J) F (derivative F) (derivative (derivative F)) b (derivative b)
    (derivative (derivative b)) A (derivative A) (derivative (derivative A))
noncomputable def polyPA (h Q J : ℝ) (F b A : ℝ[X]) : ℝ[X] :=
  paE X (uP h) (C h) (C Q) (C J) F (derivative F) (derivative (derivative F)) b (derivative b)
    (derivative (derivative b)) A (derivative A) (derivative (derivative A))
noncomputable def polyPC (h Q J : ℝ) (F b A : ℝ[X]) : ℝ[X] :=
  pcE X (uP h) (C h) (C Q) (C J) F (derivative F) (derivative (derivative F)) b (derivative b)
    (derivative (derivative b)) A (derivative A) (derivative (derivative A))

/-! ## Generic Γ (F1's body with unknown `F`, `b`) and its weighted core -/

/-- F1's `gammaWith` body with `fJet`, `mBarJet` replaced by arbitrary `F`, `b`. -/
noncomputable def gammaGen (h Q J : ℝ) (F b A : ℝ[X]) : ℝ[X] :=
  let u := 1 - C h * X
  C Q * (u * X ^ 2 * F * FiniteJet.deltaR (FiniteJet.deltaR A)
    - u * FiniteJet.deltaR (X ^ 2 * F) * FiniteJet.deltaR A
    + C h * X ^ 4 * F * FiniteJet.deltaR A)
    + C 2 * (C J + C (2 * Q) * A) * F * X ^ 3 * b * (FiniteJet.deltaR A) ^ 2

/-- `Γ = x⁴ · gammaCore`. -/
noncomputable def gammaCore (h Q J : ℝ) (F b A : ℝ[X]) : ℝ[X] :=
  C Q * (uP h * F * (C 2 * thetaP A + theta2P A) - uP h * (C 2 * F + thetaP F) * thetaP A
      - C h * (X * (F * thetaP A)))
    + C 2 * (X * ((C J + C (2 * Q) * A) * F * b * thetaP A * thetaP A))

/-! ## Real-function versions and the evaluation bridge -/

/-- The real compactified residuals of functions `F b A` of `x` (genuine `deriv`). -/
noncomputable def realPF (h Q J : ℝ) (F b A : ℝ → ℝ) (x : ℝ) : ℝ :=
  pfE x (1 - h * x) h Q J (F x) (deriv F x) (deriv (deriv F) x) (b x) (deriv b x)
    (deriv (deriv b) x) (A x) (deriv A x) (deriv (deriv A) x)
noncomputable def realPM (h Q J : ℝ) (F b A : ℝ → ℝ) (x : ℝ) : ℝ :=
  pmE x (1 - h * x) h Q J (F x) (deriv F x) (deriv (deriv F) x) (b x) (deriv b x)
    (deriv (deriv b) x) (A x) (deriv A x) (deriv (deriv A) x)
noncomputable def realPA (h Q J : ℝ) (F b A : ℝ → ℝ) (x : ℝ) : ℝ :=
  paE x (1 - h * x) h Q J (F x) (deriv F x) (deriv (deriv F) x) (b x) (deriv b x)
    (deriv (deriv b) x) (A x) (deriv A x) (deriv (deriv A) x)
noncomputable def realPC (h Q J : ℝ) (F b A : ℝ → ℝ) (x : ℝ) : ℝ :=
  pcE x (1 - h * x) h Q J (F x) (deriv F x) (deriv (deriv F) x) (b x) (deriv b x)
    (deriv (deriv b) x) (A x) (deriv A x) (deriv (deriv A) x)

/-- `δ = -x² d/dx` on real functions of `x`. -/
noncomputable def deltaFun (g : ℝ → ℝ) : ℝ → ℝ := fun x => -x ^ 2 * deriv g x

/-- Real-function version of `gammaGen`. -/
noncomputable def realGamma (h Q J : ℝ) (F b A : ℝ → ℝ) (x : ℝ) : ℝ :=
  Q * ((1 - h * x) * x ^ 2 * F x * deltaFun (deltaFun A) x
    - (1 - h * x) * deltaFun (fun y => y ^ 2 * F y) x * deltaFun A x
    + h * x ^ 4 * F x * deltaFun A x)
    + 2 * (J + 2 * Q * A x) * F x * x ^ 3 * b x * (deltaFun A x) ^ 2

section EvalBridge

variable (h Q J : ℝ) (F b A : ℝ[X]) (x : ℝ)

end EvalBridge

end ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.Compact