Quarter-turn converts a directional integral to its adjugate

Proved

RybinAI2026.P01.directionalIntegral2_quarterTurn

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

adjugateintegral-inequalitymatrix-analysisp01quarter-turn

For a symmetric real 2x2 matrix M, rotating the directional vector by the quarter-turn J transfers that rotation to the quadratic form as the explicit adjugate: F_M(Je)=F_adj2(M)(e), with F defined by the P01 sphere surface measure.

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 directionalIntegral2_quarterTurn (M : Matrix (Fin 2) (Fin 2) ℝ)
    (e : Euclidean 2) (hM : M.transpose = M) :
    directionalIntegral2 M (quarterTurn2 e) = directionalIntegral2 (adj2 M) e := by
  sorry
end RybinAI2026.P01

Source

P01 mission c36fd4df-ef29-4fbc-9bb6-1f6acf3c0733, root 8d67c9ac-a6c7-418c-b8db-0bc029c18484. This is the exact directional-integral change-of-variables statement needed to reduce orthogonal pair contraction in dimension two to one direction.

View graph