-- 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/JetRecursion.lean
-- definition bundle: kept ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.Compact.JetNormalization, ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.Compact.SelectedRows, ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.Compact.jetA2, ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.Compact.jetA3, ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.Compact.jetA4, ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.Compact.jetB1, ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.Compact.jetB2, ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.Compact.jetB3, ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.Compact.jetF2, ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.Compact.jetF3, ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.Compact.AgreeBelow
import Mathlib
import Definitions.Def_Atlas_EinsteinMaxwell_ES5_KerrSchild_CompactifiedResiduals
import Definitions.Def_Atlas_EinsteinMaxwell_ES5_KerrSchild_FiniteJetObstruction
import Definitions.Def_Atlas_EinsteinMaxwell_ES5_KerrSchild_PolynomialJet
import Definitions.Def_Atlas_EinsteinMaxwell_ES5_KerrSchild_ScalarCertificate

/-! # VII-04 (F2c1): finite coefficient recursion of the actual compactified residual polynomials

Unknown `F b A : Polynomial ℝ` with only the leading normalisation
`F₀ = b₀ = 1, A₀ = 0, F₁ = -M, A₁ = c` (`JetNormalization`). The *rows* are the coefficients of
the actual polynomials `polyPF polyPM polyPA polyPC` of `CompactifiedResiduals.lean`; each row
lemma states `(actual residual).coeff k = explicit expression in the low coefficients`, proved by
opaque-factor product-coefficient lemmas (the factors `F b A` are never expanded), so it holds for
*every* polynomial with that normalisation, whatever its higher coefficients. Independently, for
every order `n` the coefficients below `n` of the four residuals (below `n + 4` of Γ) depend only on
the coefficients below `n` of `F b A` (`residuals_agreeBelow`, `gammaGen_agreeBelow`).

The eight selected rows (`SelectedRows`) determine, in triangular order with fixed integer pivots
only, `B₁ F₂ B₂ A₂ A₃ F₃ B₃ A₄` (`jet_recursion`); nothing is divided by `M h J Q c`. These are
outputs, not inputs. The generic Γ coefficients 6, 7, 8 depend only on `F≤3, b≤1, A≤4`
(`gammaGen_coeff_six/seven/eight`), so they coincide with F1's `gammaJet` coefficients, and F1's
obstruction applies (`vii04_compactified_jet_recursion`).

Boundary: this is a finite-coefficient statement about polynomials. How an actual real solution
(one-sided expansion at `x = 0`, remainder control) yields these coefficient conditions is F2c2
and is not proved here; F3 (Kerr–Schild geometry) is not touched. -/

open Polynomial

namespace ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.Compact

/-- The only coefficient inputs: leading normalisation of the unknown jets. -/
structure JetNormalization (M c : ℝ) (F b A : ℝ[X]) : Prop where
  F0 : F.coeff 0 = 1
  b0 : b.coeff 0 = 1
  A0 : A.coeff 0 = 0
  F1 : F.coeff 1 = -M
  A1 : A.coeff 1 = c

variable {M h J Q c : ℝ} {F b A : ℝ[X]}

/-! ## Locality at every order `n` (no truncation, arbitrary tails) -/

/-- `p` and `q` have the same coefficients below `n`. -/
def AgreeBelow (n : ℕ) (p q : ℝ[X]) : Prop := ∀ k < n, p.coeff k = q.coeff k

section Locality

variable {n : ℕ} {F' b' A' : ℝ[X]} (hF : AgreeBelow n F F') (hb : AgreeBelow n b b')
  (hA : AgreeBelow n A A')
include hF hb hA

end Locality

/-! ## Generic Γ coefficients: only `F≤3`, `b≤1`, `A≤4` enter -/

/-! ## The eight selected rows and the triangular recursion -/

/-- The eight selected coefficient equations of the actual compactified residual polynomials
(RECURRENCE.md): `PC₁ PM₂ PC₂ PA₂ PA₃ PM₃ PC₃ PA₄ = 0`. -/
structure SelectedRows (h Q J : ℝ) (F b A : ℝ[X]) : Prop where
  C1 : (polyPC h Q J F b A).coeff 1 = 0
  M2 : (polyPM h Q J F b A).coeff 2 = 0
  C2 : (polyPC h Q J F b A).coeff 2 = 0
  A2 : (polyPA h Q J F b A).coeff 2 = 0
  A3 : (polyPA h Q J F b A).coeff 3 = 0
  M3 : (polyPM h Q J F b A).coeff 3 = 0
  C3 : (polyPC h Q J F b A).coeff 3 = 0
  A4 : (polyPA h Q J F b A).coeff 4 = 0

/-! Derived values (outputs of `jet_recursion`; compare RECURRENCE.md). -/
noncomputable def jetB1 (M h _J _Q _c : ℝ) : ℝ := -(M + h) / 2
noncomputable def jetF2 (M h _J Q _c : ℝ) : ℝ := M * (M - h) / 2 + 4 * Q ^ 2 / 3
noncomputable def jetB2 (_M _h _J Q _c : ℝ) : ℝ := 4 * Q ^ 2 / 3
noncomputable def jetA2 (M h J Q c : ℝ) : ℝ := M * c / 6 + h * c / 2 + 2 * J * Q / 3
noncomputable def jetA3 (M h J Q c : ℝ) : ℝ :=
  M ^ 2 * c / 12 + M * h * c / 6 - M * J * Q / 6 + h ^ 2 * c / 4 + 2 * h * J * Q / 3
noncomputable def jetF3 (M h J Q c : ℝ) : ℝ :=
  -M ^ 3 / 6 + M ^ 2 * h / 2 - M * h ^ 2 / 3 - 16 * M * Q ^ 2 / 9 + 4 * h * Q ^ 2 / 3
    + 2 * J ^ 2 / 3 + 4 * c ^ 2 / 9
noncomputable def jetB3 (M h J Q c : ℝ) : ℝ :=
  M ^ 3 / 24 - M * h ^ 2 / 24 - 8 * M * Q ^ 2 / 9 + 2 * h * Q ^ 2 / 3 + 5 * J ^ 2 / 6
    + 2 * c ^ 2 / 9
noncomputable def jetA4 (M h J Q c : ℝ) : ℝ :=
  M ^ 3 * c / 60 + M ^ 2 * h * c / 8 + M ^ 2 * J * Q / 12 + 2 * M * h ^ 2 * c / 15
    - M * h * J * Q / 4 - 34 * M * Q ^ 2 * c / 135 + h ^ 3 * c / 8 + 17 * h ^ 2 * J * Q / 30
    - 7 * J ^ 2 * c / 30 + 8 * J * Q ^ 3 / 135 - 2 * c ^ 3 / 45

/-! ## F1's transcribed jets have exactly these low coefficients -/

/-! ## Connection to F1 and the equation-sourced finite-coefficient obstruction -/

end ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.Compact