-- 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/KSBackgroundEnergy.lean
-- definition bundle: kept ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.BackgroundEnergy.EinsteinBackgroundKSTail, ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.BackgroundEnergy.NonposBackgroundKSTail
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_ChargedTail
import Definitions.Def_Atlas_EinsteinMaxwell_ES5_KerrSchild_CompactifiedBridge
import Definitions.Def_Atlas_EinsteinMaxwell_ES5_KerrSchild_CompactifiedResiduals
import Definitions.Def_Atlas_EinsteinMaxwell_ES5_KerrSchild_CoordinateAcceleration
import Definitions.Def_Atlas_EinsteinMaxwell_ES5_KerrSchild_FiniteJetObstruction
import Definitions.Def_Atlas_EinsteinMaxwell_ES5_KerrSchild_FiniteTaylorJet
import Definitions.Def_Atlas_EinsteinMaxwell_ES5_KerrSchild_GeodesicCongruenceObstruction
import Definitions.Def_Atlas_EinsteinMaxwell_ES5_KerrSchild_JetRecursion
import Definitions.Def_Atlas_EinsteinMaxwell_ES5_KerrSchild_KSConnection
import Definitions.Def_Atlas_EinsteinMaxwell_ES5_KerrSchild_KSMetric
import Definitions.Def_Atlas_EinsteinMaxwell_ES5_KerrSchild_KSRicci
import Definitions.Def_Atlas_EinsteinMaxwell_ES5_KerrSchild_MaxwellFrame
import Definitions.Def_Atlas_EinsteinMaxwell_ES5_KerrSchild_NullRicciEnergy
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_PrincipalGeodesic
import Definitions.Def_Atlas_EinsteinMaxwell_ES5_KerrSchild_RadialBVP
import Definitions.Def_Atlas_EinsteinMaxwell_ES5_KerrSchild_RadialBVPEquivalence
import Definitions.Def_Atlas_EinsteinMaxwell_ES5_KerrSchild_RicciNullDirections
import Definitions.Def_Atlas_EinsteinMaxwell_ES5_KerrSchild_ScalarCertificate
import Definitions.Def_Atlas_EinsteinMaxwell_ES5_KerrSchild_SmoothBranch
import Definitions.Def_Atlas_Transport_Connection

/-! # VII-09 (2/3): the same-chart KS background inherits the actual null-Ricci SOS; strictly
positive background contraction arbitrarily far out; nonpositive / Einstein-form backgrounds

Input geometry is the VII-08 raw `KSData gb gbi v K U` (actual background `MetricData`, C∞ profile
and vector, actual background nullity) with the open-set representation
`esMetric … = ksMetric gb v K` on `U ⊆ esDomain I`, and actual `PregeodesicAt gb gbi K`. The
actual candidate inverse is the KS inverse on `U` (`es_inverse_eq_ks`, uniqueness of the
inverse); Ricci tensors are moved only through the open-set locality `ricciOf_congr_of_eqOn`. With
VII-08 `ks_pregeodesic_ricci_contract_eq` this gives

`Ric_gb(K,K) = Ric_gA(K,K)` at every point of `U`,

so on the actual positive charged region the background contraction along **this** `K` equals the
VII-09 weighted sum of squares and is `≥ mu·misalign ≥ 0`. No sign, Ricci-flatness or Einstein
property of the background is assumed; `v` may vanish; `K` may depend on all coordinates.

On the selected branch (`PaperData` + `FactorizedN` + actual `PaperBVP` + `SmoothBranch`,
`J ≠ 0`, `Q ≠ 0`) the VII-08 defect is applied to the **same** data restricted to every farther
tail, so the background contraction is strictly positive at points beyond any cutoff, and (by
continuity on the open KS domain) on a nonempty open five-dimensional set there. This excludes
backgrounds whose contraction along `K` is `≤ 0` on a tail, in particular backgrounds with
pointwise Einstein-form Ricci `R_ij = Λ(x) gb_ij`. Strict positivity is compatible with the null
energy condition; merely asymptotically Einstein backgrounds are not excluded. Same chart only;
the physical candidate keeps `Λ = 0`; no solution is constructed.
-/

open scoped ContDiff Topology Matrix
open ExactVacuumAtlas ExactVacuumAtlas.EinsteinMaxwell ExactVacuumAtlas.EinsteinMaxwell.ES5
open ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.Radial
open ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.Compact
open ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.SmoothExt
open ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.NullDirections
open ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.Geodesic
open ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.Geometry
open ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.NullEnergy
open ExactVacuumAtlas.EinsteinMaxwell.D (einsteinMaxwellD EMCertificateD)

namespace ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.BackgroundEnergy

/-! ## Restriction and continuity helpers -/

section Helpers

variable {gb gbi : Metric 5} {v : Pt 5 → ℝ} {K : Pt 5 → Fin 5 → ℝ} {U V : Set (Pt 5)}

end Helpers

/-! ## Transfer to the background -/

section Transfer

variable {I : Set ℝ} {f m N w p a : ℝ → ℝ} {gb gbi : Metric 5} {v : Pt 5 → ℝ}
  {K : Pt 5 → Fin 5 → ℝ} {U : Set (Pt 5)}

end Transfer

/-! ## Arbitrarily far strictly positive points and open patches -/

section Tail

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

end Tail

/-! ## Nonpositive and Einstein-form backgrounds -/

/-- Same-chart nonzero smooth background-null pregeodesic KS representation of the actual tail
`U_T` whose background Ricci contraction **along its own `K`** is `≤ 0` throughout `U_T`. -/
def NonposBackgroundKSTail (I : Set ℝ) (f m N w : ℝ → ℝ) (T : ℝ) : Prop :=
  ∃ gb gbi : Metric 5, ∃ v : Pt 5 → ℝ, ∃ K : Pt 5 → Fin 5 → ℝ,
    KSData gb gbi v K (esDomain I ∩ {x : Pt 5 | T < x 1}) ∧
    (∀ i j, Set.EqOn (esMetric f (Dfun f m N) (Afun f m) (Hfun m N) w i j) (ksMetric gb v K i j)
      (esDomain I ∩ {x : Pt 5 | T < x 1})) ∧
    (∀ x ∈ esDomain I ∩ {x : Pt 5 | T < x 1}, K x ≠ 0) ∧
    (∀ x ∈ esDomain I ∩ {x : Pt 5 | T < x 1}, PregeodesicAt gb gbi K x) ∧
    ∀ x ∈ esDomain I ∩ {x : Pt 5 | T < x 1}, contract2 (ricciOf gb gbi) x (K x) ≤ 0

/-- Same representation data with a background whose actual Ricci tensor has pointwise
Einstein form `ricciOf gb gbi i j x = Λ x * gb i j x` on `U_T` (`Λ` an arbitrary function; no
constancy, sign or Bianchi argument is used). The candidate itself keeps `Λ = 0`. -/
def EinsteinBackgroundKSTail (I : Set ℝ) (f m N w : ℝ → ℝ) (T : ℝ) : Prop :=
  ∃ gb gbi : Metric 5, ∃ v : Pt 5 → ℝ, ∃ K : Pt 5 → Fin 5 → ℝ, ∃ Λ : Pt 5 → ℝ,
    KSData gb gbi v K (esDomain I ∩ {x : Pt 5 | T < x 1}) ∧
    (∀ i j, Set.EqOn (esMetric f (Dfun f m N) (Afun f m) (Hfun m N) w i j) (ksMetric gb v K i j)
      (esDomain I ∩ {x : Pt 5 | T < x 1})) ∧
    (∀ x ∈ esDomain I ∩ {x : Pt 5 | T < x 1}, K x ≠ 0) ∧
    (∀ x ∈ esDomain I ∩ {x : Pt 5 | T < x 1}, PregeodesicAt gb gbi K x) ∧
    ∀ x ∈ esDomain I ∩ {x : Pt 5 | T < x 1}, ∀ i j, ricciOf gb gbi i j x = Λ x * gb i j x

section Exclusion

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

end Exclusion

/-! ## Own-certificate versions (common `Q, J` extracted by the frozen VII-06 root) -/

section Certificate

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

end Certificate

end ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.BackgroundEnergy