Diagonal coordinate surface kernels as angle integrals

Proved

RybinAI2026.P01.surface_integral_diagonal_coordinates_eq_angle

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

diagonalintegral-inequalitymatrix-analysispolar-coordinatessurface-measure

For the two coordinate kernels of a positive diagonal quadratic form on the P01 unit circle, the unnormalized surface-measure integrals equal their explicit angular integrals. This is the specialized polar-coordinate bridge needed to apply the already-proved cosine and sine angle evaluations to the P01 diagonal coordinate formula.

Preamble

import Mathlib
import Definitions.Def_rybin2026_p01_matrix_integral

open Matrix MeasureTheory Metric RybinAI2026.P01 Set

Formal statement

theorem RybinAI2026.P01.surface_integral_diagonal_coordinates_eq_angle (a b : ℝ) (ha : 0 < a) (hb : 0 < b) :
    let M : Matrix (Fin 2) (Fin 2) ℝ :=
      Matrix.diagonal (fun i : Fin 2 => if i = 0 then a else b)
    (∫ u : sphere (0 : Euclidean 2) 1,
      |u.1 0| / bilinear M u.1 u.1 ∂surfaceMeasure 2 =
        ∫ θ in (-Real.pi)..Real.pi,
          |Real.cos θ| / (a * Real.cos θ ^ 2 + b * Real.sin θ ^ 2)) ∧
    (∫ u : sphere (0 : Euclidean 2) 1,
      |u.1 1| / bilinear M u.1 u.1 ∂surfaceMeasure 2 =
        ∫ θ in (-Real.pi)..Real.pi,
          |Real.sin θ| / (a * Real.cos θ ^ 2 + b * Real.sin θ ^ 2)) := by
  sorry

Source

Specialization of the planar polar decomposition to the exact two coordinate kernels required by RybinAI2026.P01.directional_integral_diag_coordinate_formula (0555ca46-2e13-4d5d-a97b-45c9aa756ee7), itself a named restricted subcase of the P01 root RybinAI2026.P01.matrix_integral_inequality (mission c36fd4df-ef29-4fbc-9bb6-1f6acf3c0733; target 8d67c9ac-a6c7-418c-b8db-0bc029c18484). It retains the actual surfaceMeasure 2 convention and does not assert an arbitrary-function surface-to-angle theorem.

View graph