$K_G\ge\pi/2$

Provenance: this read-back is NOT blind and is NOT independent testimony. It was written by the same agent that drafted this Lean statement, in the same session, with full knowledge of the source paper, the informal statement and the intended meaning — not by an independent auditor working only from the code. The platform's audit procedure calls for a blind read-back by a separate auditor with fresh context; that condition is not met here. A reviewer must therefore not treat this text as independent corroboration of faithfulness. Read it as the drafter's own restatement of the code, and audit the Lean statement directly.

The claim is the single inequality

where $\pi$ is the circle constant and $P(K)$ is the property that for every pair of natural numbers $m,n$ and every real $m\times n$ matrix $A$, the supremum of $\sum_{i,j}A_{i,j}\langle u_i,v_j\rangle$ over families of unit vectors in Euclidean space of arbitrary finite dimension is at most $K$ times the supremum of $\sum_{i,j}A_{i,j}x_iy_j$ over $\pm1$-valued real vectors $x,y$.

There are no free variables and no hypotheses. Note that the infimum is taken in the reals: if the set of such $K$ were empty, or unbounded below, the convention in force would make the right-hand side $0$ and the statement false; the assertion therefore also implicitly carries information about that set being nonempty and bounded below.