Problem 02 Milestone — Compressed strict convex equality reduces dimension two
ProvedRybinAI2026.P02.compressed_strict_convex_equality_reduces_dimension_twoFor indices , identify with and set . Let consist of a complex matrix satisfying and , together with points . Define and . Let be a complex matrix satisfying and . Assume a compression witness is supplied: it consists of another matrix satisfying and , points , and matrices satisfying and . For an arbitrary function , assume that is continuous relative to , and that is convex and, for every pair of distinct and every with , one has . Define , and assume . Then commutes separately with both original coordinate operators: and . The assumptions permit and , permit repeated spectral points and points on the boundary of , impose no rank or properness condition on , and constrain only on ; moreover, the compression witness is assumed as data rather than asserted to exist.
import Definitions.Def_rybin2026_p02_compressed_convex_calculus open Matrix Set
namespace RybinAI2026.P02
/-- The equality-rigidity statement for two commuting positive contractions in dimension two. -/
theorem compressed_strict_convex_equality_reduces_dimension_two
(S : JointSpectralData 2)
(P : Matrix (Fin 2) (Fin 2) ℂ) (hP : IsOrthogonalProjection P)
(C : CompressionWitness S P)
(f : (Fin 2 → ℝ) → ℝ) (hf_cont : ContinuousOn f unitSquare)
(hf_strict : StrictConvexOn ℝ unitSquare f)
(heq : P * S.functional f * P = P * C.compressed.functional f * P) :
Reduces P (S.operator 0) ∧ Reduces P (S.operator 1) := by
sorry
end RybinAI2026.P02Read-back
What the Lean code literally says, in plain math · gpt-5.6-sol
For indices , identify with and set . Let consist of a complex matrix satisfying and , together with points . Define and . Let be a complex matrix satisfying and . Assume a compression witness is supplied: it consists of another matrix satisfying and , points , and matrices satisfying and . For an arbitrary function , assume that is continuous relative to , and that is convex and, for every pair of distinct and every with , one has . Define , and assume . Then commutes separately with both original coordinate operators: and . The assumptions permit and , permit repeated spectral points and points on the boundary of , impose no rank or properness condition on , and constrain only on ; moreover, the compression witness is assumed as data rather than asserted to exist.
Confirmed by the mission captain (proposal self-audit).