-- 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/VII17C6Bridge.lean
-- definition bundle: kept ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.VII17.Df, ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.VII17.Std, ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.VII17.Std.Inv, ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.VII17.Vf, ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.VII17.Wf, ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.VII17.Zf, ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.VII17.rf
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
import Definitions.Def_Atlas_EinsteinMaxwell_ES5_KerrSchild_VII13FiniteBranchSpec
import Definitions.Def_Atlas_EinsteinMaxwell_ES5_KerrSchild_VII16AsymptoticBridge
import Definitions.Def_Atlas_EinsteinMaxwell_ES5_KerrSchild_VII17Algebra
import Definitions.Def_Atlas_EinsteinMaxwell_ES5_KerrSchild_VII17Analysis

/-!
# VII17 — finite `C⁶` bridge for the actual EM value-asymptotic branch (B3 coordinate certificate)

Main theorem `actualC6_of_residuals`: with exactly the inputs of the accepted `VII16R.actualL1_of_residuals`
(actual `PaperData`, `PaperBVP`, real-root branch `FactorizedN`, chart tail, three value-level `O(x²)`
remainder bounds), the actual pull-backs admit a genuine `FiniteBranch6`.

Route (MATHEMATICAL_PREPARATION §§2–4, all on the real residuals): state `Z = uF′/F`, `V = A/x`, `W = bA′`,
`D = (b² − F)/x`, `r = b′/b`. Exact positive-side identities `zf_deriv`, `f_deriv`, `b_deriv` (small root,
branch inequalities derived in `Std.branch`), `maxwell_deriv`, `d_deriv`. Bootstrap invariant `Std.Inv k`
(`F, b, Z ∈ Cᵏ⁺¹`, `V, W, D ∈ Cᵏ`): base from L1 only; step via Hadamard quotients (−1), Maxwell `S`
primitive (+1), Euler gain for `T` and `D + h` (+1), then `F′ = FZ/u`, `b′ = b·rootE`, `Z′ = zrhsE` (+1).
Five steps give `C⁶`; `A′ = W/b` gives `A ∈ C⁶`. Negative-side extensions are re-glued at each stage
(VII16 `glue`) and need not satisfy any ODE.

No derivative limit/bound, `C¹`/`C⁶` extension, formal recursion, `SelectedRows`, `G = 0` or KS conclusion
is a hypothesis. No new black-hole solution; scope: Eq. 33-type first-order value asymptotics only.
-/

namespace ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.VII17

open Filter Set Topology ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.Compact
open scoped ContDiff

/-- Actual state functions on the positive side (`u = 1 - h x`). -/
noncomputable def Zf (h : ℝ) (F : ℝ → ℝ) (x : ℝ) : ℝ := (1 - h * x) * deriv F x / F x
noncomputable def Vf (A : ℝ → ℝ) (x : ℝ) : ℝ := A x / x
noncomputable def Wf (b A : ℝ → ℝ) (x : ℝ) : ℝ := b x * deriv A x
noncomputable def Df (F b : ℝ → ℝ) (x : ℝ) : ℝ := (b x ^ 2 - F x) / x
noncomputable def rf (b : ℝ → ℝ) (x : ℝ) : ℝ := deriv b x / b x

section Pointwise
variable {h Q J x : ℝ} {F b A : ℝ → ℝ}

end Pointwise

/-- Standing data of the abstract bootstrap (all on the positive side, from L1 and the real residuals). -/
structure Std (h Q J f₁ b₁ a₁ : ℝ) (F b A : ℝ → ℝ) : Prop where
  cF : PS F
  cb : PS b
  cA : PS A
  hPF : ∀ᶠ x in 𝓝[>] (0:ℝ), realPF h Q J F b A x = 0
  hPA : ∀ᶠ x in 𝓝[>] (0:ℝ), realPA h Q J F b A x = 0
  hPC : ∀ᶠ x in 𝓝[>] (0:ℝ), realPC h Q J F b A x = 0
  tF : Tendsto F (𝓝[>] (0:ℝ)) (𝓝 1)
  tb : Tendsto b (𝓝[>] (0:ℝ)) (𝓝 1)
  tA : Tendsto A (𝓝[>] (0:ℝ)) (𝓝 0)
  dF : Tendsto (deriv F) (𝓝[>] (0:ℝ)) (𝓝 f₁)
  db : Tendsto (deriv b) (𝓝[>] (0:ℝ)) (𝓝 b₁)
  dA : Tendsto (deriv A) (𝓝[>] (0:ℝ)) (𝓝 a₁)
  rel : f₁ - 2 * b₁ = h

namespace Std
variable {h Q J f₁ b₁ a₁ : ℝ} {F b A : ℝ → ℝ} (S : Std h Q J f₁ b₁ a₁ F b A)
include S

end Std

section Comp
variable {k : ℕ} {h Q J : ℝ} {F b Z V W D r P P₁ P₂ : ℝ → ℝ} {LZ LV LW LD Lr LP L₁ L₂ : ℝ}

end Comp

namespace Std
variable {h Q J f₁ b₁ a₁ : ℝ} {F b A : ℝ → ℝ} (S : Std h Q J f₁ b₁ a₁ F b A)
include S

/-- Bootstrap invariant at stage `k`: `F, b, Z ∈ Cᵏ⁺¹`, `V, W, D ∈ Cᵏ` (independent extensions). -/
def Inv (k : ℕ) : Prop :=
  ExtV (k + 1) F 1 ∧ ExtV (k + 1) b 1 ∧ ExtV (k + 1) (Zf h F) f₁ ∧
    ExtV k (Vf A) a₁ ∧ ExtV k (Wf b A) a₁ ∧ ExtV k (Df F b) (-h)

end Std

end ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.VII17