Positive Singular-Support Columns and Diagonalization

Abstract

Positive singular-support candidate columns admit an explicit real diagonalization.

Definition 1.1 (The singular-support radius).

$$z:\mathbb{R},p:(\mathrm{Fin}(2))\to \mathbb{R}\Rightarrow r(z,p)=\sqrt{z^2+{p_0}^2+{p_1}^2}.$$

Formalization. D5/S3/QuantumContext/SingularSupportCandidateDiagonalizable.r (✓ std3).

Source. Repository-derived.

Commentary.

The radius combines the distinguished positive coordinate with the two support coordinates.

Definition 1.2 (The unnormalized support block).

$$z:\mathbb{R},p:(\mathrm{Fin}(2))\to \mathbb{R}\Rightarrow \mathrm{gZero}(z,p)=zr(z,p)I_2+\frac{r(z,p)}{r(z,p)+z}\mathrm{vecMulVec}(p,p).$$

Formalization. D5/S3/QuantumContext/SingularSupportCandidateDiagonalizable.gZero (✓ std3).

Source. Repository-derived.

Commentary.

The support block is a positive scalar identity plus a positive rank-one matrix.

Definition 1.3 (The column-normalization matrix).

$$z:\mathbb{R},p:(\mathrm{Fin}(2))\to \mathbb{R},H(z,p)=\mathrm{diagonal}((j\mapsto \frac{p_j}{r(z,p)\sqrt{z^2+{p_j}^2}})).$$

Formalization. D5/S3/QuantumContext/SingularSupportCandidateDiagonalizable.H (✓ std3).

Source. Repository-derived.

Commentary.

Each diagonal entry normalizes one support column by its radius and planar length.

Definition 1.4 (The normalized support block).

$$z:\mathbb{R},p:(\mathrm{Fin}(2))\to \mathbb{R}\Rightarrow K(z,p)=\mathrm{gZero}(z,p)H(z,p).$$

Formalization. D5/S3/QuantumContext/SingularSupportCandidateDiagonalizable.K (✓ std3).

Source. Repository-derived.

Commentary.

Right multiplication by the diagonal normalization rescales the two columns of the support block.

Definition 1.5 (The distinguished eigenvalue).

$$z:\mathbb{R},p:(\mathrm{Fin}(2))\to \mathbb{R}\Rightarrow q(z,p)=\frac{1}{r(z,p)}\sum _{j\in \mathrm{Fin}(2)}{p}_j\sqrt{z^2+{p_j}^2}.$$

Formalization. D5/S3/QuantumContext/SingularSupportCandidateDiagonalizable.q (✓ std3).

Source. Repository-derived.

Commentary.

The distinguished eigenvalue is the radius-normalized sum of the two weighted planar lengths.

Definition 1.6 (The final candidate column).

$$z:\mathbb{R},p:(\mathrm{Fin}(2))\to \mathbb{R}\Rightarrow u(z,p)=\frac{1}{z}(q(z,p)I_2-K(z,p))p.$$

Formalization. D5/S3/QuantumContext/SingularSupportCandidateDiagonalizable.u (✓ std3).

Source. Repository-derived.

Commentary.

The final column is the scaled residual of the distinguished eigenvalue equation on the positive support vector.

Definition 1.7 (The three-dimensional block candidate).

$$z:\mathbb{R},p:(\mathrm{Fin}(2))\to \mathbb{R}\Rightarrow Q(z,p)=\mathrm{fromBlocks}(K(z,p),u(z,p),0,q(z,p)).$$

Formalization. D5/S3/QuantumContext/SingularSupportCandidateDiagonalizable.Q (✓ std3).

Source. Repository-derived.

Commentary.

The candidate is block upper triangular with support block K, final column u, and scalar block q.

Theorem 1.8 (Positive columns and explicit real diagonalization).

$$\begin{array}{c}\forall z:\mathbb{R},p:(\mathrm{Fin}(2))\to \mathbb{R},\\ 0<z\wedge (\forall j:\mathrm{Fin}(2),0<p_j)\Rightarrow \\ (\forall j:\mathrm{Fin}(2),0<u(z,p{)}_j)\wedge \\ (\forall i:\mathrm{Fin}(2),j:\mathrm{Fin}(2),0<K(z,p{)}_{ij})\wedge \\ \exists {\lambda }_1:\mathbb{R},{\lambda }_2:\mathbb{R},0<{\lambda }_1\wedge {\lambda }_1<q(z,p)\wedge 0<{\lambda }_2\wedge {\lambda }_2<q(z,p)\wedge \\ \exists S:\mathrm{Matrix}(\mathrm{Sum}(\mathrm{Fin}(2),\mathrm{Fin}(1)),\mathrm{Sum}(\mathrm{Fin}(2),\mathrm{Fin}(1)),\mathbb{R}),\mathrm{IsUnit}(\det (S))\wedge \\ Q(z,p)S=S\mathrm{fromBlocks}(\mathrm{diagonal}(![{\lambda }_1,{\lambda }_2]),0,0,\mathrm{const}(q(z,p))).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/QuantumContext/SingularSupportCandidateDiagonalizable.singular_support_candidate_positive_and_diagonalizable (✓ std3). ∎

Source. Repository-derived.

Commentary.

For each component, eliminating the radial factor gives the displayed two-coordinate positivity identity. The ratio of the two diagonal normalizations is strictly below the corresponding square-root bound, which makes both residual components positive.

The unnormalized support block is positive definite. Conjugating it by the positive square root of the normalization gives a real symmetric positive-definite matrix. Its spectral decomposition supplies two positive eigenvalues and an invertible eigenbasis for K.

The identity Kp+zu=qp makes every weighted row sum strictly smaller than q. Applying the maximum-ratio argument to an eigenvector places both support eigenvalues below q.

Adjoining p/z to the support eigenbasis gives the explicit upper-triangular block change of basis. The relation Kp+zu=qp proves the final column equation, and invertibility follows because the change of basis is block upper-triangular with invertible diagonal blocks.

References

• Truth anchor: D5/S3/QuantumContext/SingularSupportCandidateDiagonalizable.H
• Truth anchor: D5/S3/QuantumContext/SingularSupportCandidateDiagonalizable.K
• Truth anchor: D5/S3/QuantumContext/SingularSupportCandidateDiagonalizable.Q
• Truth anchor: D5/S3/QuantumContext/SingularSupportCandidateDiagonalizable.gZero
• Truth anchor: D5/S3/QuantumContext/SingularSupportCandidateDiagonalizable.q
• Truth anchor: D5/S3/QuantumContext/SingularSupportCandidateDiagonalizable.r
• Truth anchor: D5/S3/QuantumContext/SingularSupportCandidateDiagonalizable.singular_support_candidate_positive_and_diagonalizable
• Truth anchor: D5/S3/QuantumContext/SingularSupportCandidateDiagonalizable.u