Atlas VII definitions: KSMetric
DefinitionAtlas_EinsteinMaxwell_ES5_KerrSchild_KSMetricDefinitions of the Atlas VII module Atlas.EinsteinMaxwell.ES5.KerrSchild.KSMetric (kept exactly as in the accepted source, skeleton subtraction).
VII-08 (1/5): same-coordinate Kerr–Schild metric over an independent background
All objects live in one coordinate chart Pt 5 on an open U. The raw data are an
independent background metric b, its actual inverse bi, a profile v and a vector field k.
With ℓ_i = Σ_j b_ij k^j (lowerK) the Kerr–Schild metric and inverse are
g_ij = b_ij + v ℓ_i ℓ_j, gi^ij = bi^ij − v k^i k^j (plus-profile convention; the
2009 convention g = η − 2H ℓℓ is v = −2H).
KSData only packages genuine raw geometric data: the existing background record
MetricData b bi U (openness, symmetry of b, bi · b = 1, componentwise C^∞ of b, bi;
reused from Atlas/Transport, no curvature condition), C^∞ of v, k on U (stronger than the
C² that suffices; assumed for the Core.Pd API), and actual b(k,k) = 0 on all of U. It contains no connection,
acceleration, curvature or Ricci-null statement. b may be non-constant with cross terms.
Proved here: bi is two-sided and symmetric, g is symmetric, gi · g = 1 = g · gi,
g k = ℓ, gi ℓ = k, g(k,k) = 0, and C^∞ of ℓ, g, gi on U. No v ≠ 0, k ≠ 0,
Lorentz signature or flatness is used.
Constants in this bundle: KSData, ksInverse, ksMetric, lowerK.
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/KSMetric.lean
-- definition bundle: kept ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.Geometry.KSData, ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.Geometry.ksInverse, ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.Geometry.ksMetric, ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.Geometry.lowerK
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_CoordinateAcceleration
import Definitions.Def_Atlas_EinsteinMaxwell_ES5_KerrSchild_MaxwellFrame
import Definitions.Def_Atlas_EinsteinMaxwell_ES5_KerrSchild_PaperGauge
import Definitions.Def_Atlas_EinsteinMaxwell_ES5_KerrSchild_RadialBVP
import Definitions.Def_Atlas_EinsteinMaxwell_ES5_KerrSchild_RadialBVPEquivalence
import Definitions.Def_Atlas_Transport_Connection
/-! # VII-08 (1/5): same-coordinate Kerr–Schild metric over an independent background
All objects live in **one** coordinate chart `Pt 5` on an open `U`. The raw data are an
independent background metric `b`, its actual inverse `bi`, a profile `v` and a vector field `k`.
With `ℓ_i = Σ_j b_ij k^j` (`lowerK`) the Kerr–Schild metric and inverse are
`g_ij = b_ij + v ℓ_i ℓ_j`, `gi^ij = bi^ij − v k^i k^j` (plus-profile convention; the
2009 convention `g = η − 2H ℓℓ` is `v = −2H`).
`KSData` only packages genuine raw geometric data: the existing background record
`MetricData b bi U` (openness, symmetry of `b`, `bi · b = 1`, componentwise `C^∞` of `b, bi`;
reused from `Atlas/Transport`, no curvature condition), `C^∞` of `v, k` on `U` (stronger than the
`C²` that suffices; assumed for the `Core.Pd` API), and actual `b(k,k) = 0` on **all** of `U`. It contains no connection,
acceleration, curvature or Ricci-null statement. `b` may be non-constant with cross terms.
Proved here: `bi` is two-sided and symmetric, `g` is symmetric, `gi · g = 1 = g · gi`,
`g k = ℓ`, `gi ℓ = k`, `g(k,k) = 0`, and `C^∞` of `ℓ, g, gi` on `U`. No `v ≠ 0`, `k ≠ 0`,
Lorentz signature or flatness is used.
-/
open scoped ContDiff Topology Matrix
open ExactVacuumAtlas ExactVacuumAtlas.EinsteinMaxwell ExactVacuumAtlas.EinsteinMaxwell.ES5
open ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.NullDirections (contract2)
open ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.Geodesic
namespace ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.Geometry
/-- Lowered Kerr–Schild one-form `ℓ_i = Σ_j b_ij k^j` (background lowering). -/
noncomputable def lowerK (b : Metric 5) (k : Pt 5 → Fin 5 → ℝ) (x : Pt 5) (i : Fin 5) : ℝ :=
∑ j, b i j x * k x j
/-- Kerr–Schild metric `g_ij = b_ij + v ℓ_i ℓ_j`. -/
noncomputable def ksMetric (b : Metric 5) (v : Pt 5 → ℝ) (k : Pt 5 → Fin 5 → ℝ) : Metric 5 :=
fun i j x => b i j x + v x * lowerK b k x i * lowerK b k x j
/-- Kerr–Schild inverse `gi^ij = bi^ij − v k^i k^j`. -/
noncomputable def ksInverse (bi : Metric 5) (v : Pt 5 → ℝ) (k : Pt 5 → Fin 5 → ℝ) : Metric 5 :=
fun i j x => bi i j x - v x * k x i * k x j
/-- Raw same-coordinate Kerr–Schild data on an open `U` (geometric data only). -/
structure KSData (b bi : Metric 5) (v : Pt 5 → ℝ) (k : Pt 5 → Fin 5 → ℝ) (U : Set (Pt 5)) :
Prop where
bg : MetricData b bi U
smooth_v : ContDiffOn ℝ ∞ v U
smooth_k : ∀ i, ContDiffOn ℝ ∞ (fun x => k x i) U
null : ∀ x ∈ U, contract2 b x (k x) = 0
variable {b bi : Metric 5} {v : Pt 5 → ℝ} {k : Pt 5 → Fin 5 → ℝ} {U : Set (Pt 5)}
namespace KSData
variable (hD : KSData b bi v k U)
include hD
/-! ### Genuine smoothness and differentiability on `U` -/
end KSData
end ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.Geometry