-- 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/ChargedTail.lean
-- definition bundle: kept ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.NullDirections.alphaCore
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_MaxwellFrame
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

/-!
# VII-06 (F3a, part A): charged-tail nondegeneracy

On the actual `PaperData` + `FactorizedN` + `PaperBVP` branch with the independent VII-05
`SmoothBranch` extension `(F, b, Aext)` and `Q ≠ 0`, the actual `f, m, N` and the actual Maxwell
discriminant `alphaSq` are positive on a smaller radial tail `R > s + δ⁻¹`.

Route: the compact core `alphaCore Q h F b Aext x = Q² F² - x (1 - h x) b F (Aext')²` has no
division at `x = 0`, is continuous there (smoothness of the extensions) and equals `Q²` at `0`. For
`0 < x < ε` the real chart identity `(1 - h x) b(x) alphaSq(s + 1/x) = 4 x³ alphaCore(x)` holds,
obtained from `f = F`, `m = b/x`, `N = (1 - h x)/x²` and `a'(s + 1/x) = -x² Aext'(x)` (open-set
`Set.EqOn.deriv` + the VII-04 real chain rule `deltaFun_pull_a`). No `G = 0`, Kerr–Schild premise,
Taylor expansion or literal `pullM` at `x = 0` is used. Positivity is only eventual: no claim is made
for the whole exterior, and `Q = 0` branches are not covered.
-/

open scoped ContDiff Topology
open ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.Radial
open ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.Compact
open ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.SmoothExt

namespace ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.NullDirections

/-- Compact discriminant core (no division at `x = 0`):
`alphaCore Q h F b A x = Q² F(x)² - x (1 - h x) b(x) F(x) (A'(x))²`. -/
noncomputable def alphaCore (Q h : ℝ) (F b A : ℝ → ℝ) (x : ℝ) : ℝ :=
  Q ^ 2 * F x ^ 2 - x * (1 - h * x) * b x * F x * deriv A x ^ 2

variable {I : Set ℝ} {f m N w p a F b A : ℝ → ℝ} {s h ε Q J : ℝ}

end ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.NullDirections