Remaining integer-Gram matrix inequality beyond uniform-ratio certificates

Open

RybinAI2026.P01.matrix_integral_inequality_integer_gram_ratio_residual

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

integral-inequalitymatrix-analysispositive-definite-matrices

Let $n>0$ , let $m$ be a positive integer, and let $P,Q,R,S$ be integer $n\times n$ matrices. Cast the factors to real matrices and set

A=P^{\mathsf T}P+mI,\quad B=Q^{\mathsf T}Q+mI,\quad C=R^{\mathsf T}R+mI,\quad D=S^{\mathsf T}S+mI.

Let $E$ be the sum of the squares of all entries of all four factors. Assume $m<3E$ . Assume also that no positive scalar $t$ satisfies

(B\succeq tA\ \text{or}\ D\succeq tC)\quad\text{and}\quad (B\preceq tA\ \text{or}\ D\preceq tC),

and that there is no real matrix $M$ and no real scalars $\alpha,\beta$ with $A-C=\alpha M$ and $B-D=\beta M$ .

Finally, assume there are no positive real constants $l,U,r,V$ satisfying all of

lA\preceq B\preceq UA,\qquad rC\preceq D\preceq VC,\qquad \frac{1}{(1+l)(1+r)}+\frac{UV}{(1+U)(1+V)}\leq1.

Then, for the original unnormalized double spherical integral $d$ ,

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

This is an open restricted case of Problem 1. It retains every hypothesis of the existing integer-Gram noncollinear subproblem and additionally excludes the region covered by the uniform-ratio sufficient criterion. It is not a claim that the criterion applies to every positive-definite quadruple, nor a conjecture about arbitrary functions. All matrix comparisons are in Loewner order. Commuting and noncommuting matrices are both allowed when they satisfy the stated conditions.

Preamble

import Definitions.Def_rybin2026_p01_matrix_integral

open Matrix RybinAI2026.P01
open scoped BigOperators

Formal statement

theorem RybinAI2026.P01.matrix_integral_inequality_integer_gram_ratio_residual
    {n : ℕ} (hn : 0 < n) (m : ℤ) (hm : 0 < m)
    (P Q R S : Matrix (Fin n) (Fin n) ℤ)
    (hsmall : (m : ℝ) < 3 * (∑ i : Fin n, ∑ j : Fin n,
      ((P i j : ℝ)^2 + (Q i j : ℝ)^2 + (R i j : ℝ)^2 + (S i j : ℝ)^2))) :
    let p : Matrix (Fin n) (Fin n) ℝ := P.map (fun q : ℤ => (q : ℝ))
    let q : Matrix (Fin n) (Fin n) ℝ := Q.map (fun q : ℤ => (q : ℝ))
    let r : Matrix (Fin n) (Fin n) ℝ := R.map (fun q : ℤ => (q : ℝ))
    let s : Matrix (Fin n) (Fin n) ℝ := S.map (fun q : ℤ => (q : ℝ))
    let A := p.transpose * p + (m : ℝ) • 1
    let B := q.transpose * q + (m : ℝ) • 1
    let C := r.transpose * r + (m : ℝ) • 1
    let D := s.transpose * s + (m : ℝ) • 1
    (¬ ∃ t : ℝ, 0 < t ∧
      ((B - t • A).PosSemidef ∨ (D - t • C).PosSemidef) ∧
      ((t • A - B).PosSemidef ∨ (t • C - D).PosSemidef)) →
    (¬ ∃ M : Matrix (Fin n) (Fin n) ℝ, ∃ α β : ℝ,
      A-C = α • M ∧ B-D = β • M) →
    (¬ (∃ l U r V : ℝ, 0 < l ∧ 0 < U ∧ 0 < r ∧ 0 < V ∧
      (B - l • A).PosSemidef ∧ (U • A - B).PosSemidef ∧
      (D - r • C).PosSemidef ∧ (V • C - D).PosSemidef ∧
      1 / ((1+l)*(1+r)) + U*V / ((1+U)*(1+V)) ≤ 1)) →
    distance (A + B) (C + D) ≤ max (distance A C) (distance B D) := by
  sorry

Source

https://rybindmitry.github.io/problems/1.html, Problem 1; restriction of https://prove2.me/theorems/a900d293-0b59-4345-952e-528f4a81b221 excluding the supplied Section 4 uniform-ratio sufficient condition. Open reduction target, not an independently proved source theorem.

View graph