Atlas VII definitions: FiniteTaylorJet
DefinitionAtlas_EinsteinMaxwell_ES5_KerrSchild_FiniteTaylorJetDefinitions of the Atlas VII module Atlas.EinsteinMaxwell.ES5.KerrSchild.FiniteTaylorJet (kept exactly as in the accepted source, skeleton subtraction).
VII-05 (F2c2): finite Taylor-4 jets of genuine real functions at x = 0
For g : ℝ → ℝ the genuine Taylor coefficients at zero are tcoef g n = g⁽ⁿ⁾(0)/n!
(iteratedDeriv), and jet4 g = ∑_{n ≤ 4} tcoef g n · Xⁿ.
jet4 is not a ring homomorphism into Polynomial ℝ: products of jets have coefficients of
degree 5–8 that jet4 of the product does not see (jet4_mul_counterexample). The only claim
is compatibility below degree five, packaged as the relation Matches4 g p (g is C^∞ at
0 and tcoef g n = p.coeff n for n < 5) and the subring matchRing of
(ℝ → ℝ) × ℝ[X] of matching pairs: sums, negatives and products (genuine Leibniz rule
iteratedDeriv_mul, factorial cancellation) stay matching. No quotient ring, power series or
general asymptotic library is introduced. The weighted operators θ g = x g', θ₂ g = x² g''
match thetaP, theta2P of VII-04 (tcoef (θ g) n = n · tcoef g n,
tcoef (θ₂ g) n = n (n - 1) · tcoef g n); note theta2P p = X² p'' contains no 2 X p'.
coreE is the commutative-ring body of VII-04's gammaCore (gammaCore_eq_coreE).
Constants in this bundle: coreE, jet4, tcoef, coeff_jet4, coeff_jet4_of_lt, tcoef_mul.
Registered B3 definition layer (Mathlib at the pinned revision has no Lorentzian metric / Ricci API): mission/PHYSICS_BOUNDARY.md, Atlas VII sections P–XVII.
-- 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/FiniteTaylorJet.lean
-- definition bundle: kept ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.SmoothExt.coreE, ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.SmoothExt.jet4, ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.SmoothExt.tcoef, ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.SmoothExt.coeff_jet4, ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.SmoothExt.coeff_jet4_of_lt, ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.SmoothExt.tcoef_mul
import Mathlib
import Definitions.Def_Atlas_EinsteinMaxwell_ES5_KerrSchild_CompactifiedResiduals
import Definitions.Def_Atlas_EinsteinMaxwell_ES5_KerrSchild_FiniteJetObstruction
import Definitions.Def_Atlas_EinsteinMaxwell_ES5_KerrSchild_JetRecursion
import Definitions.Def_Atlas_EinsteinMaxwell_ES5_KerrSchild_PolynomialJet
import Definitions.Def_Atlas_EinsteinMaxwell_ES5_KerrSchild_ScalarCertificate
/-! # VII-05 (F2c2): finite Taylor-4 jets of genuine real functions at `x = 0`
For `g : ℝ → ℝ` the genuine Taylor coefficients at zero are `tcoef g n = g⁽ⁿ⁾(0)/n!`
(`iteratedDeriv`), and `jet4 g = ∑_{n ≤ 4} tcoef g n · Xⁿ`.
`jet4` is **not** a ring homomorphism into `Polynomial ℝ`: products of jets have coefficients of
degree 5–8 that `jet4` of the product does not see (`jet4_mul_counterexample`). The only claim
is compatibility below degree five, packaged as the relation `Matches4 g p` (`g` is `C^∞` at
`0` and `tcoef g n = p.coeff n` for `n < 5`) and the subring `matchRing` of
`(ℝ → ℝ) × ℝ[X]` of matching pairs: sums, negatives and products (genuine Leibniz rule
`iteratedDeriv_mul`, factorial cancellation) stay matching. No quotient ring, power series or
general asymptotic library is introduced. The weighted operators `θ g = x g'`, `θ₂ g = x² g''`
match `thetaP`, `theta2P` of VII-04 (`tcoef (θ g) n = n · tcoef g n`,
`tcoef (θ₂ g) n = n (n - 1) · tcoef g n`); note `theta2P p = X² p''` contains no `2 X p'`.
`coreE` is the commutative-ring body of VII-04's `gammaCore` (`gammaCore_eq_coreE`). -/
open Polynomial
open scoped ContDiff
namespace ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.SmoothExt
open ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.Compact
/-! ## Genuine Taylor coefficients and the degree-4 jet -/
/-- `g⁽ⁿ⁾(0) / n!` with the genuine iterated derivative. -/
noncomputable def tcoef (g : ℝ → ℝ) (n : ℕ) : ℝ := iteratedDeriv n g 0 / (n.factorial : ℝ)
/-- `∑_{n ≤ 4} tcoef g n · Xⁿ`. Multiplication is compatible only below degree five. -/
noncomputable def jet4 (g : ℝ → ℝ) : ℝ[X] := ∑ k ∈ Finset.range 5, C (tcoef g k) * X ^ k
theorem coeff_jet4 (g : ℝ → ℝ) (n : ℕ) :
(jet4 g).coeff n = if n < 5 then tcoef g n else 0 := by
simp only [jet4, finsetSum_coeff, coeff_C_mul_X_pow, Finset.sum_ite_eq, Finset.mem_range]
theorem coeff_jet4_of_lt (g : ℝ → ℝ) {n : ℕ} (hn : n < 5) : (jet4 g).coeff n = tcoef g n := by
rw [coeff_jet4, if_pos hn]
/-! ## Order bookkeeping for `C^∞` at a point -/
/-! ## Leibniz rule for normalised coefficients -/
theorem tcoef_mul {g h : ℝ → ℝ} {n : ℕ} (hg : ContDiffAt ℝ n g 0) (hh : ContDiffAt ℝ n h 0) :
tcoef (g * h) n = ∑ i ∈ Finset.range (n + 1), tcoef g i * tcoef h (n - i) := by
rw [tcoef, iteratedDeriv_mul hg hh, div_eq_mul_inv, Finset.sum_mul]
refine Finset.sum_congr rfl fun i hi => ?_
have hin : i ≤ n := Nat.lt_succ_iff.mp (Finset.mem_range.mp hi)
rw [tcoef, tcoef, Nat.cast_choose ℝ hin]
have h1 : (i.factorial : ℝ) ≠ 0 := by positivity
have h2 : ((n - i).factorial : ℝ) ≠ 0 := by positivity
have h3 : (n.factorial : ℝ) ≠ 0 := by positivity
field_simp
/-! ## The matching relation and its subring -/
/-! ## Counterexample: `jet4` is not multiplicative on the whole polynomial ring -/
/-! ## Ring-hom transport of the weighted bodies and the Γ core body -/
section Expr
variable {R S : Type*} [CommRing R] [CommRing S]
/-- Commutative-ring body of VII-04's `gammaCore` (values `x u h Q J F θF b A θA θ₂A`). -/
def coreE (x u h Q J F dF b A dA ddA : R) : R :=
Q * (u * F * (2 * dA + ddA) - u * (2 * F + dF) * dA - h * (x * (F * dA)))
+ 2 * (x * ((J + 2 * Q * A) * F * b * dA * dA))
end Expr
end ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.SmoothExt