Off-shell first-variation bridge for the Einstein–Maxwell residual (goal)

Off-shell first-variation bridge for the Einstein–Maxwell residual (goal)

Let (g_ε, ginv_ε, F_ε), ε ∈ ℝ, be four-dimensional component fields on an open set W ⊆ ℝ × ℝ⁴ satisfying FamilyData, and let (h, f) be the genuine ε-derivative of (g_ε, F_ε) at ε = 0 on the slice {y : (0, y) ∈ W} (IsTangent). Then for every x with (0, x) ∈ W and all indices: d/dε|₀ E_ab(g_ε, ginv_ε, F_ε)(x) = LE_ab(g_0, ginv_0, F_0; h, f)(x), d/dε|₀ J^b(g_ε, ginv_ε, F_ε)(x) = LJ^b(g_0, ginv_0, F_0; h, f)(x), and d/dε|₀ H_abc(F_ε)(x) = LH_abc(f)(x), each as a Mathlib HasDerivAt at ε = 0. Residuals (registered H1–H8, 4D): E_ab = R_ab − ½ g_ab R − 2 S_ab with R = Σ g^{ab} R_ab and S_ab = Σ_{c,d} F_ac g^{cd} F_bd − ¼ g_ab F_cd F^{cd} (F^{ab} = Σ g^{ac} g^{bd} F_cd, raised with the given ginv); J^b = Σ_a (∂a F^{ab} + Σ_k (Γ^a{ak} F^{kb} + Γ^b_{ak} F^{ak})) (an upper-index vector); H_abc = ∂a F_bc + ∂b F_ca + ∂c F_ab (a covariant 3-index quantity). E is a covariant 2-index quantity. Linearised residuals (registered J1–J10) are specified independently by finite sums and coordinate derivatives; they are not defined as the parameter derivative of the nonlinear residual. In particular, with K = invVar ginv h = −G h G (G = ginv) and C = chrVar g ginv h, LE_ab = δR_ab − ½ (h_ab R + g_ab δR) − 2 δS_ab, LJ^b = Σ_a [∂a V^{ab} + Σ_k (C^a{ak} F^{kb} + Γ^a{ak} V^{kb} + C^b{ak} F^{ak} + Γ^b{ak} V^{ak})] with V = raise2Var, LH_abc = ∂_a f_bc + ∂_b f_ca + ∂_c f_ab.

Scope. FamilyData contains exactly: W open; (ε, y) ↦ g_ε,ij(y) and (ε, y) ↦ F_ε,ij(y) are C^∞ on W; ginv_ε(y) · g_ε(y) = 1 (true left inverse, as 4×4 matrices) at every (ε, y) ∈ W. It does NOT assume symmetry of g, a Lorentzian signature, antisymmetry of F or any field equation; it is a derivative contract for the finite coordinate expressions, not a statement that an arbitrary matrix field is a physical metric. Physical backgrounds enter only through the full EinsteinMaxwellCertificate. The statement is off-shell: no residual is assumed to vanish, and no family of solutions is assumed.

中文摘要 离壳一阶变分桥：对满足 FamilyData 的同一四维族、同一切向 (h,f) 与基点 (0,x)∈W，E、J、H 三个残差在 ε=0 的真实导数分别等于显式算子 LE、LJ、LH。