-- 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/OneSidedExtraction.lean
-- definition bundle: kept ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.SmoothExt.realCore
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_FiniteTaylorJet
import Definitions.Def_Atlas_EinsteinMaxwell_ES5_KerrSchild_JetRecursion
import Definitions.Def_Atlas_EinsteinMaxwell_ES5_KerrSchild_PolynomialJet
import Definitions.Def_Atlas_EinsteinMaxwell_ES5_KerrSchild_ScalarCertificate

/-! # VII-05 (F2c2): right-side vanishing ⇒ finite coefficient conditions

1. **One-sided zero lemma.** If `g` is `C^∞` at `0` and `g = 0` on `(0, ε)`, then every
   `iteratedDeriv k g 0 = 0`: first `iteratedDeriv k g = 0` on the open set `(0, ε)`
   (`Set.EqOn.iteratedDeriv_of_isOpen`), then the value at `0` is the limit along `𝓝[>] 0`
   of a function continuous at `0` (`tendsto_nhds_unique`). Only right-side equality is used;
   nothing is assumed on `(-ε, 0)`, and a single value `g(0) = 0` is never used to kill
   derivatives (controls in `SmoothBranchControls.lean`).
2. **Actual residuals match the actual residual polynomials below degree five.** Through the
   VII-04 weighted bodies (`pcE_eq_pcW`, `polyPC_eq`) and the subring `matchRing`, the real
   `realPC h Q J F b A` matches `polyPC h Q J (jet4 F) (jet4 b) (jet4 A)` (same for `PM`, `PA`).
3. **Γ through its fourth-order core.** `realCore` is the real-function instance of the
   `gammaCore` body (`coreE`); on any point where `F` and `A'` are differentiable,
   `realGamma = x⁴ · realCore` (genuine `HasDerivAt` for `δ(δA)` and `δ(x² F)`). Division by
   `x⁴` happens only for `x > 0`.

Consequences: right-side vanishing of `realPM realPA realPC` gives the eight VII-04
`SelectedRows` for `jet4 F, jet4 b, jet4 A`; right-side vanishing of `realGamma` gives
`gammaGen` coefficients 6, 7, 8 zero. The two sources are kept separate. -/

open Polynomial Filter Topology
open scoped ContDiff

namespace ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.SmoothExt

open ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.Compact

/-! ## One-sided zero ⇒ zero jet -/

/-! ## Weighted atoms as matching pairs -/

/-! ## The actual residuals match the actual residual polynomials -/

section Residuals

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

end Residuals

/-! ## The real Γ core -/

/-- Real-function instance of the `gammaCore` body: atoms `θg = x g'`, `θ₂g = x² g''`. -/
noncomputable def realCore (h Q J : ℝ) (F b A : ℝ → ℝ) (x : ℝ) : ℝ :=
  coreE x (1 - h * x) h Q J (F x) (x * deriv F x) (b x) (A x) (x * deriv A x)
    (x ^ 2 * deriv (deriv A) x)

/-! ## Right-side vanishing ⇒ the finite coefficient conditions -/

section Extraction

variable {ε h Q J : ℝ} {F b A : ℝ → ℝ} (hε : 0 < ε)
  (cF : ContDiffOn ℝ ∞ F (Set.Ioo (-ε) ε)) (cb : ContDiffOn ℝ ∞ b (Set.Ioo (-ε) ε))
  (cA : ContDiffOn ℝ ∞ A (Set.Ioo (-ε) ε))
include hε

include cF cb cA

end Extraction

end ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.SmoothExt