The comma kernel of 3-limit regular temperaments

Intervals of the 3-limit are monzos in ℤ × ℤ (exponents of 2 and 3); a val is a linear map ℤ × ℤ →ₗ[ℤ] ℤ; a comma of a val is an element of its kernel. Twelve fifths minus seven octaves is the Pythagorean comma, 12-EDO tempers it, and the comma generates the kernel of the 12-EDO val; 5-EDO and 7-EDO do not temper it. In the 5-limit, 12-EDO tempers the syntonic comma.

Main results

• closure_defect_eq_pc, v12_tempers_pc.
• ker_v12_eq_span_pc: the kernel is spanned by the Pythagorean comma.
• v5_pc, v7_pc.
• v12_5_tempers_syntonic, ker_v12_5_eq_span, meantone_defect_eq_syntonic.

References

• C. Marín, One transform and one duality: a machine-checked core of music theory in Lean 4, Zenodo (2026), doi:10.5281/zenodo.20953767.

Monzos: the 3-limit just-intonation lattice ℤ × ℤ

def MusicTheory.Temperament.fifth : ℤ × ℤ

The perfect fifth 3/2, as a monzo (exp of 2, exp of 3) = (-1, 1).

Equations

• MusicTheory.Temperament.fifth = (-1, 1)

def MusicTheory.Temperament.oct : ℤ × ℤ

The octave 2/1, as a monzo (1, 0).

Equations

• MusicTheory.Temperament.oct = (1, 0)

def MusicTheory.Temperament.pc : ℤ × ℤ

The Pythagorean comma 3^12 / 2^19 = 531441/524288, as a monzo (-19, 12).

Equations

• MusicTheory.Temperament.pc = (-19, 12)

Vals: ℤ-linear "steps per prime" functionals

def MusicTheory.Temperament.v12 : ℤ × ℤ →ₗ[ℤ] ℤ

The 12-EDO patent val ⟨12, 19|: a perfect octave is 12 steps, a perfect twelfth (3/1) is 19 steps, so 2^a·3^b ↦ 12a + 19b.

Equations

• MusicTheory.Temperament.v12 = { toFun := fun (p : ℤ × ℤ) => 12 * p.1 + 19 * p.2, map_add' := ⋯, map_smul' := ⋯ }

def MusicTheory.Temperament.v5 : ℤ × ℤ →ₗ[ℤ] ℤ

The 5-EDO val ⟨5, 8|.

Equations

• MusicTheory.Temperament.v5 = { toFun := fun (p : ℤ × ℤ) => 5 * p.1 + 8 * p.2, map_add' := ⋯, map_smul' := ⋯ }

def MusicTheory.Temperament.v7 : ℤ × ℤ →ₗ[ℤ] ℤ

The 7-EDO val ⟨7, 11|.

Equations

• MusicTheory.Temperament.v7 = { toFun := fun (p : ℤ × ℤ) => 7 * p.1 + 11 * p.2, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem MusicTheory.Temperament.v12_apply (p : ℤ × ℤ) : v12 p = 12 * p.1 + 19 * p.2

@[simp]

theorem MusicTheory.Temperament.v5_apply (p : ℤ × ℤ) : v5 p = 5 * p.1 + 8 * p.2

@[simp]

theorem MusicTheory.Temperament.v7_apply (p : ℤ × ℤ) : v7 p = 7 * p.1 + 11 * p.2

Theorem 1 — the bridge: the comma is the closure defect of the circle of fifths

theorem MusicTheory.Temperament.closure_defect_eq_pc : 12 • fifth - 7 • oct = pc

Twelve stacked fifths minus seven octaves equals the Pythagorean comma. This is the closure defect of the circle of fifths and the bridge to DiatonicScale: it is exactly why stacking the fifth twelve times in ℤ/12 returns to the start (the defect lands in the kernel of the 12-EDO val — see closure_defect_tempered).

Theorem 2 — 12-EDO tempers the Pythagorean comma

theorem MusicTheory.Temperament.v12_tempers_pc : v12 pc = 0

12-EDO tempers out the Pythagorean comma: v12 pc = 12·(-19) + 19·12 = 0.

theorem MusicTheory.Temperament.closure_defect_tempered : v12 (12 • fifth - 7 • oct) = 0

Corollary phrased on the closure defect itself: the defect of the circle of fifths is a comma of 12-EDO. This is the precise reason the ℤ/12 circle of fifths closes.

Theorem 3 — the comma generates the kernel (the only nontrivial proof)

theorem MusicTheory.Temperament.ker_v12_eq_span_pc : v12.ker = ℤ ∙ pc

The Pythagorean comma generates the entire kernel of the 12-EDO val: ker v12 = span_ℤ {pc}. The ⊇ direction is span_le + theorem 2. The ⊆ direction is the Bézout content: if 12a + 19b = 0 then, reducing 19 ≡ 7 (mod 12) and using gcd(7,12)=1, we get 12 ∣ b; writing b = 12t forces a = -19t, i.e. (a,b) = t • pc.

Theorem 4 — 5-EDO and 7-EDO do NOT temper the comma

theorem MusicTheory.Temperament.v5_pc : v5 pc = 1

5-EDO does not temper the Pythagorean comma: v5 pc = 1 ≠ 0.

theorem MusicTheory.Temperament.v7_pc : v7 pc = -1

7-EDO does not temper the Pythagorean comma: v7 pc = -1 ≠ 0.

theorem MusicTheory.Temperament.only_twelve_tempers_pc : v12 pc = 0 ∧ v5 pc ≠ 0 ∧ v7 pc ≠ 0

Restated: 12 is special among 5, 7, 12 — only 12-EDO sends the comma to a unison.

5-limit coda — 12-EDO is a meantone (tempers the syntonic comma)

def MusicTheory.Temperament.v12_5 : ℤ × ℤ × ℤ →ₗ[ℤ] ℤ

The 12-EDO val in the 5-limit ⟨12, 19, 28| on the monzo lattice ℤ × ℤ × ℤ (primes 2, 3, 5).

Equations

• MusicTheory.Temperament.v12_5 = { toFun := fun (p : ℤ × ℤ × ℤ) => 12 * p.1 + 19 * p.2.1 + 28 * p.2.2, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem MusicTheory.Temperament.v12_5_apply (p : ℤ × ℤ × ℤ) : v12_5 p = 12 * p.1 + 19 * p.2.1 + 28 * p.2.2

def MusicTheory.Temperament.syntonic : ℤ × ℤ × ℤ

The syntonic comma 81/80 = 3^4·5⁻¹·2⁻⁴, as a 5-limit monzo (-4, 4, -1).

Equations

• MusicTheory.Temperament.syntonic = (-4, 4, -1)

theorem MusicTheory.Temperament.v12_5_tempers_syntonic : v12_5 syntonic = 0

12-EDO is a meantone: it tempers out the syntonic comma, 12·(-4) + 19·4 + 28·(-1) = 0.

The rank-2 kernel: the two classical commas GENERATE the 5-limit comma lattice

The completion of the 5-limit kernel picture. Where the 3-limit section gave the rank-1 3-limit fact ker v12 = span_ℤ{pc}, here the kernel of the 5-limit val is rank 2, and the two classical commas — the syntonic comma 81/80 AND the Pythagorean comma 3¹²/2¹⁹ (embedded in the 5-limit, no factor of 5) — TOGETHER generate the whole sublattice of commas 12-EDO tempers out. They genuinely GENERATE (not merely lie in) the kernel because the gcd of the 2×2 minors of the matrix [syntonic; pc5] is gcd(28, −19, 12) = 1, so {syntonic, pc5} is a ℤ-basis of the saturated rank-2 kernel.

def MusicTheory.Temperament.pc5 : ℤ × ℤ × ℤ

The Pythagorean comma embedded in the 5-limit 3¹²/2¹⁹ (no factor of 5), as a 5-limit monzo (-19, 12, 0).

Equations

• MusicTheory.Temperament.pc5 = (-19, 12, 0)

theorem MusicTheory.Temperament.v12_5_tempers_pc5 : v12_5 pc5 = 0

12-EDO tempers the (5-limit) Pythagorean comma: 12·(-19) + 19·12 + 28·0 = 0.

theorem MusicTheory.Temperament.ker_v12_5_eq_span : v12_5.ker = Submodule.span ℤ {syntonic, pc5}

The syntonic and Pythagorean commas generate the entire 5-limit kernel of the 12-EDO val: ker v12_5 = span_ℤ {syntonic, pc5}. This is a genuine rank-2 lattice-generation theorem. The ⊇ direction is span_le + the two tempering facts. The ⊆ direction is a 2D-Bézout content made omega-checkable by explicit witnesses: any tempered comma (a,b,c) with 12a+19b+28c=0 equals (-c)•syntonic + t•pc5 where 12t = b+4c (the divisibility 12 ∣ b+4c follows from the kernel equation mod 12). The witnesses exist because the 2×2-minor gcd is 1 (saturated kernel).

Meantone identity — the syntonic comma is "four fifths vs. a major third"

The defining identity of meantone temperament (Aron 1523; textbook 5-limit RTT): four perfect fifths, reduced by two octaves, exceed the just major third (5/4) by exactly the syntonic comma. Tempering the comma (which 12-EDO does, v12_5_tempers_syntonic) makes the identity exact, which is why a stack of four fifths lands on a major third in any meantone. This is the SECOND great comma of the kernel wing (syntonic, after the Pythagorean pc), and the algebraic seed of triadic harmony.

def MusicTheory.Temperament.fifth5 : ℤ × ℤ × ℤ

The perfect fifth 3/2 as a 5-limit monzo (-1, 1, 0).

Equations

• MusicTheory.Temperament.fifth5 = (-1, 1, 0)

def MusicTheory.Temperament.oct5 : ℤ × ℤ × ℤ

The octave 2/1 as a 5-limit monzo (1, 0, 0).

Equations

• MusicTheory.Temperament.oct5 = (1, 0, 0)

def MusicTheory.Temperament.third5 : ℤ × ℤ × ℤ

The just major third 5/4 as a 5-limit monzo (-2, 0, 1).

Equations

• MusicTheory.Temperament.third5 = (-2, 0, 1)

theorem MusicTheory.Temperament.meantone_defect_eq_syntonic : 4 • fifth5 - third5 - 2 • oct5 = syntonic

The meantone defect is the syntonic comma: four perfect fifths minus a just major third minus two octaves equals 81/80. 4•(-1,1,0) − (-2,0,1) − 2•(1,0,0) = (-4,4,-1) = syntonic. This is the gap between four fifths and a (just) major third plus two octaves.

theorem MusicTheory.Temperament.meantone_identity_tempered : v12_5 (4 • fifth5 - third5 - 2 • oct5) = 0

12-EDO closes the meantone identity: it tempers the four-fifths-vs-major-third defect to a unison. Hence in 12-EDO four fifths (mod octaves) are a major third — the harmonic analog of the circle of fifths closing.