Documentation

Formalizations.MusicTheory.DiatonicExtremality

The diatonic maximizes the fifth Fourier coefficient and minimizes convex energies #

Among the 7-subsets of ℤ/12, the diatonic collection maximizes ‖Ahat A 5‖, with value 2 + √3 = sin (7π/12) / sin (π/12), and the maximizers are exactly its twelve transpositions (Huddling through the multiplication by 5). It also minimizes every all-pairs energy with convex V decreasing at the top, uniquely under strict hypotheses, so the two extremal problems have the same solutions.

Main results #

References #

source
def MusicTheory.DiatonicExtremality.Admissible (V : ℕ → ℝ) :
Prop

Weak discrete convexity on distances 1,...,6 and the decreasing upper boundary.

Equations
Instances For
    source
    def MusicTheory.DiatonicExtremality.StrictAdmissible (V : ℕ → ℝ) :
    Prop

    The strict hypotheses needed to identify the equality class.

    Equations
    Instances For
      source
      @[simp]
      theorem MusicTheory.DiatonicExtremality.diatonic_card :
      AllPairsEvenness.D.card = 7
      source
      theorem MusicTheory.DiatonicExtremality.m5_diatonic :
      Huddling.m5 AllPairsEvenness.D = Fourier.tpose 7 (Huddling.arc 7)

      M5 sends the diatonic to a consecutive seven-note collection, transposed by seven.

      source
      theorem MusicTheory.DiatonicExtremality.fifthArc_to_diatonic :
      Fourier.tpose 11 (Huddling.fifthArc 7) = AllPairsEvenness.D
      source
      theorem MusicTheory.DiatonicExtremality.fifthArc_seven_orbit :
      Huddling.orbitT (Huddling.fifthArc 7) = AllPairsEvenness.orbitTI

      A seven-note fifth chain and the diatonic have exactly the same transposition/TI orbit.

      source
      theorem MusicTheory.DiatonicExtremality.diatonic_mem_orbit :
      AllPairsEvenness.D ∈ AllPairsEvenness.orbitTI
      source
      theorem MusicTheory.DiatonicExtremality.reference_power_eq :
      (Fourier.powerSpec (Huddling.fifthArc 7) 5).re = (Fourier.powerSpec AllPairsEvenness.D 5).re
      source
      theorem MusicTheory.DiatonicExtremality.diatonic_spectral_max (A : Finset (ZMod 12)) (hA : A.card = 7) :
      (Fourier.powerSpec A 5).re ≤ (Fourier.powerSpec AllPairsEvenness.D 5).re

      Among all seven-note collections, the diatonic maximizes the fifth Fourier power.

      source
      theorem MusicTheory.DiatonicExtremality.diatonic_spectral_unique (A : Finset (ZMod 12)) (hA : A.card = 7) :
      (Fourier.powerSpec A 5).re = (Fourier.powerSpec AllPairsEvenness.D 5).re ↔ A ∈ AllPairsEvenness.orbitTI

      The spectral equality class is precisely the twelve diatonic transpositions.

      source
      theorem MusicTheory.DiatonicExtremality.diatonic_power_value :
      (Fourier.powerSpec AllPairsEvenness.D 5).re = 7 + 4 * √3
      source
      theorem MusicTheory.DiatonicExtremality.diatonic_norm_value :
      ‖Fourier.Ahat AllPairsEvenness.D 5‖ = 2 + √3

      The familiar exact diatonic magnitude: |a5| = 2 + sqrt(3).

      source
      theorem MusicTheory.DiatonicExtremality.diatonic_sine_ratio_value :
      Real.sin (Real.pi * 7 / 12) / Real.sin (Real.pi / 12) = 2 + √3

      Euler's sine ratio equals the exact seven-note constant used by the library.

      source
      theorem MusicTheory.DiatonicExtremality.pentatonic_sine_ratio_value :
      Real.sin (Real.pi * 5 / 12) / Real.sin (Real.pi / 12) = 2 + √3

      Five- and seven-note maxima share one constant by sine complementation.

      source
      theorem MusicTheory.DiatonicExtremality.diatonic_norm_max (A : Finset (ZMod 12)) (hA : A.card = 7) :
      ‖Fourier.Ahat A 5‖ ≤ 2 + √3
      source
      theorem MusicTheory.DiatonicExtremality.diatonic_norm_unique (A : Finset (ZMod 12)) (hA : A.card = 7) :
      ‖Fourier.Ahat A 5‖ = 2 + √3 ↔ A ∈ AllPairsEvenness.orbitTI
      source
      def MusicTheory.DiatonicExtremality.EnergyCertificate (A : Finset (ZMod 12)) :
      Prop

      Finite input to the symbolic Abel engine, bundled so interval counts are shared.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[instance_reducible]
        instance MusicTheory.DiatonicExtremality.instDecidableEnergyCertificate (A : Finset (ZMod 12)) :
        Decidable (EnergyCertificate A)
        Equations
        source
        theorem MusicTheory.DiatonicExtremality.energy_census (A : Finset (ZMod 12)) :
        A ∈ Finset.powersetCard 7 Finset.univ → EnergyCertificate A

        Exact seven-note census for the energy proof, assembled from the censuses of AllPairsEvenness.

        source
        theorem MusicTheory.DiatonicExtremality.orbit_card (A : Finset (ZMod 12)) :
        A ∈ AllPairsEvenness.orbitTI → A.card = 7
        source
        theorem MusicTheory.DiatonicExtremality.seven_mem (A : Finset (ZMod 12)) (hA : A.card = 7) :
        A ∈ Finset.powersetCard 7 Finset.univ
        source
        theorem MusicTheory.DiatonicExtremality.diatonic_energy_min (V : ℕ → ℝ) (hV : Admissible V) (A : Finset (ZMod 12)) (hA : A.card = 7) :
        AllPairsEvenness.E V AllPairsEvenness.D ≤ AllPairsEvenness.E V A

        Every weakly admissible potential has the diatonic as an all-pairs ground state.

        source
        theorem MusicTheory.DiatonicExtremality.diatonic_energy_unique (V : ℕ → ℝ) (hV : StrictAdmissible V) (A : Finset (ZMod 12)) (hA : A.card = 7) :
        AllPairsEvenness.E V AllPairsEvenness.D = AllPairsEvenness.E V A ↔ A ∈ AllPairsEvenness.orbitTI

        With strict convexity/decrease, the energy equality class is the diatonic orbit.

        source
        theorem MusicTheory.DiatonicExtremality.spectral_energy_equivalence (V : ℕ → ℝ) (hV : StrictAdmissible V) (A : Finset (ZMod 12)) (hA : A.card = 7) :
        ‖Fourier.Ahat A 5‖ = 2 + √3 ↔ AllPairsEvenness.E V AllPairsEvenness.D = AllPairsEvenness.E V A

        The connection: the fifth Fourier maximum and every strict convex-energy minimum have exactly the same seven-note equality class.