Linear coefficient budget after doubling an added denominator

Disproved

RybinAI2026.P01.crossIntegral_add_double_l1_coefficients

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

integral-inequalitymatrix-analysispositive-definite-matriceszonoids

Let $A$ and $B$ be real symmetric positive-definite matrices of the same finite size. Then there should exist nonnegative constants $p$ and $q$ , depending only on $A$ and $B$ , with

p+q\leq1,

such that doubling the added denominator gives the uniform contractions

K_{A+2B,P}(M)\leq pK_{A,P}(M),\qquad K_{2A+B,P}(M)\leq qK_{B,P}(M)

for every matrix numerator $M=X-Y$ and every positive-definite other denominator $P$ . The same constants satisfy the corresponding inequalities when $A+2B$ and $2A+B$ occur in the second sphere variable. Here $K$ denotes the mission's mixed spherical integral with its original unnormalized surface measure.

This is a strengthened one-sphere coefficient formulation for the matrix-integral addition problem. Together with midpoint log-convexity along the denominator ray, its linear budget produces square-summable contraction coefficients for $A+B$ .

Formalization Note Lean writes $A+2B$ as ((A+B)+B) and $2A+B$ as ((A+B)+A). The statement also covers dimension zero.

Preamble

import Definitions.Def_rybin2026_p01_cross_integral

set_option autoImplicit false

open Matrix RybinAI2026.P01

Formal statement

theorem RybinAI2026.P01.crossIntegral_add_double_l1_coefficients
    {n : ℕ} (A B : Matrix (Fin n) (Fin n) ℝ)
    (hA : A.PosDef) (hB : B.PosDef) :
    ∃ p q : ℝ,
      0 ≤ p ∧ 0 ≤ q ∧ p+q ≤ 1 ∧
      ∀ (X Y P : Matrix (Fin n) (Fin n) ℝ), P.PosDef →
        (crossIntegral X Y ((A+B)+B) P ≤ p*crossIntegral X Y A P) ∧
        (crossIntegral X Y ((A+B)+A) P ≤ q*crossIntegral X Y B P) ∧
        (crossIntegral X Y P ((A+B)+B) ≤ p*crossIntegral X Y P A) ∧
        (crossIntegral X Y P ((A+B)+A) ≤ q*crossIntegral X Y P B) := by
  sorry

Source

Derived one-sphere strengthening for CUHK-Shenzhen AI Math Problems, Problem 1 (Prof. Cosme Louart), https://rybindmitry.github.io/problems/1.html; introduced as the remaining coefficient budget after the proved Prove2Me theorem RybinAI2026.P01.crossIntegral_add_logConvex (02cf0844-154e-494e-ad1e-1c75cffc0605).

View graph