-- 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/VII16AsymptoticBridge.lean
-- definition bundle: kept ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.VII16.flatExt, ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.VII16.glue, ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.VII16.taylorPoly
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

/-!
# VII16 — the finite asymptotic bridge (sufficiency direction)

Real germs on `(0, ε)` whose iterated derivatives `0 … n` have finite right limits at the
origin. Glue the negative side to the Taylor polynomial of those limits. The result is a
genuine `Cⁿ` function on `(-ε, ε)` agreeing with the germ on the positive side — exactly the
regularity interface `FiniteBranch6` needs.

**The derivative limits are an INPUT.** `notes/VII16_ASYMPTOTIC_ANALYSIS.md` records that the
paper's §3.1 supplies value-level asymptotics (Eq. 30/33) and a *chosen* formal integer-power
series (Eq. 32/36), not derivative asymptotics. The converse (paper branch ⇒ these limits) is
not established in this round, so the original goal stays conditional.
-/

open Filter Set
open scoped Topology ContDiff
open ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.Compact (pull pullM)
open ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.VII13FiniteBranchSpec (FiniteBranch6)
-- (open ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.SmoothExt.Controls: no listed name exists here)
-- (open ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.Radial: no listed name exists here)

namespace ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.VII16

/-! ## Negative-side Taylor polynomial -/

/-- Negative-side Taylor polynomial with prescribed jet `L`. -/
noncomputable def taylorPoly (L : ℕ → ℝ) (n : ℕ) : ℝ → ℝ :=
  fun x => ∑ k ∈ Finset.range (n + 1), L k / (k.factorial : ℝ) * x ^ k

/-! ## The flat extension -/

/-- Extend a function on `(0, ε)` by zero to the left of the origin. -/
noncomputable def flatExt (h : ℝ → ℝ) : ℝ → ℝ := fun x => if 0 < x then h x else 0

/-! ## Continuity -/

/-! ## Derivative at the origin and the derivative identity -/

end ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.VII16

namespace ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.VII16

/-! ## The Cⁿ induction -/

end ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.VII16

namespace ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.VII16

/-! ## The glued germ: polynomial on the left, the actual germ on the right -/

/-- Glue: Taylor polynomial below `0`, the actual germ above. Written as polynomial plus a
flat correction so that the flat-extension theory applies unchanged. -/
noncomputable def glue (L : ℕ → ℝ) (n : ℕ) (g : ℝ → ℝ) : ℝ → ℝ :=
  fun x => taylorPoly L n x + flatExt (fun y => g y - taylorPoly L n y) x

end ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.VII16

namespace ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.VII16

/-! ## From derivative limits to the `C⁶` gluing -/

end ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.VII16

namespace ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.VII16

/-! ## One-sided C⁶ germs of the actual pull-backs -/

/-! ## The main assembly -/

end ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.VII16

namespace ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.VII16

/-! ## Negative control: value asymptotics do not give derivative control

`x ↦ 1 + x⁷ sin((x⁸)⁻¹)` on `(0, ∞)` has value remainder `O(x⁷)`: **every** value coefficient
below order 7 is that of the constant `1`. Its actual derivative, however, is
`7x⁶ sin(x⁻⁸) − 8x⁻² cos(x⁻⁸)` (the outer `x⁷` cancels one power of `x` in `x¹⁴/x¹⁶`), whose
second term grows like `x⁻²` and oscillates in sign, so the derivative has no finite right limit
at `0⁺`. The no-limit conclusion itself is an analysis argument (`notes/VII16_ASYMPTOTIC_ANALYSIS.md`
§6); only the two algebraic facts above are formalised in Lean.

This function is **not** an Einstein–Maxwell solution. It refutes only the inference
"value expansion ⇒ differentiable control", which is precisely the inference the paper's
Eq. (30)/(33) do not license and which `FiniteBranch6` requires. -/

end ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.VII16

namespace ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.VII16

/-! ## Positive control: the real RN branch through the new bridge

Reissner–Nordström with `Q = 3/4`, `J = 0`. The extension `rnExtF`, `rnExtb` is a *ratio of
polynomials*, so its iterated derivatives at the origin exist and are given by the rational
function itself; the derivative limits required by `finiteBranch6_of_deriv_limits` are therefore
discharged **from the actual pull-backs**, not assumed as a `FiniteBranch6` premise. -/

end ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.VII16

namespace ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.VII16

end ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.VII16