Every C^∞ direction is realised by a genuine local straight-line family
ProvedExactVacuumAtlas.Variation.familyData_lineEvery C^∞ direction is realised by a genuine local straight-line family
For any n, open U ⊆ ℝⁿ and C^∞ (on U) component fields g, h (Metric n) and F, f (TwoForm n): the family ε ↦ (g + εh, (g + εh)⁻¹, F + εf), with (g + εh)⁻¹ the Mathlib matrix inverse, satisfies FamilyData on lineDom U g h = {(ε, y) : y ∈ U, det(g + εh)(y) ≠ 0}.
Scope. Local: lineDom is open but no uniform ε-interval over a non-compact U is claimed; (0, x) ∈ lineDom iff x ∈ U and det g(x) ≠ 0. h, f may depend on all four coordinates; no symmetry or field equation is assumed. Combined with the goal bridge this gives the derivatives along the line (hasDerivAt_line_*). The family is not claimed to consist of solutions.
中文摘要 任意 C^∞ 的 (h,f) 都由真实的直线族 g+εh、(g+εh)⁻¹、F+εf 在开集 lineDom 上实现为 FamilyData。
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_LineFamily
import Definitions.Def_Atlas_EinsteinMaxwell_Variation_Local
import Definitions.Def_Atlas_Transport_MatrixCalc
open Filter Topology
open scoped ContDiff
open Matrix
open ExactVacuumAtlas.EinsteinMaxwell
open ExactVacuumAtlas
open ExactVacuumAtlas.Variation
variable {n : ℕ}
variable {U : Set (Pt n)} {g gi h : Metric n} {F f : TwoForm n}
theorem ExactVacuumAtlas.Variation.familyData_line (hU : IsOpen U) (hg : ∀ i j, ContDiffOn ℝ ∞ (g i j) U)
(hh : ∀ i j, ContDiffOn ℝ ∞ (h i j) U) (hF : ∀ i j, ContDiffOn ℝ ∞ (F i j) U)
(hf : ∀ i j, ContDiffOn ℝ ∞ (f i j) U) :
FamilyData (lineMetric g h) (lineInv g h) (lineMetric F f) (lineDom U g h) := by sorryConfirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.