Compression rigidity on arbitrary complex Hilbert spaces
OpenRybinAI2026.P02Hilbert.hilbert_compression_rigidityLet be any complete complex Hilbert space and let be continuous and strictly convex. Let be commuting positive contractions on , and let be an orthogonal projection for which and commute. With the joint continuous functional calculus, the proposed assertion is
This is the arbitrary-complex-Hilbert-space compression question, not just its finite-dimensional matrix instance. It includes the zero space and the projections zero and identity; no assumption that is made. All compressed operators act on the original space , and both outer projections on the right are retained.
Formalization Note. The function is stored on the ambient real plane but only its restriction to the square is used. Joint evaluation is defined by classical choice from continuous unital real star-algebra homomorphisms with the specified coordinate images, or zero when no representation exists. The standard existence-and-uniqueness theorem for commuting positive contractions justifies this representation. Its separate formal statement is supplied as a supporting obligation; neither that lemma nor the open rigidity claim is asserted to have a completed Lean proof here.
import Definitions.Def_rybin2026_p02_joint_calculus_hilbert
namespace RybinAI2026.P02Hilbert
/-- Strict Jensen equality for the joint continuous functional calculus on an arbitrary
complex Hilbert space forces the projection to reduce both coordinate operators. -/
theorem hilbert_compression_rigidity
(H : Type*) [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]
(f : (Fin 2 → ℝ) → ℝ) (hf : ContinuousOn f unitSquare)
(hstrict : StrictConvexOn ℝ unitSquare f)
(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 (restrictFunction f hf) * P =
P * jointCFC (P * X * P) (P * Y * P) (restrictFunction f hf) * P) :
P * X = X * P ∧ P * Y = Y * P := by
sorry
end RybinAI2026.P02Hilbert