  We show that the semidefinite programs involved in the computer proofs for
Kazhdan's property (T) satisfy strong duality and that the dual programs have a
geometric interpretation in terms of harmonic cocycles. By dualizing geometric
arguments about cocycles, we are able to simplify the property (T) SDP in the
case where it carries a symmetry by finite-order inner automorphisms. As an
application, we simplify the SDP proof for $SL(n,\mathbb{Z})$ and we prove that
$Aut(F_4)$ has property (T).
