No-W remainder as a convex interpolation

Proved

RybinAI2026.P01.fourWaySlack_noW_interpolation

by WillR · Sep 29, 2026 · Mathlib c5ea003 (Lean v4.30.0)

harmonic-meanintegral-inequalitymatrix-analysispositive-definite-matrices

Let p=ab/(a+b), q=cd/(c+d), U=ab-x(a+b), V=cd-y(c+d), and W=xy-k(x+y), with denominators nonzero. The exact remainder after omitting only the final W term obeys the cleared identity (P-RnoW)(p+q)=S(xy+k(p+q-x-y)); equivalently the associated no-W bound is k+W/(p+q)=(1-alpha)k+alpha*xy/(x+y), where alpha=(x+y)/(p+q). For the matrix application, p and q are the two parallel-sum corners, so this isolates the final harmonic variance penalty without asserting the global budget.

Preamble

import Definitions.Def_rybin2026_p01_matrix_integral
import Definitions.Def_rybin2026_p01_cross_integral

open Matrix RybinAI2026.P01
open scoped BigOperators

Formal statement

namespace RybinAI2026.P01

/-- The four-way remainder with the final W term omitted reduces to a convex interpolation between k and the final harmonic envelope. -/
theorem fourWaySlack_noW_interpolation (a b c d x y k p q U V : ℝ)
    (hp : a*b = p*(a+b)) (hq : c*d = q*(c+d))
    (hU : U = a*b - x*(a+b)) (hV : V = c*d - y*(c+d))
    (hpq : p+q ≠ 0) (hxy : x+y ≠ 0) :
    (a*b*c*d - (V*(a+b)*(x-k) + U*(c+d)*(y-k) + U*V)) * (p+q) =
        (b*c*d + a*c*d + a*b*d + a*b*c) * (x*y + k*(p+q-x-y)) ∧
      k + (x*y-k*(x+y))/(p+q) =
        (1-(x+y)/(p+q))*k + ((x+y)/(p+q))*(x*y/(x+y)) := by
  sorry

end RybinAI2026.P01

Source

CUHK-Shenzhen AI Math Problems, Problem 1; exact algebraic consequence of the accepted fourWaySlack_ledger and fourWaySlack_ledger_col identities in the P01 matrix-integral mission.

View graph