Two-ball packing obstruction in the projective plane (source code)

= Two-ball packing obstruction in the projective plane
{title2=$r_1^2+r_2^2\leq1$}

Two disjoint <symplectic balls> of radii $r_1,r_2$ embedding into the unit four-ball must satisfy the displayed inequality. Extend their transported standard <complex structures> on smaller concentric balls to a <compatible almost complex structure> on the projective plane. A degree-one <J-holomorphic curve> through both centres has area $\pi$. The <Monotonicity theorem for a J-holomorphic curve> bounds its area in each smaller ball below by $\pi\rho_i^2$. Disjointness allows these bounds to be added; letting $\rho_i$ increase to $r_i$ proves the result.