Atlas VII definitions: VII14FiniteKSSpec

-- 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/VII14FiniteKSSpec.lean
-- definition bundle: kept ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.VII14FiniteKSSpec.BackgroundPositiveOutput, ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.VII14FiniteKSSpec.ChargedTailOutput, ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.VII14FiniteKSSpec.GeneralPositiveFamily, ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.VII14FiniteKSSpec.NoCongruenceOutput, ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.VII14FiniteKSSpec.OwnFiniteKSOutput, ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.VII14FiniteKSSpec.PrincipalDefectOutput
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_FiniteTaylor6
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_KSBackgroundEnergy
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_EinsteinMaxwell_ES5_KerrSchild_VII13FiniteBranchSpec
import Definitions.Def_Atlas_Transport_Connection

/-!
VII14 fixed OUTPUT specification: the accepted finite C6 infinity branch reaches the
general same-chart Kerr-Schild obstruction and actual background positive witnesses.
Prepared without local Lean; no kernel receipt is claimed.

Canonical destination: Atlas/EinsteinMaxwell/ES5/KerrSchild/VII14FiniteKSSpec.lean
Proof support: FiniteChargedTail.lean; proof roots: FiniteKSObstruction.lean.
All previously accepted 51 mathematical sources remain unchanged.

All seven new definitions below are transparent output propositions. The independent
FiniteBranch6 input is reused unchanged from VII13. Finite-radius PaperData and all local
KSData smoothness are unchanged. General roots do not assume G=0, principal alignment,
co-rotating-plane membership or a normalized field. No AF=>C6, cross-chart, global-solution
or general five-dimensional black-hole nonexistence claim is made.
-/

set_option autoImplicit false

open scoped ContDiff Topology Matrix
open ExactVacuumAtlas ExactVacuumAtlas.EinsteinMaxwell ExactVacuumAtlas.EinsteinMaxwell.ES5
open ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.Radial
open ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.NullDirections
open ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.NullEnergy
open ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.Geodesic
open ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.Geometry
open ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.BackgroundEnergy
-- (open ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.SmoothExt.Controls: no listed name exists here)
open ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.VII13FiniteBranchSpec (FiniteBranch6)

namespace ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.VII14FiniteKSSpec

/-- Weak charged-tail output, with no rotation, G or KS premise. -/
def ChargedTailOutput (I : Set ℝ) (s ε : ℝ) (f m N w p a : ℝ → ℝ) : Prop :=
  ∃ δ : ℝ, 0 < δ ∧ δ ≤ ε ∧ ∀ R : ℝ, s + δ⁻¹ < R →
    R ∈ I ∧ 0 < f R ∧ 0 < m R ∧ 0 < N R ∧ 0 < alphaSq f m N w p a R

/-- Arbitrarily-far actual G defect and failure of both actual principal fields to be
pregeodesic there. This does not assert positivity for every pointwise vector at that R. -/
def PrincipalDefectOutput (I : Set ℝ) (f m N w p a : ℝ → ℝ) : Prop :=
  ∀ B : ℝ, ∃ R : ℝ, B < R ∧ R ∈ I ∧ Gfun p a R ≠ 0 ∧
    ∀ x : Pt 5, x 1 = R → 0 < x 2 → x 2 < 1 →
      ¬ PregeodesicAt (esMetric f (Dfun f m N) (Afun f m) (Hfun m N) w)
        (esInverse f (Dfun f m N) (Afun f m) (Hfun m N) w) (kPlus f m N w p a) x ∧
      ¬ PregeodesicAt (esMetric f (Dfun f m N) (Afun f m) (Hfun m N) w)
        (esInverse f (Dfun f m N) (Afun f m) (Hfun m N) w) (kMinus f m N w p a) x

/-- No distant actual candidate tail carries a C1 nonzero/null/Ricci-null/pregeodesic
field. Ricci-nullity is not assumed by the later general-background positive root. -/
def NoCongruenceOutput (I : Set ℝ) (f m N w : ℝ → ℝ) : Prop :=
  ¬ ∃ T : ℝ, ∃ V : Pt 5 → Fin 5 → ℝ,
    RicciNullPregeodesicField (esMetric f (Dfun f m N) (Afun f m) (Hfun m N) w)
      (esInverse f (Dfun f m N) (Afun f m) (Hfun m N) w)
      (esDomain I ∩ {x : Pt 5 | T < x 1}) V

/-- Positive witnesses for the actual given background and K, fixed before every cutoff.
The point/patch may depend on those data and the cutoff; no uniform or whole-tail
strict lower bound is asserted. -/
def BackgroundPositiveOutput (I : Set ℝ) (f m N w p a : ℝ → ℝ) (T : ℝ)
    (gb gbi : Metric 5) (K : Pt 5 → Fin 5 → ℝ) : Prop :=
  let U := esDomain I ∩ {x : Pt 5 | T < x 1}
  (∀ B : ℝ, ∃ x ∈ U, B < x 1 ∧
    0 < contract2 (ricciOf gb gbi) x (K x) ∧ 0 < misalign f m N w p a x (K x) ∧
    ¬ ∃ t : ℝ, K x = t • kPlus f m N w p a x ∨ K x = t • kMinus f m N w p a x) ∧
  (∀ B : ℝ, ∃ V : Set (Pt 5), IsOpen V ∧ V.Nonempty ∧
    V ⊆ U ∩ {x : Pt 5 | B < x 1} ∧
    ∀ x ∈ V, 0 < contract2 (ricciOf gb gbi) x (K x))

/-- Full arbitrary-K family, with the same old raw KSData, actual representation,
nonzero field and background pregeodesicity. No plane, rescaling or curvature-sign input. -/
def GeneralPositiveFamily (I : Set ℝ) (f m N w p a : ℝ → ℝ) : Prop :=
  ∀ (T : ℝ) (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) →
    BackgroundPositiveOutput I f m N w p a T gb gbi K

/-- The candidate's own certificate yields one common actual Q/J pair and BVP, with
the complete finite-branch tail, principal defect, no-congruence, general-background
positive family and nonpositive/Einstein-form exclusions. -/
def OwnFiniteKSOutput (I : Set ℝ) (f m N w p a : ℝ → ℝ) (r₀ s ε : ℝ) : Prop :=
  ∃ Q J : ℝ, Q = -qFun f N w p a r₀ ∧ J = -ellFun f m N w p a r₀ / 2 ∧
    PaperBVP I f m N w p a Q J ∧ Q ≠ 0 ∧ J ≠ 0 ∧
    ChargedTailOutput I s ε f m N w p a ∧
    PrincipalDefectOutput I f m N w p a ∧ NoCongruenceOutput I f m N w ∧
    GeneralPositiveFamily I f m N w p a ∧
    (¬ ∃ T : ℝ, NonposBackgroundKSTail I f m N w T) ∧
    (¬ ∃ T : ℝ, EinsteinBackgroundKSTail I f m N w T)

end ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.VII14FiniteKSSpec