Real noncommutative convexity I

We initiate the theory of real noncommutative (nc) convex sets, the real case of the recent and profound complex theory developed by Davidson and Kennedy (2025). The present paper focuses on the real case of the topics from the first several sections of their memoir. Later results will be discussed in future papers. We develop here some of the infrastructure of real nc convexity, giving many foundational structural results for real operator systems and their associated nc convex sets, and elucidate how the complexification interacts with the basic convexity theory constructions. Several new features appear in the real case, including the novel notion of the complexification of a nc convex set.