Rank-one pair-contraction bound for the P01 kernel

Proved

RybinAI2026.P01.rank_one_pair_contraction_kernel_bound

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

integral-inequalitymatrix-analysispair-contractionrank-one

For positive-definite matrices with symmetric rank-one differences along directions e and f, suppose the exact P01 directional integrals satisfy the two pair-contraction inequalities for (A,B) and (C,D). Then the P01 distance after componentwise addition is bounded by the maximum of the two native distances. This is the Cauchy/factorization reduction that turns a directional pair-contraction theorem into a genuine restricted instance of the mission root.

Preamble

import Mathlib
import Definitions.Def_rybin2026_p01_matrix_integral
import Definitions.Def_rybin2026_p01_cross_integral
import Theorems.Thm_RybinAI2026_P01_pair_dot_le_one
import Theorems.Thm_RybinAI2026_P01_crossIntegral_factor_of_bilinear_factor
import Theorems.Thm_RybinAI2026_P01_crossIntegral_triangle_split

open Matrix MeasureTheory Metric RybinAI2026.P01

Formal statement

theorem RybinAI2026.P01.rank_one_pair_contraction_kernel_bound {n : ℕ}
    (A B C D : Matrix (Fin n) (Fin n) ℝ) (e f : Euclidean n) (r s : ℝ)
    (hA : A.PosDef) (hB : B.PosDef) (hC : C.PosDef) (hD : D.PosDef)
    (hAB : (A + B).PosDef) (hCD : (C + D).PosDef)
    (hfacN : ∀ u v : sphere (0 : Euclidean n) 1,
      bilinear (A - C) u.1 v.1 =
        r * dotProduct (fun i => u.1 i) (fun i => e i) *
            dotProduct (fun i => v.1 i) (fun i => e i))
    (hfacM : ∀ u v : sphere (0 : Euclidean n) 1,
      bilinear (B - D) u.1 v.1 =
        s * dotProduct (fun i => u.1 i) (fun i => f i) *
            dotProduct (fun i => v.1 i) (fun i => f i))
    (F : Matrix (Fin n) (Fin n) ℝ → Euclidean n → ℝ)
    (hF : ∀ M g, F M g =
      ∫ u : sphere (0 : Euclidean n) 1,
        |dotProduct (fun i => u.1 i) (fun i => g i)| /
          bilinear M u.1 u.1 ∂surfaceMeasure n)
    (hFAe : 0 < F A e) (hFBe : 0 < F B e)
    (hFCe : 0 < F C e) (hFDe : 0 < F D e)
    (hFABe : 0 < F (A + B) e) (hFABf : 0 < F (A + B) f)
    (hFCDe : 0 < F (C + D) e) (hFCDf : 0 < F (C + D) f)
    (hpairAB : (F (A + B) e / F A e) ^ 2 +
        (F (A + B) f / F B f) ^ 2 ≤ 1)
    (hpairCD : (F (C + D) e / F C e) ^ 2 +
        (F (C + D) f / F D f) ^ 2 ≤ 1) :
    distance (A + B) (C + D) ≤ max (distance A C) (distance B D) := by
  sorry

Source

Exact reduction of the P01 root for two symmetric rank-one numerator differences, using the Proved pair_dot_le_one, crossIntegral_factor_of_bilinear_factor, and crossIntegral_triangle_split theorems. This isolates the remaining analytic obligation to the two directional pair-contraction inequalities (mission c36fd4df-ef29-4fbc-9bb6-1f6acf3c0733, root 8d67c9ac-a6c7-418c-b8db-0bc029c18484).

View graph