Straight-line family
DefinitionAtlas_EinsteinMaxwell_Variation_LineFamilyeinstein-maxwellexact-spacetime-atlas-ivexact-vacuum-atlasgeneral-relativity
Straight-line family
lineMetric g h ε = g + εh, lineInv = Mathlib matrix inverse of g + εh, lineDom U g h = {y ∈ U, det(g + εh) ≠ 0}.
中文摘要 直线族 g+εh 及其真实逆与开域。
Registry: PHYSICS_BOUNDARY §J (J18).
Definition code
-- Generated by scripts/release04/gen_platform_tree.py (ATLAS-RELEASE-04) by skeleton subtraction from Atlas/EinsteinMaxwell/Variation/LineFamily.lean
-- definition bundle: kept ExactVacuumAtlas.Variation.lineDom, ExactVacuumAtlas.Variation.lineInv, ExactVacuumAtlas.Variation.lineMetric
import Mathlib
import Definitions.Def_Atlas_Core_Basic
import Definitions.Def_Atlas_EinsteinMaxwell_Basic
import Definitions.Def_Atlas_EinsteinMaxwell_Variation_Defs
import Definitions.Def_Atlas_EinsteinMaxwell_Variation_Local
import Definitions.Def_Atlas_Transport_MatrixCalc
/-! # Every `C^∞` perturbation is realised: straight-line families with the true inverse (ATLAS-IV-03)
For a background `(g, gi, F)` on an open `U` (`g`, `F` of class `C^∞`, `gi g = 1` on `U`; **no** field
equation, symmetry or signature assumed) and **arbitrary** `C^∞` perturbations `h`, `f` on `U` (all four
coordinates, no symmetry required by the bridge itself), the straight-line family
`g_ε = g + ε h`, `ginv_ε = (g + ε h)⁻¹` (Mathlib's `Matrix.inv`), `F_ε = F + ε f`
is a `FamilyData` on the open set `lineDom U g h = {(ε, y) | y ∈ U, det(g + ε h)(y) ≠ 0}` (it contains
`{0} × U`; nondegeneracy near `ε = 0` is proved, not assumed, and no uniform `ε`-interval is claimed), with
genuine tangent `(h, f)`. Consequently (`hasDerivAt_line_einstein`, `_maxwell`, `_faraday`) the explicit
operators are the actual directional derivatives of the nonlinear residual along every admissible
perturbation, at every `x ∈ U`. -/
open Filter Topology
open scoped ContDiff
open Matrix
open ExactVacuumAtlas.EinsteinMaxwell
namespace ExactVacuumAtlas.Variation
variable {n : ℕ}
/-- `g + ε h` (class B). -/
def lineMetric (g h : Metric n) (ε : ℝ) : Metric n := fun i j y => g i j y + ε * h i j y
/-- `(g + ε h)⁻¹` entrywise (class B; Mathlib's nonsingular inverse). -/
noncomputable def lineInv (g h : Metric n) (ε : ℝ) : Metric n :=
fun i j y => (metricMatrix (lineMetric g h ε) y)⁻¹ i j
/-- Open domain of the straight-line family (class B). -/
def lineDom (U : Set (Pt n)) (g h : Metric n) : Set (ℝ × Pt n) :=
{p | p.2 ∈ U ∧ (metricMatrix (lineMetric g h p.1) p.2).det ≠ 0}
section line
variable {U : Set (Pt n)} {g gi h : Metric n} {F f : TwoForm n}
end line
section line4
variable {U : Set (Pt 4)} {g gi h : Metric 4} {F f : TwoForm 4}
(hU : IsOpen U) (hg : ∀ i j, ContDiffOn ℝ ∞ (g i j) U)
(hinv : ∀ y ∈ U, metricMatrix gi y * metricMatrix g y = 1) (hF : ∀ i j, ContDiffOn ℝ ∞ (F i j) U)
(hh : ∀ i j, ContDiffOn ℝ ∞ (h i j) U) (hf : ∀ i j, ContDiffOn ℝ ∞ (f i j) U)
include hU hg hinv hF hh hf
end line4
end ExactVacuumAtlas.Variation
Source
He Wang, Exact Spacetime Atlas IV: Certified Einstein–Maxwell Backgrounds and First Variations. Local source, no public repository; commit 543904bfcfa3bb169f43fc4d9dbd569999b71886; Atlas/EinsteinMaxwell/Variation/LineFamily.lean; SHA-256 afc3b70a17a93bd1217b6ce19d567cf12c2c04fac9d9ce907ceab23c88c02112. Registered definitions and literature: mission/PHYSICS_BOUNDARY.md (§H–§J); Müller–Grave arXiv:0904.4184; Newman et al., J. Math. Phys. 6 (1965) 918.
Human review
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.