Problem 02 definitions — Equality case for compressed convex functional calculus

unitSquare. This is the subset of functions $x:\{0,1\}\to\mathbb R$ lying pointwise between the constant functions $0$ and $1$; equivalently,

$$\operatorname{unitSquare} =\left\{x:\{0,1\}\to\mathbb R\ \middle|\ 0\le x(0)\le1\ \text{and}\ 0\le x(1)\le1\right\}.$$

JointSpectralData. For every natural number $n$, including $n=0$, a value of $\operatorname{JointSpectralData}(n)$ consists of a complex $n\times n$ matrix $U$, proofs of both $U^{*}U=I_n$ and $UU^{*}=I_n$, and a function assigning to every $i\in\{0,\ldots,n-1\}$ a pair $\lambda_i:\{0,1\}\to\mathbb R$ such that $0\le\lambda_i(0)\le1$ and $0\le\lambda_i(1)\le1$. Here $U^{*}$ is the conjugate transpose. When $n=0$, the matrices and spectral function have empty index sets, and the spectral bounds are vacuous.

JointSpectralData.operator. Given any natural number $n$, joint spectral data with unitary matrix $U$ and spectral pairs $\lambda_i\in[0,1]^2$, and a coordinate $c\in\{0,1\}$, the associated complex $n\times n$ matrix is defined by

$$X_c =U\,\operatorname{diag}\!\bigl((\lambda_i(c))_{i=0}^{n-1}\bigr)\,U^{*},$$

where each real number $\lambda_i(c)$ is regarded as a complex number and the displayed diagonal matrix has zero off-diagonal entries. For $n=0$, this is the unique empty $0\times0$ matrix.

JointSpectralData.functional. Given any natural number $n$, joint spectral data with unitary matrix $U$ and spectral pairs $\lambda_i\in[0,1]^2$, and an arbitrary total function $f:\mathbb R^{\{0,1\}}\to\mathbb R$, the associated complex $n\times n$ matrix is defined by

$$f(S) =U\,\operatorname{diag}\!\bigl((f(\lambda_i))_{i=0}^{n-1}\bigr)\,U^{*},$$

with each real value $f(\lambda_i)$ regarded as complex. No continuity, measurability, boundedness, or other regularity condition is imposed on $f$. For $n=0$, the result is the unique empty $0\times0$ matrix.

IsOrthogonalProjection. For every natural number $n$, including $0$, and every complex $n\times n$ matrix $P$, the proposition $\operatorname{IsOrthogonalProjection}(P)$ means exactly the conjunction

$$P^{*}=P \qquad\text{and}\qquad P^2=P.$$

Thus it requires both self-adjointness and idempotence. In dimension $0$, the unique empty matrix satisfies both equalities.

Reduces. For every natural number $n$, including $0$, and arbitrary complex $n\times n$ matrices $P$ and $X$, the proposition $\operatorname{Reduces}(P,X)$ means exactly

$$PX=XP.$$

This definition itself does not require $P$ to be a projection or impose any other condition on either matrix. In dimension $0$, the equality holds automatically.

CompressionWitness. Fix any natural number $n$, joint spectral data $S$ with unitary matrix $U$ and spectral pairs $\lambda_i\in[0,1]^2$, and an arbitrary complex $n\times n$ matrix $P$. A compression witness consists of another joint spectral-data record with a complex matrix $V$ and pairs $\mu_i\in[0,1]^2$, satisfying $V^{*}V=I_n$ and $VV^{*}=I_n$, together with the two equalities

$$V\,\operatorname{diag}\!\bigl((\mu_i(0))_{i=0}^{n-1}\bigr)V^{*} = P\!\left(U\,\operatorname{diag}\!\bigl((\lambda_i(0))_{i=0}^{n-1}\bigr)U^{*}\right)P$$

and

$$V\,\operatorname{diag}\!\bigl((\mu_i(1))_{i=0}^{n-1}\bigr)V^{*} = P\!\left(U\,\operatorname{diag}\!\bigl((\lambda_i(1))_{i=0}^{n-1}\bigr)U^{*}\right)P.$$

The parameter $P$ is not required here to be self-adjoint, idempotent, or commuting with either matrix; the factor on both sides of each compressed operator is $P$ itself. No relationship between $(V,\mu_i)$ and $(U,\lambda_i)$ is required beyond the two displayed matrix equalities. When $n=0$, all indexing data are empty and both equalities are automatic.

import Mathlib

open Matrix Set
open scoped ComplexConjugate Matrix

namespace RybinAI2026.P02

/-- The square `[0,1]²`, represented as functions on a two-element type. -/
def unitSquare : Set (Fin 2 → ℝ) := Icc 0 1

/-- Simultaneous spectral data for two commuting positive contractions in finite dimension. -/
structure JointSpectralData (n : ℕ) where
  unitary : Matrix (Fin n) (Fin n) ℂ
  unitary_left : unitaryᴴ * unitary = 1
  unitary_right : unitary * unitaryᴴ = 1
  spectrum : Fin n → Fin 2 → ℝ
  spectrum_mem : ∀ i, spectrum i ∈ unitSquare

/-- The operator with coordinate `c` in a simultaneous diagonalization. -/
noncomputable def JointSpectralData.operator {n : ℕ} (S : JointSpectralData n)
    (c : Fin 2) : Matrix (Fin n) (Fin n) ℂ :=
  S.unitary * diagonal (fun i => (S.spectrum i c : ℂ)) * S.unitaryᴴ

/-- Joint continuous functional calculus in the supplied common eigenbasis. -/
noncomputable def JointSpectralData.functional {n : ℕ} (S : JointSpectralData n)
    (f : (Fin 2 → ℝ) → ℝ) : Matrix (Fin n) (Fin n) ℂ :=
  S.unitary * diagonal (fun i => (f (S.spectrum i) : ℂ)) * S.unitaryᴴ

/-- A self-adjoint idempotent matrix. -/
def IsOrthogonalProjection {n : ℕ} (P : Matrix (Fin n) (Fin n) ℂ) : Prop :=
  Pᴴ = P ∧ P * P = P

/-- A projection reduces an operator exactly when it commutes with it. -/
def Reduces {n : ℕ} (P X : Matrix (Fin n) (Fin n) ℂ) : Prop :=
  P * X = X * P

/-- A simultaneous diagonalization of the two compressed operators. -/
structure CompressionWitness {n : ℕ} (S : JointSpectralData n)
    (P : Matrix (Fin n) (Fin n) ℂ) where
  compressed : JointSpectralData n
  first_eq : compressed.operator 0 = P * S.operator 0 * P
  second_eq : compressed.operator 1 = P * S.operator 1 * P

end RybinAI2026.P02