Integer-Gram residual beyond isometry mixtures and the canonical diagonal family

Open

RybinAI2026.P01.matrix_integral_inequality_integer_gram_orbit_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.

Additionally, assume there is no coordinate permutation $\pi$ such that either

D=A,\quad B=A^{\pi},\quad C^{\pi}=C,

C=B,\quad A=B^{\pi},\quad D^{\pi}=D,

where $X^{\pi}_{ij}=X_{\pi^{-1}(i),\pi^{-1}(j)}$ .

Two further classes are excluded. Write $M=(A+B)-(C+D)$ and $\beta_H(u,v)=u^{\mathsf T}Hv$ .

First, assume that there are no real-linear Euclidean isometry $e$ and real number $t\in[0,1]$ for which either of the following alternatives holds for every $u,v\in\mathbb R^n$ :

\beta_B(eu,eu)=\beta_B(u,u),\qquad \beta_M(u,v)=t\beta_{B-D}(u,v)+(1-t)\beta_{B-D}(eu,v),

\beta_A(eu,eu)=\beta_A(u,u),\qquad \beta_M(u,v)=t\beta_{A-C}(u,v)+(1-t)\beta_{A-C}(eu,v).

The isometry acts only on the first variable in the second numerator term. This is a sufficient certificate for the matrix inequality; it is not invariance under arbitrary invertible congruence.

Second, assume that there are no real parameters $a,d\ge1$ for which $n=2$ and the matrices, in the displayed coordinate order, are

A=\operatorname{diag}(1,a),\quad B=\operatorname{diag}(a,1),\quad C=I_2,\quad D=\operatorname{diag}(1,d).

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 condition of the preceding integer-Gram residual, including the small-regularizer, scalar-threshold, noncollinearity, uniform-ratio, and crossed-permutation exclusions, and adds precisely the two exclusions stated above. Those excluded cases are covered by the proved isometry-mixture criterion and the proved canonical two-parameter diagonal family. The remaining assertion is not a completed proof of the unrestricted matrix inequality, and failure of a sufficient certificate is not a counterexample.

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_orbit_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)) →
    (¬ (∃ e : Equiv.Perm (Fin n),
      (D = A ∧ B = Matrix.reindex e e A ∧ Matrix.reindex e e C = C) ∨
      (C = B ∧ A = Matrix.reindex e e B ∧ Matrix.reindex e e D = D))) →
    (¬ (∃ e : Euclidean n ≃ₗᵢ[ℝ] Euclidean n, ∃ t : ℝ, 0 ≤ t ∧ t ≤ 1 ∧
      (((∀ u : Euclidean n, bilinear B (e u) (e u) = bilinear B u u) ∧
        (∀ u v : Euclidean n,
          bilinear ((A+B)-(C+D)) u v =
            t * bilinear (B-D) u v + (1-t) * bilinear (B-D) (e u) v)) ∨
       ((∀ u : Euclidean n, bilinear A (e u) (e u) = bilinear A u u) ∧
        (∀ u v : Euclidean n,
          bilinear ((A+B)-(C+D)) u v =
            t * bilinear (A-C) u v + (1-t) * bilinear (A-C) (e u) v))))) →
    (¬ (∃ a d : ℝ, 1 ≤ a ∧ 1 ≤ d ∧ n = 2 ∧
      A = Matrix.diagonal (fun i : Fin n => if (i : ℕ) = 0 then 1 else a) ∧
      B = Matrix.diagonal (fun i : Fin n => if (i : ℕ) = 0 then a else 1) ∧
      C = 1 ∧
      D = Matrix.diagonal (fun i : Fin n => if (i : ℕ) = 0 then 1 else d))) →
    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/5eeb8f77-365d-4cad-844c-4b03a7ce50ea additionally excluding the stated isometry-mixture certificates and canonical two-parameter diagonal family. Derived open reduction target, not an independently proved source theorem.

View graph