A machine-checked library, in Lean 4 on top of Mathlib, of core results in the mathematics of music theory over the chromatic universe Z₁2, organized so that one object and one phenomenon do most of the work. The object is the autocorrelation, or power spectrum |A-hat|², of a pitch-class set: the interval vector, Babbitt's hexachord theorem, homometry and the Z-relation read as the crystallographic phase problem, deep scales, rhythmic oddity, and the common-tone theorems are all functions of it, and maximal evenness reconnects to it in the scale theory. The phenomenon is duality: the neo-Riemannian PLR group is the centralizer of the regular T/I action on the 24 triads (Crans-Fiore-Satyendra, via the regular case of Wielandt's centralizer theorem, a lemma added over Mathlib), and the same shape recurs as a tritone-centered order-12 self-duality of the Petrushka set class 6-30 and as the val-comma lattice duality of regular temperament theory. The library is organized in three pillars (Fourier invariants of pitch-class sets; transformational duality; scales and tuning), ~275 theorems and lemmas across 9 Lean files, every theorem sorry-free with a clean axiom audit (propext, Classical. choice, Quot. sound; the finite maximal-evenness censuses additionally use nativedecide). The mathematics is classical; the contributions are the formalization itself - the first comprehensive one in this area, since prior proof-assistant work covers only the T/I action - an autocorrelation/DFT organizing lens, and two results that appear not to have been noted in the literature: the 6-30 self-duality and a unified phase taxonomy of the |A-hat|² invariants. This corpus paper is the umbrella over three notes of the Mathematics of Music series (the 6-30 self-duality, the phase taxonomy, the Tonnetz spectrum), adding the connective tissue and the scale-and-tuning pillar. Not new mathematics - a unified, certified account. This record bundles the English and Spanish versions of the paper.
CARLES MARÍN MUÑOZ (Sat,) studied this question.