Rigidez da compressão para a função quadrática em Hilbert arbitrário
ProvedRybinAI2026.P02Hilbert.quadratic_compression_rigidityLet be commuting positive contractions on a complete complex Hilbert space , and let be an orthogonal projection such that and commute. For the continuous strictly convex function
suppose the joint continuous functional calculus satisfies
Then
This result is the quadratic case of CUHK-Shenzhen Problem 2, with no restriction on dimension or separability. Both outer factors in the source's equality are preserved. The compressions act on the original space ; the zero space and the zero and identity projections are also included. The statement for an arbitrary continuous strictly convex function is not part of this result.
Formalization note. The function appears as the sum of the squares of the two continuous coordinate functions on the square. The functional calculus is exactly the mission's jointCFC.
import Definitions.Def_rybin2026_p02_joint_calculus_hilbert set_option autoImplicit false open RybinAI2026.P02Hilbert
theorem RybinAI2026.P02Hilbert.quadratic_compression_rigidity
(H : Type*) [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]
(X Y : H →L[ℂ] H) (hX : PositiveContraction X) (hY : PositiveContraction Y)
(hXY : X * Y = Y * X)
(P : H →L[ℂ] H) (hPstar : star P = P) (hPidempotent : P * P = P)
(hCompressedCommute : (P * X * P) * (P * Y * P) = (P * Y * P) * (P * X * P))
(hEquality : P * jointCFC X Y
(coordinate 0 * coordinate 0 + coordinate 1 * coordinate 1) * P =
P * jointCFC (P * X * P) (P * Y * P)
(coordinate 0 * coordinate 0 + coordinate 1 * coordinate 1) * P) :
P * X = X * P ∧ P * Y = Y * P := by sorry