Atlas VII definitions: FiniteJetObstruction
DefinitionAtlas_EinsteinMaxwell_ES5_KerrSchild_FiniteJetObstructionDefinitions of the Atlas VII module Atlas.EinsteinMaxwell.ES5.KerrSchild.FiniteJetObstruction (kept exactly as in the accepted source, skeleton subtraction).
Atlas VII-00/01 (F1): finite-jet obstruction for the actual polynomial Γ, with controls.
Level VII01_FINITE_JET_OBSTRUCTION_LEAN. What is certified: for the explicit real polynomial
gammaJet M h J Q c (built from the transcribed jets of Fröb–Khavkine–Málek–Pravda 2022,
Eq. 36), vanishing of its x⁶, x⁷, x⁸ coefficients forces J³ Q⁵ = 0, hence J = 0 ∨ Q = 0,
for all real parameters (no division, no sign or nonvanishing assumption).
What is NOT certified here (pending, notes/VII_BRIDGE_STATUS.md): F2 — that solutions of the
five-dimensional Einstein–Maxwell equations with the paper's asymptotics have these jets and
that Γ represents (1 - h x)² G for the actual geodesic defect G; F3 — that a flat-background
geodesic Kerr–Schild form forces G = 0 (Ricci principal null directions, anomalous branches).
This file is therefore not a Kerr–Schild no-go theorem for black holes.
Constants in this bundle: certP6, certP7.
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/FiniteJetObstruction.lean -- definition bundle: kept ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.FiniteJet.certP6, ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.FiniteJet.certP7 import Mathlib import Definitions.Def_Atlas_EinsteinMaxwell_ES5_KerrSchild_PolynomialJet import Definitions.Def_Atlas_EinsteinMaxwell_ES5_KerrSchild_ScalarCertificate /- Atlas VII-00/01 (F1): finite-jet obstruction for the actual polynomial Γ, with controls. Level `VII01_FINITE_JET_OBSTRUCTION_LEAN`. What is certified: for the explicit real polynomial `gammaJet M h J Q c` (built from the transcribed jets of Fröb–Khavkine–Málek–Pravda 2022, Eq. 36), vanishing of its x⁶, x⁷, x⁸ coefficients forces `J³ Q⁵ = 0`, hence `J = 0 ∨ Q = 0`, for all real parameters (no division, no sign or nonvanishing assumption). What is NOT certified here (pending, notes/VII_BRIDGE_STATUS.md): F2 — that solutions of the five-dimensional Einstein–Maxwell equations with the paper's asymptotics have these jets and that Γ represents `(1 - h x)² G` for the actual geodesic defect `G`; F3 — that a flat-background geodesic Kerr–Schild form forces `G = 0` (Ricci principal null directions, anomalous branches). This file is therefore not a Kerr–Schild no-go theorem for black holes. -/ set_option autoImplicit false open Polynomial namespace ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.FiniteJet /-- Multiplier of `[x⁶] Γ` in the polynomial-coefficient certificate. -/ noncomputable def certP6 (M h J Q c : ℝ) : ℝ := ((3 : ℝ) / 4) * elimS M h J Q c + Q * M ^ 3 * (4 * h ^ 2 - ((11 : ℝ) / 5) * M * h) /-- Multiplier of `[x⁷] Γ` in the polynomial-coefficient certificate. -/ noncomputable def certP7 (M h _J Q _c : ℝ) : ℝ := Q * M ^ 3 * (((3 : ℝ) / 2) * h - ((11 : ℝ) / 10) * M) /-! ### Controls -/ /-! ### Root -/ end ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.FiniteJet