B-field shifts are isometries
ProvedGeneralizedComplex.bShift_pairingLet be a real 2-form on (a skew-symmetric matrix, ) and let . Then for all ,
So B-field shifts preserve the natural inner product of the generalized tangent space.
Throughout, models a tangent space of an -manifold, its dual (identified with via the standard dual basis), and the generalized tangent space with the natural inner product . A generalized almost complex structure is a real linear map of with and ; its -eigenbundle is .
Formalization Note The statement is fiberwise: is the coordinate space GIdx N → ℝ (vector part on Sum.inl, one-form part on Sum.inr), endomorphisms are matrices indexed by GIdx N, and the complexification is GIdx N → ℂ with the real matrix acting through the coercion . All notions are those of the shared definition file Definitions.Def_GeneralizedComplex_Basic.
import Definitions.Def_GeneralizedComplex_Basic open Matrix
namespace GeneralizedComplex
theorem bShift_pairing {N : ℕ} (B : Matrix (Fin N) (Fin N) ℝ) (hB : Bᵀ = -B)
(u v : GIdx N → ℝ) :
pairing (bShift B *ᵥ u) (bShift B *ᵥ v) = pairing u v := by sorry
end GeneralizedComplexConfirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.