-- 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/GeodesicCongruenceObstruction.lean
-- definition bundle: kept ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.Geodesic.RicciNullPregeodesicField
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_ChargedTail
import Definitions.Def_Atlas_EinsteinMaxwell_ES5_KerrSchild_CompactifiedBridge
import Definitions.Def_Atlas_EinsteinMaxwell_ES5_KerrSchild_CompactifiedResiduals
import Definitions.Def_Atlas_EinsteinMaxwell_ES5_KerrSchild_CoordinateAcceleration
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_MaxwellFrame
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_PrincipalGeodesic
import Definitions.Def_Atlas_EinsteinMaxwell_ES5_KerrSchild_RadialBVP
import Definitions.Def_Atlas_EinsteinMaxwell_ES5_KerrSchild_RadialBVPEquivalence
import Definitions.Def_Atlas_EinsteinMaxwell_ES5_KerrSchild_RicciNullDirections
import Definitions.Def_Atlas_EinsteinMaxwell_ES5_KerrSchild_ScalarCertificate
import Definitions.Def_Atlas_EinsteinMaxwell_ES5_KerrSchild_SmoothBranch

/-! # VII-07 (F3b): arbitrary actual Ricci-null pregeodesic fields force `G = 0`

Let `V` be a vector field, `C¹` on an open `U ⊆ esDomain I`, and on all of `U` nonzero, actually
null and actually Ricci-null (actual `esMetric`, `ricciOf`), where the candidate's own
Einstein–Maxwell equations hold and `f, m, N, alphaSq > 0`. VII-06's pointwise classification
(`vii06_ricci_null_directions`) puts `V(y)` on one of the two principal lines at every `y ∈ U`; it
does not say which, and no sign choice or local constancy is used. The common scale
`ρ = f V⁰ / e` then satisfies, **on the open set `U`**, the momentum identities
`(gV)₀ = -ρ p'`, `(gV)₃ = -ρ u a'`, `(gV)₄ = -ρ (1-u) a'`, which may be differentiated. With the
lowered-acceleration identity (`∂_t g = ∂_φ g = ∂_ψ g = 0`) the derivatives of `ρ` cancel in

  `p' ((g·accel V)₃ + (g·accel V)₄) - a' (g·accel V)₀ = ρ V¹ G`,

and pregeodesicity at `x` makes the left side vanish; `ρ ≠ 0`, `V¹ ≠ 0` give `G(R) = 0`
(`vii07_ricci_null_pregeodesic_G_zero`). The multiplier `κ` is never differentiated.

Composition with VII-05: `SmoothBranch.restrict` (same independent extension, smaller radius) and a
fresh VII-05 call at the smaller radius `η`. Results are labelled a **Ricci-null pregeodesic
congruence obstruction**: the Kerr–Schild ⇒ Ricci-null bridge is not part of this module. -/

open scoped ContDiff Topology Matrix
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.NullDirections
open ExactVacuumAtlas.EinsteinMaxwell.D (einsteinMaxwellD EMCertificateD)

namespace ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.Geodesic

/-- The actual congruence premise on a set `U`: `V` is `C¹` on `U` and at every point of `U` it is
nonzero, `g`-null, `Ric`-null and pregeodesic (actual `g`, `ginv`, `ricciOf`, `accel`). -/
structure RicciNullPregeodesicField (g ginv : Metric 5) (U : Set (Pt 5))
    (V : Pt 5 → Fin 5 → ℝ) : Prop where
  smooth : ∀ i, ContDiffOn ℝ 1 (fun x => V x i) U
  ne_zero : ∀ x ∈ U, V x ≠ 0
  null : ∀ x ∈ U, contract2 g x (V x) = 0
  ricci_null : ∀ x ∈ U, contract2 (ricciOf g ginv) x (V x) = 0
  pregeodesic : ∀ x ∈ U, PregeodesicAt g ginv V x

variable {I : Set ℝ} {f m N w p a : ℝ → ℝ}

/-! ## Common scale and lowered Killing momenta of a classified vector -/

/-! ## The common-momentum wedge -/

/-! ## Restricting the raw smooth branch, and the distant-tail radius -/

/-! ## Composition with VII-05 on an arbitrary distant tail -/

section Tail

variable {I : Set ℝ} {f m N w p a F b A : ℝ → ℝ} {s h ε Q J : ℝ}

end Tail

/-! ## Certificate side -/

end ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.Geodesic