Four-corner harmonic budget for the two numerator differences

Disproved

RybinAI2026.P01.crossIntegral_four_harmonic_budget

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

integral-inequalitymatrix-analysispositive-definite-matrices

Let $A,B,C,D$ be real symmetric positive-definite $n\times n$ matrices. For the fixed numerator difference $N=A-C$ , define the four mixed integrals

a_N=K_N(A,C),\quad b_N=K_N(A,D),\quad c_N=K_N(B,C),\quad d_N=K_N(B,D),

and put

S_N=b_Nc_Nd_N+a_Nc_Nd_N+a_Nb_Nd_N+a_Nb_Nc_N,\qquad P_N=a_Nb_Nc_Nd_N.

Define $a_K,b_K,c_K,d_K,S_K,P_K$ in the same way for the numerator difference $K=B-D$ . Here $K_M(P,Q)$ denotes the mixed spherical integral with numerator $|u^{\mathsf T}Mv|$ and denominator $(u^{\mathsf T}Pu)(v^{\mathsf T}Qv)$ . Then

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

When both differences are nonzero, this says that the sum of their four-corner parallel bounds is at most the larger original distance. Combined with the proved four-way harmonic denominator estimate and numerator subadditivity, it implies the matrix-integral inequality in Problem 1. The cleared statement also includes the degenerate zero-difference and zero-dimensional cases.

Retirement note (2026-09-10). This conjectural strengthening was retired after a reproducible two-dimensional adversarial search found a stable ratio about $1.332>1$ for its parallel-sum form. This is numerical evidence against this auxiliary statement, not a disproof of Problem 1. The valid proved estimate retained in its place is RybinAI2026.P01.crossIntegral_add_four_harmonic; the unresolved intended conclusion remains RybinAI2026.P01.crossIntegral_sum_le_max.

Preamble

import Definitions.Def_rybin2026_p01_cross_integral

open Matrix RybinAI2026.P01

Formal statement

theorem RybinAI2026.P01.crossIntegral_four_harmonic_budget {n : ℕ}
    (A B C D : Matrix (Fin n) (Fin n) ℝ)
    (hA : A.PosDef) (hB : B.PosDef) (hC : C.PosDef) (hD : D.PosDef) :
    let aN := crossIntegral A C A C
    let bN := crossIntegral A C A D
    let cN := crossIntegral A C B C
    let dN := crossIntegral A C B D
    let sN := bN*cN*dN+aN*cN*dN+aN*bN*dN+aN*bN*cN
    let pN := aN*bN*cN*dN
    let aK := crossIntegral B D A C
    let bK := crossIntegral B D A D
    let cK := crossIntegral B D B C
    let dK := crossIntegral B D B D
    let sK := bK*cK*dK+aK*cK*dK+aK*bK*dK+aK*bK*cK
    let pK := aK*bK*cK*dK
    pN*sK+pK*sN ≤ max (distance A C) (distance B D)*sN*sK := by
  sorry

Source

https://rybindmitry.github.io/problems/1.html, Problem 1 and its defining integral. Derived conjectural scalar budget isolated from the proved four-way harmonic denominator estimate; the source states the general problem, not this separate formulation.

View graph