Atlas VII definitions: VII13FiniteBranchSpec

-- 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/VII13FiniteBranchSpec.lean
-- definition bundle: kept ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.VII13FiniteBranchSpec.CompactFiniteObstructionOutput, ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.VII13FiniteBranchSpec.FiniteBranch6, ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.VII13FiniteBranchSpec.FiniteJetOutput, ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.VII13FiniteBranchSpec.Matches4C4, ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.VII13FiniteBranchSpec.RadialFiniteJetOutput, ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.VII13FiniteBranchSpec.RadialFiniteObstructionOutput
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

/-!
VII13 fixed specification: finite C6 inverse-radius regularity suffices for the genuine
Taylor4 recursion and the explicit-G obstruction. Prepared without local Lean.

Canonical destination: Atlas/EinsteinMaxwell/ES5/KerrSchild/VII13FiniteBranchSpec.lean
Proof support: FiniteTaylor6.lean; proof roots: FiniteBranchObstruction.lean.
All previously accepted 48 mathematical sources stay unchanged.

FiniteBranch6 is a genuine independent regularity INPUT. It retains all11 fields of the
old SmoothBranch, replacing only the three ContDiffOn orders infinity by6. PaperData is
unchanged at finite radii. Matches4C4 is an ordinary finite-jet mathematical relation;
the remaining definitions are transparent OUTPUT propositions, never root premises.
No AF=>C6, optimal-order, analyticity, KS or black-hole nonexistence claim is made.
-/

set_option autoImplicit false

open scoped ContDiff
open Polynomial
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.SmoothExt.Controls: no listed name exists here)

namespace ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.VII13FiniteBranchSpec

/-- Raw independent finite-regularity extension. No residual, G, charge, rotation,
coefficient or C-infinity premise is hidden in this actual input structure. -/
structure FiniteBranch6 (I : Set ℝ) (s ε : ℝ) (f m a F b A : ℝ → ℝ) : Prop where
  eps_pos : 0 < ε
  chart_tail : Set.Ioi (s + ε⁻¹) ⊆ I
  cF : ContDiffOn ℝ 6 F (Set.Ioo (-ε) ε)
  cb : ContDiffOn ℝ 6 b (Set.Ioo (-ε) ε)
  cA : ContDiffOn ℝ 6 A (Set.Ioo (-ε) ε)
  matchF : Set.EqOn F (pull s f) (Set.Ioo 0 ε)
  matchb : Set.EqOn b (pullM s m) (Set.Ioo 0 ε)
  matchA : Set.EqOn A (pull s a) (Set.Ioo 0 ε)
  F0 : F 0 = 1
  b0 : b 0 = 1
  A0 : A 0 = 0

/-- Finite C4 matching of genuine derivatives to an actual polynomial below degree5.
This replaces neither tcoef/jet4 nor the old C-infinity Matches4 relation. -/
def Matches4C4 (g : ℝ → ℝ) (P : ℝ[X]) : Prop :=
  ContDiffAt ℝ 4 g 0 ∧ ∀ n < 5, tcoef g n = P.coeff n

/-- Complete finite-jet output: actual residual/core C4 matches, genuine normalization,
all eight derived selected rows, eight Taylor recursion values and Γ6..8 comparison.
SelectedRows is a conclusion derived from positive-side actual residual vanishing. -/
def FiniteJetOutput (h Q J : ℝ) (F b A : ℝ → ℝ) : Prop :=
  Matches4C4 (realPM h Q J F b A) (polyPM h Q J (jet4 F) (jet4 b) (jet4 A)) ∧
    Matches4C4 (realPA h Q J F b A) (polyPA h Q J (jet4 F) (jet4 b) (jet4 A)) ∧
    Matches4C4 (realPC h Q J F b A) (polyPC h Q J (jet4 F) (jet4 b) (jet4 A)) ∧
    Matches4C4 (realCore h Q J F b A) (gammaCore h Q J (jet4 F) (jet4 b) (jet4 A)) ∧
    JetNormalization (massLabel F) (magneticLabel A) (jet4 F) (jet4 b) (jet4 A) ∧
    SelectedRows h Q J (jet4 F) (jet4 b) (jet4 A) ∧
    (tcoef b 1 = jetB1 (massLabel F) h J Q (magneticLabel A) ∧
      tcoef F 2 = jetF2 (massLabel F) h J Q (magneticLabel A) ∧
      tcoef b 2 = jetB2 (massLabel F) h J Q (magneticLabel A) ∧
      tcoef A 2 = jetA2 (massLabel F) h J Q (magneticLabel A) ∧
      tcoef A 3 = jetA3 (massLabel F) h J Q (magneticLabel A) ∧
      tcoef F 3 = jetF3 (massLabel F) h J Q (magneticLabel A) ∧
      tcoef b 3 = jetB3 (massLabel F) h J Q (magneticLabel A) ∧
      tcoef A 4 = jetA4 (massLabel F) h J Q (magneticLabel A)) ∧
    ((gammaGen h Q J (jet4 F) (jet4 b) (jet4 A)).coeff 6 =
        (FiniteJet.gammaJet (massLabel F) h J Q (magneticLabel A)).coeff 6 ∧
      (gammaGen h Q J (jet4 F) (jet4 b) (jet4 A)).coeff 7 =
        (FiniteJet.gammaJet (massLabel F) h J Q (magneticLabel A)).coeff 7 ∧
      (gammaGen h Q J (jet4 F) (jet4 b) (jet4 A)).coeff 8 =
        (FiniteJet.gammaJet (massLabel F) h J Q (magneticLabel A)).coeff 8)

/-- Actual Γ=0 is an extra compact-root hypothesis. Its consequences include core=0
on the positive interval, the three actual jet-Γ coefficients, and the charge/rotation
product obstruction. Division by x^4 is permitted only for x>0. -/
def CompactFiniteObstructionOutput (ε h Q J : ℝ) (F b A : ℝ → ℝ) : Prop :=
  FiniteJetOutput h Q J F b A ∧
    (∀ x ∈ Set.Ioo 0 ε, realCore h Q J F b A x = 0) ∧
    (gammaGen h Q J (jet4 F) (jet4 b) (jet4 A)).coeff 6 = 0 ∧
    (gammaGen h Q J (jet4 F) (jet4 b) (jet4 A)).coeff 7 = 0 ∧
    (gammaGen h Q J (jet4 F) (jet4 b) (jet4 A)).coeff 8 = 0 ∧
    J ^ 3 * Q ^ 5 = 0 ∧ (J = 0 ∨ Q = 0)

/-- The actual PaperBVP supplies all three real residual equations; no selected-row or
desired recursion condition is an input to the radial root. -/
def RadialFiniteJetOutput (ε h Q J : ℝ) (F b A : ℝ → ℝ) : Prop :=
  (∀ x ∈ Set.Ioo 0 ε, realPM h Q J F b A x = 0) ∧
    (∀ x ∈ Set.Ioo 0 ε, realPA h Q J F b A x = 0) ∧
    (∀ x ∈ Set.Ioo 0 ε, realPC h Q J F b A x = 0) ∧
    FiniteJetOutput h Q J F b A

/-- Explicit G=0 on the actual chart tail is required by the radial obstruction root.
The actual compact Γ equation and complete finite obstruction are derived outputs. -/
def RadialFiniteObstructionOutput (ε h Q J : ℝ) (F b A : ℝ → ℝ) : Prop :=
  RadialFiniteJetOutput ε h Q J F b A ∧
    (∀ x ∈ Set.Ioo 0 ε, realGamma h Q J F b A x = 0) ∧
    CompactFiniteObstructionOutput ε h Q J F b A

end ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.VII13FiniteBranchSpec