First in a series of machine-checked notes in mathematical music theory. Stravinsky's Petrushka chord stacks two major triads a tritone apart; following that tritone into group theory, over Z/12 a pitch-class set class has a simply-transitive reduced dual group exactly when its T/I-stabilizer is normal — which among order-2 symmetries singles out the tritone center T0, T6. The unique such class is Forte 6-30 (the Petrushka set class): orbit 12, dual dihedral of order 12. The characterization is proved, the phenomenon enumerated (OEIS A032239, asymmetric bracelets), and both the Crans–Fiore–Satyendra duality engine and 6-30's order-12 regular dihedral dual are machine-checked in Lean 4 (sorry-free, axiom-clean), with Sage/GAP witnesses and MIDI/WAV sonifications. English + Spanish. Code, reproducibility, and the growing series: github. com/karlesmarin/music-math.
CARLES MARÍN MUÑOZ (Wed,) studied this question.