-- 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/FiniteTaylor6.lean
-- definition bundle: kept ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.FiniteRegularity13.cC, ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.FiniteRegularity13.evC, ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.FiniteRegularity13.jC, ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.FiniteRegularity13.matchRingC4, ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.FiniteRegularity13.polC, ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.FiniteRegularity13.th2C, ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.FiniteRegularity13.thC, ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.FiniteRegularity13.xC, ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.FiniteRegularity13.Matches4C4.add, ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.FiniteRegularity13.Matches4C4.mul, ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.FiniteRegularity13.Matches4C4.neg, ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.FiniteRegularity13.c6_deriv, ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.FiniteRegularity13.c6_deriv2, ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.FiniteRegularity13.c6_to_c4, ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.FiniteRegularity13.cda4_lt, ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.FiniteRegularity13.matches4C4_const, ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.FiniteRegularity13.matches4C4_id, ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.FiniteRegularity13.matches4C4_one, ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.FiniteRegularity13.matches4C4_source, ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.FiniteRegularity13.matches4C4_theta2_source, ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.FiniteRegularity13.matches4C4_theta_source, ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.FiniteRegularity13.matches4C4_zero, ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.FiniteRegularity13.tcoef_theta2_fin, ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.FiniteRegularity13.tcoef_theta_fin
import Mathlib
import Definitions.Def_Atlas_Core_Basic
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_Cert
import Definitions.Def_Atlas_EinsteinMaxwell_ES5_Generic_Data
import Definitions.Def_Atlas_EinsteinMaxwell_ES5_Generic_Reduced
import Definitions.Def_Atlas_EinsteinMaxwell_ES5_Generic_Tables
import Definitions.Def_Atlas_EinsteinMaxwell_ES5_KerrSchild_CompactifiedBridge
import Definitions.Def_Atlas_EinsteinMaxwell_ES5_KerrSchild_CompactifiedResiduals
import Definitions.Def_Atlas_EinsteinMaxwell_ES5_KerrSchild_FiniteJetObstruction
import Definitions.Def_Atlas_EinsteinMaxwell_ES5_KerrSchild_FiniteTaylorJet
import Definitions.Def_Atlas_EinsteinMaxwell_ES5_KerrSchild_JetRecursion
import Definitions.Def_Atlas_EinsteinMaxwell_ES5_KerrSchild_OneSidedExtraction
import Definitions.Def_Atlas_EinsteinMaxwell_ES5_KerrSchild_PaperGauge
import Definitions.Def_Atlas_EinsteinMaxwell_ES5_KerrSchild_PolynomialJet
import Definitions.Def_Atlas_EinsteinMaxwell_ES5_KerrSchild_RadialBVP
import Definitions.Def_Atlas_EinsteinMaxwell_ES5_KerrSchild_RadialBVPEquivalence
import Definitions.Def_Atlas_EinsteinMaxwell_ES5_KerrSchild_ScalarCertificate
import Definitions.Def_Atlas_EinsteinMaxwell_ES5_KerrSchild_SmoothBranch
import Definitions.Def_Atlas_EinsteinMaxwell_ES5_KerrSchild_VII13FiniteBranchSpec

/-!
# VII13 support: finite-order Taylor bookkeeping (C⁶ in, C⁴ jets out)

Proof support for `FiniteBranchObstruction.lean`. Everything here uses the genuine
`tcoef g n = iteratedDeriv n g 0 / n!` and `jet4` of `FiniteTaylorJet.lean`; nothing is
redefined. Order ledger (all at the point `0`, or at points of `(-ε, ε)`):

* sources `F b A` are `C⁶`; as atoms they are used at order `C⁴`;
* `θg = x g'` uses `deriv g`, which is `C⁵` (`ContDiffAt.derivWithin`, `5 + 1 ≤ 6`), used at `C⁴`;
* `θ₂g = x² g''` uses `deriv (deriv g)`, which is `C⁴` (`4 + 1 ≤ 5`);
* `Matches4C4` is closed under `+ - *` (a subring), **not** under `θ`: the weighted atoms are
  built directly from the original `C⁶` sources, never by differentiating a `C⁴` match.

No `C^∞`, no old `Matches4`/`matchRing`, no selected-row or coefficient premise is used.
-/

set_option autoImplicit false

open scoped ContDiff Topology
open Polynomial Filter
open ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.Compact
open ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.SmoothExt
open ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.VII13FiniteBranchSpec

namespace ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.FiniteRegularity13

/-! ## Finite order bookkeeping -/

/-- `C⁴` at a point gives every order `n < 5` used by `tcoef`. -/
theorem cda4_lt {g : ℝ → ℝ} {x : ℝ} (hg : ContDiffAt ℝ 4 g x) {n : ℕ} (hn : n < 5) :
    ContDiffAt ℝ n g x :=
  hg.of_le (by exact_mod_cast Nat.lt_succ_iff.mp hn)

/-- `C⁶ → C⁴` for a source function. -/
theorem c6_to_c4 {g : ℝ → ℝ} {x : ℝ} (hg : ContDiffAt ℝ 6 g x) : ContDiffAt ℝ 4 g x :=
  hg.of_le (by norm_num)

/-- `C⁶ g → C⁵ g'` (one derivative costs one order). -/
theorem c6_deriv {g : ℝ → ℝ} {x : ℝ} (hg : ContDiffAt ℝ 6 g x) :
    ContDiffAt ℝ 5 (deriv g) x :=
  hg.derivWithin (by norm_num)

/-- `C⁶ g → C⁴ g''` (two derivatives cost two orders). -/
theorem c6_deriv2 {g : ℝ → ℝ} {x : ℝ} (hg : ContDiffAt ℝ 6 g x) :
    ContDiffAt ℝ 4 (deriv (deriv g)) x :=
  (c6_deriv hg).derivWithin (by norm_num)

/-! ## Finite one-sided extraction -/

/-! ## Weighted Taylor coefficients with explicit finite orders -/

/-- `θ g = x g'`: needs only `C^n` of `deriv g` at `0` for the order-`n` coefficient. -/
theorem tcoef_theta_fin {g : ℝ → ℝ} {n : ℕ} (hd : ContDiffAt ℝ n (deriv g) 0) :
    tcoef (fun x => x * deriv g x) n = n * tcoef g n := by
  have hx : ContDiffAt ℝ n (fun x : ℝ => x) 0 := contDiffAt_id
  rw [tcoef, iteratedDeriv_fun_mul hx hd]
  simp only [iteratedDeriv_fun_id_zero, mul_ite, ite_mul, mul_one, mul_zero, zero_mul,
    Finset.sum_ite_eq', Finset.mem_range]
  rcases n with _ | k
  · simp [tcoef]
  · rw [if_pos (by omega), Nat.choose_one_right, Nat.add_sub_cancel, ← iteratedDeriv_succ', tcoef]
    ring

/-- `θ₂ g = x² g''`: needs only `C^n` of `deriv (deriv g)` at `0`. -/
theorem tcoef_theta2_fin {g : ℝ → ℝ} {n : ℕ} (hd : ContDiffAt ℝ n (deriv (deriv g)) 0) :
    tcoef (fun x => x ^ 2 * deriv (deriv g) x) n = n * (n - 1) * tcoef g n := by
  have hx : ContDiffAt ℝ n (fun x : ℝ => x ^ 2) 0 := contDiffAt_id.pow 2
  rw [tcoef, iteratedDeriv_fun_mul hx hd]
  simp only [iteratedDeriv_fun_pow_zero, Nat.cast_ite, Nat.cast_zero, mul_ite, ite_mul, mul_zero,
    zero_mul, Finset.sum_ite_eq', Finset.mem_range]
  rcases n with _ | _ | k
  · simp [tcoef]
  · simp [tcoef]
  · rw [if_pos (by omega), show k + 1 + 1 - 2 = k by omega, ← iteratedDeriv_succ',
      ← iteratedDeriv_succ', tcoef, Nat.cast_choose ℝ (show 2 ≤ k + 1 + 1 by omega),
      show k + 1 + 1 - 2 = k by omega]
    simp only [Nat.factorial_succ]
    push_cast
    have hk : (k.factorial : ℝ) ≠ 0 := by positivity
    field_simp
    ring

/-! ## `Matches4C4` is closed under `+ - *` (but not under `θ`) -/

theorem matches4C4_const (c : ℝ) : Matches4C4 (fun _ => c) (C c) :=
  ⟨contDiffAt_const, fun n _ => by
    rcases n with _ | n <;> simp [tcoef, iteratedDeriv_const, coeff_C]⟩

theorem matches4C4_id : Matches4C4 (fun x => x) X :=
  ⟨contDiffAt_id, fun n _ => by
    rcases n with _ | _ | n <;> simp [tcoef, iteratedDeriv_fun_id_zero, coeff_X]⟩

theorem matches4C4_one : Matches4C4 1 1 := by
  have h := matches4C4_const (1 : ℝ); rw [map_one] at h; exact h

theorem matches4C4_zero : Matches4C4 0 0 := by
  have h := matches4C4_const (0 : ℝ); rw [map_zero] at h; exact h

theorem Matches4C4.add {g h : ℝ → ℝ} {p q : ℝ[X]} (hg : Matches4C4 g p) (hh : Matches4C4 h q) :
    Matches4C4 (g + h) (p + q) :=
  ⟨hg.1.add hh.1, fun n hn => by
    rw [tcoef, iteratedDeriv_add (cda4_lt hg.1 hn) (cda4_lt hh.1 hn), add_div, coeff_add,
      ← tcoef, ← tcoef, hg.2 n hn, hh.2 n hn]⟩

theorem Matches4C4.neg {g : ℝ → ℝ} {p : ℝ[X]} (hg : Matches4C4 g p) : Matches4C4 (-g) (-p) :=
  ⟨hg.1.neg, fun n hn => by rw [tcoef, iteratedDeriv_neg, neg_div, coeff_neg, ← tcoef, hg.2 n hn]⟩

theorem Matches4C4.mul {g h : ℝ → ℝ} {p q : ℝ[X]} (hg : Matches4C4 g p) (hh : Matches4C4 h q) :
    Matches4C4 (g * h) (p * q) :=
  ⟨hg.1.mul hh.1, fun n hn => by
    rw [tcoef_mul (cda4_lt hg.1 hn) (cda4_lt hh.1 hn), coeff_mul,
      Finset.Nat.sum_antidiagonal_eq_sum_range_succ_mk]
    refine Finset.sum_congr rfl fun i hi => ?_
    have hin : i ≤ n := Nat.lt_succ_iff.mp (Finset.mem_range.mp hi)
    rw [hg.2 i (by omega), hh.2 (n - i) (by omega)]⟩

/-- Finite `C⁴` matching pairs form a subring of `(ℝ → ℝ) × ℝ[X]`. -/
def matchRingC4 : Subring ((ℝ → ℝ) × ℝ[X]) where
  carrier := {q | Matches4C4 q.1 q.2}
  mul_mem' := fun ha hb => Matches4C4.mul ha hb
  one_mem' := show Matches4C4 (1 : ℝ → ℝ) (1 : ℝ[X]) from matches4C4_one
  add_mem' := fun ha hb => Matches4C4.add ha hb
  zero_mem' := show Matches4C4 (0 : ℝ → ℝ) (0 : ℝ[X]) from matches4C4_zero
  neg_mem' := fun ha => Matches4C4.neg ha

/-! ## Atoms built directly from `C⁶` sources (orders recorded per atom) -/

/-- Source atom `(g, jet4 g)`: `C⁶ → C⁴`. -/
theorem matches4C4_source {g : ℝ → ℝ} (hg : ContDiffAt ℝ 6 g 0) : Matches4C4 g (jet4 g) :=
  ⟨c6_to_c4 hg, fun _ hn => (coeff_jet4_of_lt g hn).symm⟩

/-- Weighted atom `(x g', thetaP (jet4 g))`: uses `g' ∈ C⁵` (from `g ∈ C⁶`), at order `C⁴`. -/
theorem matches4C4_theta_source {g : ℝ → ℝ} (hg : ContDiffAt ℝ 6 g 0) :
    Matches4C4 (fun x => x * deriv g x) (thetaP (jet4 g)) := by
  have hd : ContDiffAt ℝ 4 (deriv g) 0 := (c6_deriv hg).of_le (by norm_num)
  exact ⟨contDiffAt_id.mul hd, fun n hn => by
    rw [tcoef_theta_fin (cda4_lt hd hn), coeff_thetaP, coeff_jet4_of_lt g hn]⟩

/-- Weighted atom `(x² g'', theta2P (jet4 g))`: uses `g'' ∈ C⁴` (from `g ∈ C⁶`). -/
theorem matches4C4_theta2_source {g : ℝ → ℝ} (hg : ContDiffAt ℝ 6 g 0) :
    Matches4C4 (fun x => x ^ 2 * deriv (deriv g) x) (theta2P (jet4 g)) := by
  have hd : ContDiffAt ℝ 4 (deriv (deriv g)) 0 := c6_deriv2 hg
  exact ⟨(contDiffAt_id.pow 2).mul hd, fun n hn => by
    rw [tcoef_theta2_fin (cda4_lt hd hn), coeff_theta2P, coeff_jet4_of_lt g hn]⟩

/-- `(x, X)`. -/
noncomputable def xC : matchRingC4 := ⟨(fun x => x, X), matches4C4_id⟩
/-- `(c, C c)`. -/
noncomputable def cC (c : ℝ) : matchRingC4 := ⟨(fun _ => c, C c), matches4C4_const c⟩
/-- `(g, jet4 g)` for a `C⁶` source. -/
noncomputable def jC {g : ℝ → ℝ} (hg : ContDiffAt ℝ 6 g 0) : matchRingC4 :=
  ⟨(g, jet4 g), matches4C4_source hg⟩
/-- `(x g', thetaP (jet4 g))` for a `C⁶` source. -/
noncomputable def thC {g : ℝ → ℝ} (hg : ContDiffAt ℝ 6 g 0) : matchRingC4 :=
  ⟨(fun x => x * deriv g x, thetaP (jet4 g)), matches4C4_theta_source hg⟩
/-- `(x² g'', theta2P (jet4 g))` for a `C⁶` source. -/
noncomputable def th2C {g : ℝ → ℝ} (hg : ContDiffAt ℝ 6 g 0) : matchRingC4 :=
  ⟨(fun x => x ^ 2 * deriv (deriv g) x, theta2P (jet4 g)), matches4C4_theta2_source hg⟩

/-- Evaluation of the function component at `x`. -/
noncomputable def evC (x : ℝ) : matchRingC4 →+* ℝ :=
  (Pi.evalRingHom (fun _ : ℝ => ℝ) x).comp ((RingHom.fst (ℝ → ℝ) ℝ[X]).comp matchRingC4.subtype)
/-- The polynomial component. -/
noncomputable def polC : matchRingC4 →+* ℝ[X] :=
  (RingHom.snd (ℝ → ℝ) ℝ[X]).comp matchRingC4.subtype

/-! ## Actual residuals and core: finite `C⁴` matches from `C⁶` sources -/

section Residuals

variable {F b A : ℝ → ℝ} (hF : ContDiffAt ℝ 6 F 0) (hb : ContDiffAt ℝ 6 b 0)
  (hA : ContDiffAt ℝ 6 A 0) (h Q J : ℝ)
include hF hb hA

end Residuals

/-! ## From `C⁶` on `(-ε, ε)` and actual positive-side vanishing to coefficient conditions -/

section Extraction

variable {ε h Q J : ℝ} {F b A : ℝ → ℝ}

end Extraction

end ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.FiniteRegularity13