Non-vacuum control, route 2: the same sixteen components from the transformation law
ProvedExactVacuumAtlas.Release02.control_transportFor every real λ, every x ∈ domEF and all b, d ∈ {0,1,2,3}: Ric(gCtl λ, giCtl λ)_{bd}(x) = ctlR λ b d x. Coordinates (T, R, α, β) = (x 0, x 1, x 2, x 3); domEF = {R > 0, 0 < α < π}. The control metric gCtl λ = Jᵀ h(Φ) J is the pull-back of the cylinder-type metric h = −dT² + dR² + dα² + sin²α dβ² (Controls.Cylinder.gCyl 0, release I; not vacuum: R_αα = 1, R_ββ = sin²α) under the shear Φ(T,R,α,β) = (T,R,α,β + λ sin α), J = I + λ cos α E₃₂: g_00 = −1, g_11 = 1, g_22 = 1 + λ²c²s², g_23 = g_32 = λ c s², g_33 = s², rest 0 (c = cos α, s = sin α); candidate inverse giCtl: ĝ^00 = −1, ĝ^11 = 1, ĝ^22 = 1, ĝ^23 = ĝ^32 = −λc, ĝ^33 = (1 + λ²c²s²)/s². ctlR λ: R_22 = 1 + λ²c²s², R_23 = R_32 = λ c s², R_33 = s², the other 12 components 0. (Identical formal statement to control_direct; proved through ricci_law.) The formulas hold for every real λ. The map is the identity for λ = 0 and is non-affine for λ ≠ 0; non-affinity is not asserted for the entire parameter family without this qualification.
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.control_transport : ∀ lam : ℝ, ∀ x ∈ domEF, ∀ b d,
ricciOf (Shear.gCtl lam) (Shear.giCtl lam) b d x = Shear.ctlR lam b d x := by sorryConfirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.