Prove2Me

Quarter-turn reduction of the two-dimensional pair score

Proved
RybinAI2026.P01.pairScore_quarterTurn_eq_sameDirection

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

adjugateintegral-inequalitymatrix-analysisp01pair-contraction

For symmetric P and Q and f=Je, the two-direction pair score equals the same-direction score for P,Q and their explicit adjugates. This uses additivity of 2x2 adjugation and the quarter-turn directional-integral identity.

Preamble
import Mathlib
import Definitions.Def_rybin2026_p01_matrix_integral
import Definitions.Def_rybin2026_p01_adj2

open Matrix RybinAI2026.P01
Formal statement
namespace RybinAI2026.P01
theorem pairScore_quarterTurn_eq_sameDirection (P Q : Matrix (Fin 2) (Fin 2) ℝ)
    (e : Euclidean 2) (hP : P.transpose = P) (hQ : Q.transpose = Q) :
    (directionalIntegral2 (P + Q) e / directionalIntegral2 P e) ^ 2 +
        (directionalIntegral2 (P + Q) (quarterTurn2 e) /
          directionalIntegral2 Q (quarterTurn2 e)) ^ 2 =
      (directionalIntegral2 (P + Q) e / directionalIntegral2 P e) ^ 2 +
        (directionalIntegral2 (adj2 P + adj2 Q) e /
          directionalIntegral2 (adj2 Q) e) ^ 2 := by
  sorry
end RybinAI2026.P01
Source
P01 mission c36fd4df-ef29-4fbc-9bb6-1f6acf3c0733, root 8d67c9ac-a6c7-418c-b8db-0bc029c18484. Exact algebraic connector for the adjugate reduction of the full two-dimensional orthogonal pair-contraction conjecture.

View graph