OAI/Analysis/OInfinity/ConnectedHalfFlipTheorem.lean

The connected approximate inner half-flip of O∞, obtained from the actual finite connected conjugacy of its two commuting tensor-factor rows. This is the specialization of Kirchberg (2006), Proposition 4.4(3),(5) and Remark 4.6 needed by the nonunital absorption criterion.