Vacuum certificates transport along a first-release coordinate relation (four dimensions)
ProvedExactVacuumAtlas.Release02.certificate_transportDimension 4. Let (h, ĥ) carry a vacuum certificate on V, let r : CoordRelation g h U V Φ Ψ J, and assume U is open, U is nonempty, J(y)·K(y) = I for every y ∈ U (an explicit right inverse K of the Jacobian) and ĝ(y)·g(y) = I for every y ∈ U (any genuine left inverse ĝ of g). Then (g, ĝ) carries a vacuum certificate on U. CoordRelation g₁ g₂ U V Φ Ψ J (bundle Atlas_Core_Relation, release I) is the conjunction of seven obligations: Ψ(Φ x) = x on U; Φ(Ψ y) = y on V; Φ maps U bijectively onto V; Φ is C^∞ on U; Ψ is C^∞ on V; every entry J(x)_{ki} is the genuine derivative of the slice u ↦ Φ(x[x_i := u])k at u = x_i (x ∈ U); and J(x)ᵀ g₂(Φ x) J(x) = g₁(x) on U. It has no Ricci content. VacuumCertificate g ĝ U (bundle Atlas_Core_Certificate, release I) is the conjunction of eight obligations: U open; U nonempty; g symmetric on U; ĝ(x)·g(x) = I on U; every component of g C^∞ on U; every component of ĝ C^∞ on U; at every x ∈ U an invertible E with Eᵀ g(x) E = diag(−1,1,1,1) (Lorentzian); and all 16 components Ric(g,ĝ){bd}(x) = 0 for x ∈ U.
import Mathlib import Definitions.Def_Atlas_Controls_CylinderTables import Definitions.Def_Atlas_Controls_Shear import Definitions.Def_Atlas_Controls_ShearTables import Definitions.Def_Atlas_Core_Basic import Definitions.Def_Atlas_Core_Certificate import Definitions.Def_Atlas_Core_Lift import Definitions.Def_Atlas_Core_Relation import Definitions.Def_Atlas_Isotropic_CartChart import Definitions.Def_Atlas_Isotropic_CartCover import Definitions.Def_Atlas_Isotropic_CartMaps import Definitions.Def_Atlas_Isotropic_Defs import Definitions.Def_Atlas_Minkowski_Spherical import Definitions.Def_Atlas_Schwarzschild_Defs import Definitions.Def_Atlas_Schwarzschild_Domain import Definitions.Def_Atlas_Schwarzschild_PGCertParts import Definitions.Def_Atlas_Schwarzschild_PGDefs import Definitions.Def_Atlas_Schwarzschild_PGRelation import Definitions.Def_Atlas_Transport_Connection import Definitions.Def_Atlas_Transport_Curvature import Definitions.Def_Atlas_Transport_MatrixCalc open Real Matrix open ExactVacuumAtlas ExactVacuumAtlas.Schwarzschild ExactVacuumAtlas.Controls
theorem ExactVacuumAtlas.Release02.certificate_transport {U V : Set (Pt 4)} {Φ Ψ : Pt 4 → Pt 4}
{J K : Pt 4 → Matrix (Fin 4) (Fin 4) ℝ} {g gi h hi : Metric 4}
(hcert : VacuumCertificate h hi V) (r : CoordRelation g h U V Φ Ψ J) (hU : IsOpen U)
(hne : U.Nonempty) (hJK : ∀ y ∈ U, J y * K y = 1)
(hgi : ∀ y ∈ U, metricMatrix gi y * metricMatrix g y = 1) :
VacuumCertificate g gi U := by sorryConfirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.