Real index zero characterizes generalized almost complex structures
ProvedGeneralizedComplex.realIndex_eq_zero_iffLet be a maximal isotropic subspace and let be its real index. Then is the -eigenbundle of a generalized almost complex structure if and only if
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 realIndex_eq_zero_iff {N : ℕ} (L : Submodule ℂ (GIdx N → ℂ))
(hL : IsMaximalIsotropic L) :
(∃ J : Matrix (GIdx N) (GIdx N) ℝ, IsGenAlmostComplex J ∧ plusIEigenspace J = L) ↔
realIndex L = 0 := by sorry
end GeneralizedComplexConfirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.