Imaginary part evaluation of the witness quartet

Proved

KobayashiMaskawa1973.complex_quartet_eval

by Mazecto · Sep 24, 2026 · Mathlib 0df444a (Lean v4.33.1)

complex-analysis

For any real $s$ , the imaginary part of $(1/s)(1/(2s) - i/2) (-1/2)^* (1/2)^*$ equals $1/(8s)$ .

Preamble

import Mathlib

Formal statement

namespace KobayashiMaskawa1973

theorem complex_quartet_eval (s : ℝ) :
    (((1 / s : ℂ) * (1 / (2 * s) - Complex.I / 2) * star (-1/2 : ℂ) * star (1/2 : ℂ))).im = 1 / (8 * s) := by sorry

end KobayashiMaskawa1973

Source

M. Kobayashi and T. Maskawa, Progress of Theoretical Physics 49 (1973) 652-657, pp. 654

View graph