Counting Melodies: Generating Functions, Regular Languages, and the Combinatorics of Pitch, Duration, and Silence

Christopher Yamba

September 2026

Abstract

We study a deliberately small but musically natural enumeration problem: how many monophonic melodies of fixed total duration can be written when notes carry pitch, rests carry no pitch, durations are integer multiples of a smallest temporal unit, and adjacent rests are identified with the single rest obtained by merging them? The model leads naturally to integer compositions, regular languages, and ordinary generating functions. For a pitch alphabet of size p and unrestricted positive integral event durations, the generating function reduces to a rational function Mp(q)=1−q1−(p+2)q+q2,M_p(q)=\frac{1-q}{1-(p+2)q+q^2}, giving the recurrence an=(p+2)an−1−an−2a_n=(p+2)a_{n-1}-a_{n-2} with a0=1a_0=1 and a1=p+1a_1=p+1. A direct combinatorial formula is also obtained. For a 4/4 bar quantized into sixteen sixteenth-note units and two chromatic octaves (p=24p=24), the model gives 41,006,928,746,285,492,812,22541,006,928,746,285,492,812,225 admissible melodies. We then lift the commutative counting series to a noncommutative formal series that retains individual melodic identity, illustrate the encoding on the subject of Bach’s C-minor fugue BWV 847, and outline a Lean 4 formalization. The purpose of the note is both enumerative and conceptual: to show how a musical notation problem turns into a compact piece of combinatorics.

1. The question

A bar of music looks finite. The staff has a fixed width; a time signature fixes a duration; a chosen smallest note value fixes a temporal grid. Yet even in a monophonic line, the number of possible bars becomes enormous as soon as rhythm, silence, and pitch are allowed to interact.

The point of this note is not to claim that a melody is exhausted by pitch and duration. It plainly is not. Articulation, dynamics, phrasing, harmony, timbre, voice leading, meter, notation, and musical expectation all matter. The point is narrower and, mathematically, cleaner:

Given a fixed amount of time, how many legal monophonic event sequences are possible under a specified set of notation rules?

The problem began from a very concrete representation. Take a 4/4 bar, measure time in sixteenths, and write the bar initially as sixteen atomic temporal units. Grouping consecutive units creates event durations. If order matters, these groupings are compositions rather than partitions. Pitch then colors note events, while rests behave differently: two adjacent rests are not musically distinct from their merged rest in the duration model used here.

That last observation is the small irregularity that makes the problem interesting. Notes may legitimately occur consecutively, even at the same pitch. Rests, in our canonical representation, do not: adjacent rest events are merged.

The resulting structure is simple enough to solve exactly and rich enough to connect three viewpoints:

  1. integer compositions;
  2. regular languages and formal words;
  3. ordinary generating functions.

The same model also has a natural noncommutative refinement in which an individual melody, not merely its count, is retained algebraically.

2. Basic definitions

Fix a smallest temporal unit. In the running example this unit is a sixteenth note.

Let PP be a finite pitch alphabet with

|P|=p. |P|=p.

For two chromatic octaves without duplicating the upper endpoint, for example C4 through B5, one has p=24p=24.

An event is one of two kinds:

A melody is a finite ordered sequence of events satisfying two conditions:

  1. the sum of all event durations is the required total duration nn;
  2. no two rest events are adjacent.

The second condition is a canonicalization rule. A rest of duration 2 followed immediately by a rest of duration 3 is represented instead by one rest of duration 5. Thus every sounding pattern of silence has a unique rest decomposition.

We write an,pa_{n,p} for the number of such melodies of total duration nn with pp available pitches. The empty melody is allowed at duration zero, so

a0,p=1. a_{0,p}=1.

For n=1n=1, there are pp one-unit notes and one one-unit rest:

a1,p=p+1. a_{1,p}=p+1.

3. Duration alone: compositions

Before pitch and silence are introduced, consider only durations.

A composition of a positive integer nn is an ordered sequence of positive integers

(d1,d2,…,dm) (d_1,d_2,\ldots,d_m)

such that

d1+d2+⋯+dm=n. d_1+d_2+\cdots+d_m=n.

For example, the compositions of 44 are

4,3+1,1+3,2+2, 4, \quad 3+1, \quad 1+3, \quad 2+2,

2+1+1,1+2+1,1+1+2,1+1+1+1. 2+1+1, \quad 1+2+1, \quad 1+1+2, \quad 1+1+1+1.

There are 2n−12^{n-1} compositions of nn. The familiar proof uses the n−1n-1 internal gaps between nn atomic units. At each gap we choose either to retain a separator or remove it. Thus a composition corresponds bijectively to a subset of the set of internal gaps.

Musically, the composition is the duration skeleton. It says how a fixed time span is partitioned into consecutive events before we decide which events are notes, which are rests, and which pitches the notes carry.

For a 4/4 bar quantized into sixteenths, n=16n=16, so duration alone gives

215=32768 2^{15}=32768

ordered duration skeletons.

That is only the first layer.

4. A formal-language description

Let NN denote the class of single note events and RR the class of single rest events. Let ε\varepsilon denote the empty word.

A legal melody has a unique decomposition

(ε+R)(N(ε+R))*. \boxed{(\varepsilon+R)\bigl(N(\varepsilon+R)\bigr)^*.}

This expression is worth reading literally.

This construction permits

N,NN,NR,RN,NRN,RNR,… N,\quad NN,\quad NR,\quad R N,\quad NRN,\quad RNR,\ldots

but never permits RRRR.

The role of the three appearances of an empty choice should not be conflated. The optional initial rest has an empty alternative; the optional rest after a note has an empty alternative; and the Kleene star has its own zero-repetition case. At the language level the empty object is ε\varepsilon. Only after passing to generating functions does its weight become the scalar 1=q01=q^0.

Lemma 1. Unique block decomposition

Every legal melody has a unique representation in the language

(ε+R)(N(ε+R))*. (\varepsilon+R)\bigl(N(\varepsilon+R)\bigr)^*.

Proof. If a melody begins with a rest, remove that initial rest; otherwise choose the empty initial factor. Every remaining event begins with a note. After each note, either the next event is a rest, in which case pair the two, or it is another note or the melody ends, in which case pair the note with the empty choice. Since adjacent rests are forbidden, no rest can belong to two blocks and no rest can be left unpaired. The decomposition is therefore both exhaustive and unique. ▫\square

This small lemma is the structural heart of the generating function.

5. The general generating function

The most useful formulation allows note durations and rest durations to have different admissible notation systems.

Let

A(q)=∑d≥1αdqd A(q)=\sum_{d\ge1}\alpha_d q^d

be the duration generating function for a single note before pitch is chosen, where αd\alpha_d is the number of allowed written note forms of duration dd.

Similarly let

B(q)=∑d≥1βdqd B(q)=\sum_{d\ge1}\beta_d q^d

be the duration generating function for a single rest.

The coefficients αd\alpha_d and βd\beta_d are useful when one wants to distinguish notation rather than only sounding duration. For example, if two different permitted spellings of duration 3 are to count separately, then the appropriate coefficient can be 22 rather than 11.

Since each note can have any of pp pitches,

N(q)=pA(q), N(q)=pA(q),

while

R(q)=B(q). R(q)=B(q).

Theorem 1. Melody generating function

Under the canonical rule forbidding adjacent rest events, the ordinary generating function for legal melodies is

Mp(q)=1+B(q)1−pA(q)(1+B(q)). \boxed{ M_p(q)=\frac{1+B(q)}{1-pA(q)(1+B(q))}. }

Here [qn]Mp(q)[q^n]M_p(q) is the number of legal melodies of total duration nn.

Proof. Translate the unique language decomposition of Lemma 1 into generating functions. Disjoint choice becomes addition, concatenation becomes multiplication, and the Kleene star becomes a geometric series:

Mp(q)=(1+R(q))∑k≥0(N(q)(1+R(q)))k. M_p(q) =(1+R(q))\sum_{k\ge0}\bigl(N(q)(1+R(q))\bigr)^k.

Substituting N(q)=pA(q)N(q)=pA(q) and R(q)=B(q)R(q)=B(q) gives

Mp(q)=(1+B(q))∑k≥0(pA(q)(1+B(q)))k. M_p(q) =(1+B(q))\sum_{k\ge0}\bigl(pA(q)(1+B(q))\bigr)^k.

Using ∑k≥0Xk=(1−X)−1\sum_{k\ge0}X^k=(1-X)^{-1} as an identity of formal power series,

Mp(q)=1+B(q)1−pA(q)(1+B(q)). M_p(q) =\frac{1+B(q)}{1-pA(q)(1+B(q))}.

The exponent of qq records total duration because multiplication adds exponents. Therefore the coefficient of qnq^n counts exactly the legal melodies of duration nn. ▫\square

The theorem is more general than the particular one-bar problem. Change the pitch inventory, the temporal unit, the allowed note values, the allowed rest values, or the number of orthographically distinct ways to write a duration, and only pp, AA, and BB change.

6. The unrestricted positive-duration model

The cleanest algebra occurs when every positive integral duration is allowed, with one representation per duration for both notes and rests. Then

A(q)=B(q)=q+q2+q3+⋯=q1−q. A(q)=B(q)=q+q^2+q^3+\cdots=\frac{q}{1-q}.

For a fixed target duration nn, this infinite series causes no difficulty: terms of degree greater than nn can never contribute to [qn][q^n]. Equivalently one may truncate at qnq^n.

Substituting into Theorem 1 gives

Mp(q)=1+q1−q1−pq1−q(1+q1−q). M_p(q) = \frac{1+\frac{q}{1-q}} {1-p\frac{q}{1-q}\left(1+\frac{q}{1-q}\right)}.

Since

1+q1−q=11−q, 1+\frac{q}{1-q}=\frac{1}{1-q},

we obtain the unexpectedly compact form

Mp(q)=1−q1−(p+2)q+q2. \boxed{ M_p(q)=\frac{1-q}{1-(p+2)q+q^2}. }

This is the central closed form of the model.

Corollary 1. Recurrence

Writing

Mp(q)=∑n≥0an,pqn, M_p(q)=\sum_{n\ge0}a_{n,p}q^n,

the coefficients satisfy

an,p=(p+2)an−1,p−an−2,p(n≥2), \boxed{ a_{n,p}=(p+2)a_{n-1,p}-a_{n-2,p}\qquad(n\ge2), }

with

a0,p=1,a1,p=p+1. a_{0,p}=1,\qquad a_{1,p}=p+1.

Proof. Multiply the series by the denominator:

(1−(p+2)q+q2)∑n≥0an,pqn=1−q. (1-(p+2)q+q^2)\sum_{n\ge0}a_{n,p}q^n=1-q.

Equating coefficients of qnq^n for n≥2n\ge2 gives the recurrence. The coefficients of q0q^0 and q1q^1 give the stated initial values. ▫\square

For p=24p=24 the recurrence is

an=26an−1−an−2, \boxed{a_n=26a_{n-1}-a_{n-2}},

with a0=1a_0=1 and a1=25a_1=25.

The first few values are

nn an,24a_{n,24}
0 1
1 25
2 649
3 16,849
4 437,425
5 11,356,201
6 294,823,801

For a 4/4 bar of sixteen sixteenth units,

a16,24=41,006,928,746,285,492,812,225. \boxed{ a_{16,24}=41,006,928,746,285,492,812,225. }

This is about 4.10×10224.10\times10^{22} possibilities, or about 75.175.1 bits of combinatorial choice. As a scale comparison rather than a mathematical ingredient, it is of the same order as the number of molecules in roughly a millilitre of water.

7. A direct combinatorial formula

The generating function is compact, but it is useful to see the same count without any formal power series.

Fix total duration nn and suppose a melody contains exactly mm events. There are

(n−1m−1) \binom{n-1}{m-1}

ways to choose the ordered positive durations of those events, because these are compositions of nn into exactly mm parts.

Now suppose exactly rr of the mm events are rests. Since rests may not be adjacent, the number of ways to choose their positions is

(m−r+1r). \binom{m-r+1}{r}.

To see this, first place the m−rm-r note events. They create m−r+1m-r+1 gaps: before the first note, between consecutive notes, and after the last note. At most one rest may occupy each gap. Choose rr of these gaps.

The remaining m−rm-r events are notes. Each has pp pitch choices, giving

pm−r p^{m-r}

pitch assignments.

Multiplying the independent choices and summing gives the following result.

Theorem 2. Explicit counting formula

For n≥1n\ge1,

an,p=∑m=1n(n−1m−1)∑r=0⌊(m+1)/2⌋(m−r+1r)pm−r. \boxed{ a_{n,p} = \sum_{m=1}^{n} \binom{n-1}{m-1} \sum_{r=0}^{\lfloor(m+1)/2\rfloor} \binom{m-r+1}{r}\,p^{m-r}. }

Together with a0,p=1a_{0,p}=1, this counts exactly the same objects as Theorem 1.

Proof. Every legal melody has a unique number mm of events and a unique number rr of rest events. The first binomial coefficient chooses its ordered positive durations, the second chooses a non-adjacent rest pattern among the mm event positions, and the power of pp chooses pitches for all remaining events. The decomposition by (m,r)(m,r) is disjoint and exhaustive. ▫\square

This proof is perhaps the most immediately combinatorial one: the object being counted never disappears behind a recurrence symbol.

8. A second combinatorial derivation of the recurrence

The recurrence can also be derived directly from the objects.

Let UnU_n be the number of legal duration-nn melodies whose final event is a note, and VnV_n the number whose final event is a rest. Then

an=Un+Vn. a_n=U_n+V_n.

To construct a melody counted by UnU_n, choose the duration of its final note. If the prefix has duration j∈{0,…,n−1}j\in\{0,\ldots,n-1\}, then the final note has the uniquely determined duration n−jn-j and one of pp pitches. Hence

Un=p∑j=0n−1aj. U_n=p\sum_{j=0}^{n-1}a_j.

Therefore

Un−Un−1=pan−1. U_n-U_{n-1}=p a_{n-1}.

For a melody ending in a rest, either the whole melody is the single rest of duration nn, or a legal melody ending in a note is followed by one rest. Thus

Vn=1+∑j=1n−1Uj, V_n=1+\sum_{j=1}^{n-1}U_j,

so

Vn−Vn−1=Un−1. V_n-V_{n-1}=U_{n-1}.

Adding the two differences gives

an−an−1=pan−1+Un−1. a_n-a_{n-1}=p a_{n-1}+U_{n-1}.

Applying the corresponding relation one step earlier and using

Un−1=Un−2+pan−2 U_{n-1}=U_{n-2}+p a_{n-2}

eliminates the auxiliary state UU and yields

an=(p+2)an−1−an−2. \boxed{a_n=(p+2)a_{n-1}-a_{n-2}}.

This is a useful proof because the two-state structure is visible: the only memory needed is whether the melody currently ends in a note or a rest.

9. Closed form and growth

Let

Δ=p(p+4) \Delta=\sqrt{p(p+4)}

and

λ±=p+2±Δ2. \lambda_{\pm}=\frac{p+2\pm\Delta}{2}.

These are the roots of

λ2−(p+2)λ+1=0. \lambda^2-(p+2)\lambda+1=0.

The recurrence therefore has the closed form

an,p=p+Δ2Δλ+n+Δ−p2Δλ−n. \boxed{ a_{n,p} = \frac{p+\Delta}{2\Delta}\lambda_+^n + \frac{\Delta-p}{2\Delta}\lambda_-^n. }

Since λ+λ−=1\lambda_+\lambda_-=1 and λ+>1\lambda_+>1 for p>0p>0, the count grows asymptotically like a constant multiple of λ+n\lambda_+^n.

A particularly pleasing special case is p=1p=1. Then

an=3an−1−an−2,a0=1,a1=2, a_n=3a_{n-1}-a_{n-2},\qquad a_0=1,\ a_1=2,

which gives

1,2,5,13,34,89,233,610,… 1,2,5,13,34,89,233,610,\ldots

These are the odd-indexed Fibonacci numbers:

an,1=F2n+1. \boxed{a_{n,1}=F_{2n+1}}.

This is one bridge between the melody model and recent combinatorics-of-rhythm work based on words.

10. One concrete bar

Consider the following one-bar example in 4/4. Durations are measured in sixteenth units.

A one-bar toy melody.

Its event representation is

(C4,4),(R,2),(D4,2),(E4,4),(F4,3),(G4,1). (C4,4),\ (R,2),\ (D4,2),\ (E4,4),\ (F4,3),\ (G4,1).

The durations sum to

4+2+2+4+3+1=16. 4+2+2+4+3+1=16.

At the purely duration level this is the composition

4+2+2+4+3+1. 4+2+2+4+3+1.

At the exact-melody level, however, the pitch labels and the position of the rest matter. The generating-function coefficient [q16]M24(q)[q^{16}]M_{24}(q) does not identify this particular melody; rather, it counts this melody together with every other legal melody of the same total duration.

That distinction motivates a richer algebraic representation.

11. From counts back to individual melodies

The ordinary generating function is intentionally forgetful. It remembers total duration and counts how many objects have that duration, but it does not retain the identity or order of the pitches of one particular melody.

To retain exact melodies, introduce a noncommuting alphabet

Σ={nx,d:x∈P,d≥1}∪{rd:d≥1}. \Sigma = \{n_{x,d}:x\in P,d\ge1\} \cup \{r_d:d\ge1\}.

Here nx,dn_{x,d} means a note of pitch xx and duration dd, while rdr_d means a rest of duration dd.

Because the symbols do not commute,

nC,4r2nD,2≠nD,2r2nC,4. n_{C,4}r_2n_{D,2} \neq n_{D,2}r_2n_{C,4}.

Order is therefore preserved.

Define the noncommutative event sums

𝐍=∑x∈P∑d≥1nx,d,𝐑=∑d≥1rd. \mathbf N=\sum_{x\in P}\sum_{d\ge1}n_{x,d}, \qquad \mathbf R=\sum_{d\ge1}r_d.

Then the entire legal melodic language is represented formally by

𝐌=(1+𝐑)(𝐍(1+𝐑))*. \boxed{ \mathbf M=(1+\mathbf R)\bigl(\mathbf N(1+\mathbf R)\bigr)^*. }

An individual melody appears as one word, hence one noncommutative monomial, in this formal series.

Now define a weight map ω\omega by

ω(nx,d)=qd,ω(rd)=qd. \omega(n_{x,d})=q^d, \qquad \omega(r_d)=q^d.

When ω\omega is extended multiplicatively and linearly, all pitch symbols of the same duration collapse onto the same power of qq. Summing over the pp possible pitches produces the factor pp. Thus the ordinary generating function is the commutative image of the exact melodic language:

ω(𝐌)=Mp(q). \omega(\mathbf M)=M_p(q).

Conceptually, this gives a useful hierarchy:

individual melodies→weighted words→counts by duration. \text{individual melodies} \longrightarrow \text{weighted words} \longrightarrow \text{counts by duration}.

The generating function is not the melody universe itself. It is a deliberately compressed shadow of that universe.

12. Bach’s C-minor fugue as an encoding example

A historically familiar example makes the distinction concrete. The subject of J. S. Bach’s Fugue in C minor, BWV 847, begins in the middle voice. The following schematic re-engraving shows its opening two complete measures.

Opening two full measures of the subject of J. S. Bach’s Fugue in C minor, BWV 847. The source work is public domain; the event sequence was checked against public-domain/CC score sources.

Suppressing octave register in the text notation for readability, the first complete bar has event word

r2nC,1nB,1nC,2nG,2nA♭,2nC,1nB,1nC,2nD,2. \boxed{ r_2\, n_{C,1}\, n_{B,1}\, n_{C,2}\, n_{G,2}\, n_{A\flat,2}\, n_{C,1}\, n_{B,1}\, n_{C,2}\, n_{D,2}. }

Its duration check is

2+1+1+2+2+2+1+1+2+2=16. 2+1+1+2+2+2+1+1+2+2=16.

As an exact noncommutative word, this bar is one object. Under the duration map ω\omega, the product becomes simply

q16. q^{16}.

That collapse is not a defect. It is precisely what coefficient extraction needs: every legal exact bar of duration sixteen maps to degree sixteen, and the coefficient records how many distinct exact bars arrived there.

The example also illustrates why the noncommutative lift can be useful computationally. One may retain exact words for motif searching, interval transforms, transposition classes, or pattern avoidance, and only later project onto a coarser generating function.

13. Dots, ties, and written notation

There are two different counting questions that should not be confused.

  1. Sounding-duration model. A duration of three sixteenths is simply the integer 33.
  2. Written-notation model. Distinct spellings of the same duration may count as different objects.

For example, a dotted eighth has duration three sixteenths. If the model also allows an eighth tied to a sixteenth and regards that spelling as distinct, then duration 33 has more than one notational realization.

This is exactly why Theorem 1 was stated with coefficients αd\alpha_d and βd\beta_d. If there are α3\alpha_3 legal note spellings of duration 33, then the note-duration series contains

α3q3. \alpha_3q^3.

The same framework therefore handles conventional note values, dotted notes, selected ties, or other notation systems by changing the duration series rather than rebuilding the combinatorics.

For example, if one permits only undotted powers of two in sixteenth units,

A(q)=q+q2+q4+q8+q16. A(q)=q+q^2+q^4+q^8+q^{16}.

If dotted eighths are added, one adds q3q^3; if dotted quarters are added, one adds q6q^6; and so on. If notes and rests use different conventions, take A≠BA\ne B.

This separation between structural combinatorics and notation policy is one of the useful features of the model.

14. Relation to earlier work

The basic combinatorial ingredients are classical. Integer compositions, colored compositions, formal languages, and rational generating functions are established subjects. The musical counting question also has prior treatments.

A particularly close antecedent is the 2018 essay How many melodies are there? on the blog Possibly Wrong. It considers notes and rests in a bar and derives the same structural language idea: an optional rest followed by a sequence of notes each optionally followed by a rest. Its note-duration generating function uses conventional powers-of-two values, while its rest generating function permits arbitrary integral lengths. In its notation,

fn(x)=1+h(x)1−gn(x)(1+h(x)). f_n(x)=\frac{1+h(x)}{1-g_n(x)(1+h(x))}.

Thus the structural generating-function identity of Theorem 1 should not be presented as a novelty claim.

More recently, Romero-Garcia, Tarsissi, Najman, and Agon (2026) formalized rhythms as words over an alphabet encoding onsets, sustains, and silences. Their regular-language description leads to rational generating functions and, for their rhythm model, the odd-indexed Fibonacci numbers. The specialization p=1p=1 of the present unrestricted-duration model yields the same Fibonacci subsequence, making the relationship especially suggestive.

There is also a broader combinatorial literature on colored and restricted compositions, where parts carry labels or colors and restrictions are imposed on their positions.

Accordingly, the present manuscript is best viewed in its current form as an expository synthesis and generalization, with several useful explicit consequences: the compact pp-pitch rational function, the recurrence, the direct double-sum formula, the notational multiplicity extension, and the noncommutative exact-melody lift. A stronger claim of journal-level novelty would require a more exhaustive literature search and a precise comparison theorem with existing composition and rhythm models.

15. Toward a bijective proof

The direct formula in Theorem 2 is already combinatorial, while the recurrence follows elegantly from either the generating function or the two-state ending classification.

A stronger aesthetic goal would be a direct bijection explaining

an+an−2=(p+2)an−1. a_n+a_{n-2}=(p+2)a_{n-1}.

That identity asks for an explicit correspondence between

ℳn⊔ℳn−2 \mathcal M_n\sqcup\mathcal M_{n-2}

and

{1,…,p+2}×ℳn−1, \{1,\ldots,p+2\}\times\mathcal M_{n-1},

where ℳk\mathcal M_k is the set of legal melodies of duration kk.

The generating function proves that such sets have the same cardinality, but cardinal equality is not yet an illuminating bijection. Constructing a natural musical bijection - one that explains the two extra states beyond the pp pitches without artificial casework - remains a worthwhile refinement of the argument.

This is a good example of a broader principle: an algebraic recurrence may be easy to discover, while the bijection that makes the recurrence feel inevitable can contain the deeper combinatorial insight.

16. A Lean 4 formalization plan

A formal proof assistant can separate two levels of the argument.

First, the algebraic recurrence can be encoded immediately. Second, one can formalize the combinatorial model itself and prove that its cardinalities satisfy that recurrence or equal the explicit binomial sum.

A compact Lean 4 / Mathlib core is as follows:

import Mathlib

namespace MelodyCount

/-- Algebraic sequence predicted by the generating function. -/
def a (p : Int) : Nat -> Int
  | 0     => 1
  | 1     => p + 1
  | n + 2 => (p + 2) * a p (n + 1) - a p n

@[simp] theorem a_zero (p : Int) : a p 0 = 1 := rfl

@[simp] theorem a_one (p : Int) : a p 1 = p + 1 := rfl

@[simp] theorem a_rec (p : Int) (n : Nat) :
    a p (n + 2) = (p + 2) * a p (n + 1) - a p n := by
  rfl

-- The concrete two-octave, one-bar value.
example : a 24 16 = 41006928746285492812225 := by
  native_decide

end MelodyCount

This verifies the recurrence as a definition and makes the numerical claim executable. It does not yet prove that the sequence counts the musical objects. That bridge is the important formalization task.

A natural next definition is the explicit combinatorial count

open scoped BigOperators
open Finset

/-- Direct formula from Theorem 2; blueprint. -/
def directCount (p n : Nat) : Nat :=
  if n = 0 then 1 else
    ∑ m in Icc 1 n,
      Nat.choose (n - 1) (m - 1) *
        ∑ r in (range (m + 1)).filter (fun r => 2 * r <= m + 1),
          Nat.choose (m - r + 1) r * p ^ (m - r)

The central theorem to formalize is then

/-- Main enumerative bridge to be proved in Mathlib. -/
theorem directCount_eq_recurrence (p n : Nat) :
    (directCount p n : Int) = a p n := by
  -- Suggested route:
  -- 1. prove the direct count has initial values 1 and p+1;
  -- 2. derive the same second-order recurrence using Pascal identities;
  -- 3. conclude by induction on n.
  sorry

An even more faithful formalization would define an inductive Event, define legal melodies as lists with positive durations and a no-adjacent-rest predicate, define total duration recursively, and prove that the finite subtype of duration-nn legal melodies has cardinality directCount p n. That route is longer but mathematically satisfying because the theorem would connect the recurrence all the way back to the semantic object.

A possible datatype skeleton is

inductive Event (Pitch : Type)
  | note : Pitch -> Nat -> Event Pitch
  | rest : Nat -> Event Pitch

open Event


def duration : Event Pitch -> Nat
  | note _ d => d
  | rest d   => d


def isRest : Event Pitch -> Bool
  | rest _   => true
  | note _ _ => false

One would then require positive durations, define totalDuration, and formalize the prohibition of adjacent rests. The eventual theorem would assert that for a finite pitch type of cardinality pp, the cardinality of legal melodies of total duration nn equals an,pa_{n,p}.

This division of labor is useful: the handwritten proof explains the mathematics; Lean checks that no case or algebraic identity has been smuggled past us.

17. Computational realization

The mathematics suggests a very small software tool.

An event can be represented as a pair

(pitch-or-rest, duration)

such as

(C4, 4), (R, 2), (D4, 2), (E4, 4), (F4, 3), (G4, 1).

A parser from MusicXML, MIDI plus quantization, or a small hand-entered notation can map a bar into this sequence. From the same structure one can compute three different representations:

One can then reverse the perspective and enumerate or sample legal words from the grammar. More interestingly, additional quotient maps can identify melodies up to transposition, inversion, rhythmic scaling, or other equivalence relations. The algebraic representation therefore becomes a bridge from elementary counting toward computational music analysis.

18. Scope and limitations

The model intentionally ignores many musical distinctions. Among them are:

These are not defects so much as directions in which the model can be refined. The virtue of Theorem 1 is modularity: many refinements can be implemented by replacing the event generating functions or by replacing the regular language.

The most important conceptual distinction is between possibility and musical plausibility. A coefficient can count every legal string under a formal grammar; it says nothing by itself about which strings sound coherent, memorable, beautiful, or stylistically meaningful.

19. Conclusion

The original problem sounds almost recreational: count the melodies in a bar. But it quickly reveals a clean mathematical anatomy.

Duration produces compositions. Pitch labels the note parts. Silence introduces a local exclusion rule. That exclusion rule is naturally a regular language. The language becomes a rational generating function. In the unrestricted positive-duration model the rational function collapses to

Mp(q)=1−q1−(p+2)q+q2, \boxed{ M_p(q)=\frac{1-q}{1-(p+2)q+q^2}, }

and the entire enumeration is governed by

an,p=(p+2)an−1,p−an−2,p. \boxed{ a_{n,p}=(p+2)a_{n-1,p}-a_{n-2,p}. }

For p=24p=24 and n=16n=16, this gives

41,006,928,746,285,492,812,225 \boxed{41,006,928,746,285,492,812,225}

one-bar melodies under the stated rules.

The number itself is entertaining. The structure that produces it is the more interesting result. The same object can be viewed as a composition, a constrained colored word, a regular language, a rational generating function, a recurrence, a binomial sum, or a noncommutative formal series containing each individual melody as a word.

That multiplicity of viewpoints is exactly the sort of thing that makes a small combinatorial problem worth keeping. One begins with a bar of music and ends with a piece of algebra that can be unfolded, generalized, mechanized, and - if one wishes - played.

References

  1. P. Flajolet and R. Sedgewick, Analytic Combinatorics, Cambridge University Press, 2009. See especially the symbolic method and rational languages.
  2. “Possibly Wrong,” How many melodies are there?, 24 April 2018. https://possiblywrong.wordpress.com/2018/04/24/how-many-melodies-are-there/
  3. G. Romero-Garcia, L. Tarsissi, L. Najman, and C. Agon, “Counting Rhythms Using Combinatorics on Words,” in Mathematics and Computation in Music - MCM 2026, LNCS/LNAI 16609, pp. 225-238, 2026. DOI: 10.1007/978-3-032-27827-2_13.
  4. R. Sachdeva and A. K. Agarwal, “Combinatorics of certain restricted n-color composition functions,” Discrete Mathematics 340(3), 361-372, 2017. DOI: 10.1016/j.disc.2016.09.009.
  5. J. S. Bach, The Well-Tempered Clavier, Book I, Fugue in C minor, BWV 847. Public-domain score sources include IMSLP; the subject transcription used for checking the example is also available through Wikimedia Commons.

Note on priority and submission

This manuscript records an independent derivation and develops it into a coherent theorem/proof framework. Because a closely related generating-function construction appeared publicly in 2018 and the underlying composition/regular-language machinery is classical, the current draft should not make a claim of first discovery. Before journal submission, the literature review should be expanded and the precise incremental contribution should be stated explicitly. The manuscript is already suitable as a mathematically serious expository article or blog essay; a research-journal version should sharpen the novelty around one or more of the generalization, noncommutative lift, equivalence-class enumeration, bijective proof, or formal verification directions.