Matrix-integral inequality for an explicit noncommuting integer-Gram quadruple

Proved

RybinAI2026.P01.matrix_integral_inequality_noncommuting_control

by miao · Sep 8, 2026 · Mathlib c5ea003 (Lean v4.30.0)

integral-inequalitymatrix-analysispositive-definite-matrices

Consider the four real symmetric positive-definite matrices

A=\begin{pmatrix}2&2\\2&6\end{pmatrix},\quad B=\begin{pmatrix}5&-2\\-2&3\end{pmatrix},\quad C=\begin{pmatrix}5&4\\4&6\end{pmatrix},\quad D=\begin{pmatrix}6&-1\\-1&2\end{pmatrix}.

Let $d(X,Y)$ denote the original unnormalized double spherical matrix integral in Problem 1. Then

d(A+B,C+D)\le\max\{d(A,C),d(B,D)\}.

This is a concrete noncommuting instance of the general conjecture: $AB-BA=\begin{pmatrix}0&4\\-4&0\end{pmatrix}$ . The matrices arise as integer Gram matrices plus the identity and have noncollinear differences. The statement concerns this exact quadruple, not arbitrary positive-definite matrices or dimensions.

Preamble

import Definitions.Def_rybin2026_p01_matrix_integral
import Mathlib.LinearAlgebra.Matrix.Notation

open Matrix RybinAI2026.P01

Formal statement

theorem RybinAI2026.P01.matrix_integral_inequality_noncommuting_control :
    let A : Matrix (Fin 2) (Fin 2) ℝ := !![2,2;2,6]
    let B : Matrix (Fin 2) (Fin 2) ℝ := !![5,-2;-2,3]
    let C : Matrix (Fin 2) (Fin 2) ℝ := !![5,4;4,6]
    let D : Matrix (Fin 2) (Fin 2) ℝ := !![6,-1;-1,2]
    distance (A+B) (C+D) ≤ max (distance A C) (distance B D) := by
  sorry

Source

https://rybindmitry.github.io/problems/1.html, Problem 1 and its defining integral. Derived exact instance using integer Gram sample 6 (regularizer 1, reproducible seed 20260909); the source states the general problem, not this separate numerical example.

View graph