Minimal Relational Visibility

Abstract

Two nonnegative Pick-kernel diagonal values can form an indefinite two-point relation.

Theorem 1.1 (The first negative relation certificate has width two).

$$\forall s:\mathbb{C}\to \mathbb{C},a\in \mathbb{D},(s\left(0\right)=0\wedge s\left(a\right)=1)\Rightarrow \mathrm{let}(K:=(z,w\mapsto \frac{1-s\left(z\right)\times \overline{s\left(w\right)}}{1-z\times \overline{w}}),p:=\mathrm{vector}\left(0,a\right),R:=(i,j\mapsto K\left(p\left(i\right),p\left(j\right)\right)))R=\mathrm{matrix}\left(1,1,1,0\right)\wedge (\forall i\in \{0,1\},0\le R\left(i,i\right))\wedge \det \left(R\right)=-1\wedge \neg \mathrm{PosSemidef}\left(R\right)\wedge \neg \exists A:\mathrm{Matrix}\left(2,2,\mathbb{C}\right),R=\mathrm{conjTranspose}\left(A\right)\times A.$$

Proof. Machine-checked in Lean as D5/S3/Weil/Pick/MinimalRelationalVisibility.minimal_relational_visibility (✓ std3). ∎

Source. Repository-derived.

Commentary.

Let s be a complex Schur candidate and a an interior disk point, with s zero at the origin and one at a. The displayed kernel, point family, and relation matrix are the source constructions.

Both one-point diagonal tests are nonnegative. Sampling the two names together gives the matrix with rows (1,1) and (1,0), whose determinant is minus one and which is not positive semidefinite.

Every conjugate-transpose product is positive semidefinite, so the same certificate rules out a Gram factorization of the joint relation.

References

• Truth anchor: D5/S3/Weil/Pick/MinimalRelationalVisibility.minimal_relational_visibility