What you will learn in this tutorial. We meet a curious sequence of integers from the Online Encyclopedia of Integer Sequences and notice that its values come in pairs: 1, 1, 1, 2, 2, 5, 5, 13, 13, 37, 37, … The bulk of the tutorial is devoted to explaining why. Along the way we'll meet multiset partitions and their duals, learn how a number-theoretic statistic called "density" secretly encodes a tree structure, prove a small but load-bearing graph-theoretic lemma, build a bijection that establishes the pairing, derive a generating function, and discover that our "helper sequence" had been quietly sitting in the OEIS for twenty-six years under a completely different name. At the very end we'll peek at how the load-bearing lemma can be checked by a computer.

The story is more interesting than the statement, so I recommend reading sequentially rather than jumping to the punchline. Each section builds on the previous one. You'll find Definition, Example, Theorem, and Exercise boxes throughout — exercises appear at the end of the section whose material they exercise, so you can practice each idea while it's fresh. Stars (★) indicate harder problems. If you get stuck on a definition, the answer is almost always to write down a small example.

§1. Multiset partitions: definitions and examples

We begin with the central object of study, building it up piece by piece. If you haven't seen multisets before, the first definition is the only conceptual leap; everything afterward is bookkeeping.

The next object is built out of multisets, and it has a slightly recursive flavor: we'll be looking at multisets whose elements are themselves multisets. Don't let this throw you. The standard mental picture is "a partition of a multiset into smaller pieces."

Take a moment to compute a few duals on your own before reading further. There's a subtle exercise of indexing that's easy to get wrong on the first try. (Try the multiset partition { {1,1,2}, {3} }. Answer: vertex 1 → {0,0}, vertex 2 → {0}, vertex 3 → {1}, so dual is { {0,0}, {0}, {1} }.)

Self-duality is a structural symmetry condition. Saying that a multiset partition is self-dual is saying something about the "shape" of how parts and vertices interlock — a shape that is invariant under swapping the roles of parts and vertices. We'll see in §2 that this has a beautiful geometric interpretation.

Density is a strange-looking statistic. We'll discover in §2 that it has a very natural meaning: it measures the "tree-ness" of an associated graph. Specifically, density 0 will correspond to the graph being a forest, and density −1 will correspond to a single tree.

We can finally state what our central sequence counts.

The first eleven values of this sequence (the entire b-file at the time of writing) are:

Stare at this table. Starting from n = 3, the values come in pairs: 2, 2; 5, 5; 13, 13; 37, 37. This phenomenon is the central observation of these notes. The sequence "stutters." As far as I can determine, no one has previously remarked on this — which means it is either a small mathematical discovery or a coincidence I am about to be embarrassed by.

Figure 1 shows the example multiset partition we've been working with, drawn as a bipartite incidence graph (which we will define carefully in §2). For now, just absorb the picture: parts on the left, vertices on the right, edges connecting them.

§2. The bipartite tree picture

The combinatorial definitions of §1 are accurate but unilluminating. To develop intuition, we recast every multiset partition as a graph. The recasting is so faithful that it loses no information.

This is a faithful recoding: from the bipartite incidence graph plus its edge weights, you can recover the original multiset partition exactly. Each part-node tells you which part you're talking about; the edges incident to it tell you which vertices appear in that part; the edge weights tell you with what multiplicity.

Now we make a beautiful observation about the relationship between the density statistic and the combinatorial structure of this graph. Recall that density(M) is defined as

where k = |parts| and m = |vertices|. But the sum ∑_p |distinct(p)| is exactly the number of edges in the bipartite incidence graph! Each distinct element of part p contributes exactly one edge (between p's left node and that vertex's right node). So:

Equivalently, if we let E denote the number of edges and V = k + m the total number of nodes, then

This puts us in well-trodden graph-theoretic territory. The quantity E − V is the negative of the well-known statistic V − E, which for a connected graph counts the number of independent cycles. (Sometimes called the cyclomatic complexity, or the rank of the cycle space.) In particular:

• A tree on V nodes has exactly V − 1 edges, so E − V = −1.
• More generally, a forest of c trees has V − c edges, so E − V = −c.
• A connected graph with one cycle has V edges, so E − V = 0.

The condition density = −1, plus the assumption that the partition is connected (i.e., the incidence graph is connected as a graph), is therefore equivalent to saying:

Theorem 2.3 transforms the problem from "exotic combinatorics about indexed multisets" into "graph theory with a small piece of decoration." Self-dual multiset partitions of density −1 are edge-weighted bipartite trees with a self-duality condition that we'll now figure out how to encode.

First, what does self-duality mean for the tree? Taking the dual of a multiset partition swaps the roles of parts and vertices. In graph terms, this means swapping the left side and the right side of the bipartition. So the dual of M corresponds to the same tree, but with the left and right node sets exchanged. For the original and the dual to be isomorphic as multiset partitions, the underlying tree must admit a graph isomorphism that swaps the two sides of the bipartition while preserving the edge weights. This kind of structural symmetry will become the focus of §4.

For now, observe one immediate consequence: self-duality forces the two sides to have the same size. If the left side has k nodes and the right side has m nodes, and we want a bijection swapping them, we must have k = m. The tree therefore has 2k nodes and 2k − 1 edges. The number of edges is odd. This parity will do enormous work later.

§3. A stuttering mystery

Let's pause and look at our sequence again, now that we have a geometric picture for the objects it counts.

The pairs starting from n = 3 are unmistakable. We naturally pose the question:

The fact that it's specifically odd-and-next-even pairs (and not some other pattern, like every-three-equal or "sum of two consecutive equals next") strongly suggests a parity-based bijection. The simplest such bijection would be a map that takes an object of weight 2t − 1 and produces an object of weight 2t by adding a single unit of weight somewhere. The question is: where?

We need to find a canonical, distinguished feature of every self-dual decorated bipartite tree — some structural element so unique that we can unambiguously say "increase its multiplicity by one." If we can find such a feature, the bijection writes itself.

The next two sections build that bijection. §4 establishes the load-bearing graph-theoretic lemma; §5 uses the lemma to construct the map and verify it really is a bijection.

§4. Graph automorphisms and the lemma

To formalize "self-duality" of an edge-weighted bipartite tree, we need to talk about graph automorphisms. If you've seen these in a graph theory or algebra course, this section will be a refresher; if not, the definitions are short.

Now we add the bipartite structure into the picture. A bipartite graph has its vertices partitioned into two sets — the color classes — such that every edge goes between the two classes (no edge connects two vertices of the same class). For trees, the bipartition is always uniquely determined: 2-color the vertices alternately, starting from any vertex.

The self-duality condition for our edge-weighted bipartite tree is exactly the existence of a color-swapping automorphism that preserves edge weights. (Verifying this is a small unwinding of definitions; do it as an exercise if you want to be sure.)

Before stating the lemma we need, let's make two small observations about color-swapping automorphisms.

A fixed edge is an edge whose two endpoints are swapped by σ. Every non-fixed edge belongs to a 2-orbit: a pair of edges that σ swaps with each other.

Why? Because σ² preserves colors (it's two color-swaps in a row), so for any edge e, the edge σ²(e) is in the same color-orbit as e. We need a slightly more careful argument to show that σ²(e) always equals e; this turns out to be true for trees, though it's not entirely obvious. (It's a consequence of the lemma we're about to state.) For now, take it as part of the structural picture: orbits have size 1 or 2 only.

With f denoting the number of fixed edges and c the number of 2-orbits, we have a count:

The right-hand side is odd, so f must be odd, and in particular f ≥ 1. There is always at least one fixed edge. The astonishing fact — and the load-bearing technical result of this tutorial — is that there is always exactly one.

The "at least one" half is the parity argument we just gave. The lemma's content is the upper bound: f cannot be 3, 5, 7, etc. To prove uniqueness we need a different technique.

§5. Building the bijection

With the lemma in hand, the bijection writes itself. Let T be a self-dual edge-weighted bipartite tree, and let e₀ be the unique σ-fixed edge guaranteed by Lemma 4.5. Let m₀ ≥ 1 denote its edge weight. The remaining 2k − 2 edges are partitioned by σ into k − 1 pairs. Within each pair, the two edges must carry the same weight (since σ preserves edge weights). Call these shared weights m₁, m₂, …, m_{k-1}.

The total weight of T is then:

This decomposition has an immediate parity consequence. Each mᵢ for i ≥ 1 is doubled, contributing an even amount to the total. So the parity of weight(T) is the same as the parity of m₀.

• If weight(T) is odd, then m₀ is odd; in particular, m₀ ≥ 1.
• If weight(T) is even, then m₀ is even; in particular, m₀ ≥ 2.

This is where the bijection comes from. The map that increments m₀ by 1 sends odd-weight trees to even-weight trees, and the map that decrements m₀ by 1 goes the other way. The constraint m₀ ≥ 2 on even-weight trees is exactly what makes the decrement well-defined.

Notice how essential the uniqueness in Lemma 4.5 is. If σ had multiple fixed edges, the inverse map would need to specify which one to decrement, and that choice could fail to commute with relabeling, breaking well-definedness. With exactly one, the choice makes itself.

§6. Generating functions and an old friend

The Pairing Theorem cuts our work in half: we now only need to compute the odd-indexed terms of A322111 and the even-indexed terms come along for free. But it would be more satisfying to have a closed-form expression. To produce one, we'll use generating functions.

We start by observing that the data of a self-dual edge-weighted bipartite tree of weight n consists of two pieces:

1. The weight m₀ of the unique fixed edge (which has the same parity as n);
2. The structure on one side of the fixed edge — call it the "L-side." This is a rooted edge-weighted tree, hanging off the L-endpoint of the fixed edge. The "other side" is forced by σ: it's the mirror image of the L-side, so we don't need to count it separately.

If we let e denote the total edge weight on one side (the L-side), then the weight equation reads m₀ + 2e = n.

Define

where r_j is the number of (isomorphism classes of) rooted edge-weighted trees with total edge weight j. The sum starts at j = 0, with r₀ = 1 corresponding to the empty tree (just a root, no edges).

By a standard generating-function manipulation from the theory of combinatorial species, the generating function R(x) satisfies a recursive functional equation. A rooted tree consists of a root together with a multiset of "branches," where each branch is an edge with positive integer weight attached to a child rooted tree. The generating function for a single branch is

because x/(1-x) = x + x² + x³ + ⋯ encodes "a positive integer, weighted by itself" (i.e., the choices of edge weight, each contributing its value to the generating-function exponent), and R(x) attaches a child rooted tree below the edge. The multiset construction (Pólya / exponential formula) then gives:

This recursion lets us compute the coefficients r_j one at a time, using only previously-computed values. Concretely:

Now comes a moment of mild humility. A search of the OEIS for the sequence 1, 1, 3, 8, 24, 71, 224, 710, 2318, 7659, 25703 returns exactly one result, and it is A052855: "Number of forests of rooted trees of nonempty sets with n points," contributed in January 2000 by the INRIA Encyclopedia of Combinatorial Structures. A French computer-algebra system computed our helper sequence twenty-six years before we needed it, and it has been sitting in the OEIS ever since, waiting for someone to notice that it was secretly the structural backbone of a self-dual multiset partition enumeration.

With R(x) = A052855 identified, the closed form for A322111 falls out. For odd weight n = 2t − 1, the admissible values of m₀ are {1, 3, 5, …, 2t − 1}, and the corresponding values of e = (n − m₀)/2 range over {0, 1, 2, …, t − 1}. Each value of e contributes r_e = A052855(e) trees. So:

§7. The numbers

The closed form makes computation essentially free. Here are the values of A322111 from n = 0 through n = 40, with the previously known terms (a(0) through a(10)) in plain rows and the thirty newly computed terms shaded.

Five of the new terms (a(11) through a(15)) were independently cross-validated by a brute-force enumerator using the NetworkX graph isomorphism algorithm, which builds the bipartite multigraph directly and checks self-duality via side-swapping graph isomorphism — sharing no logic with the generating function approach. The values agreed to the digit. This is the kind of cross-check that lets one sleep at night.

§8. A computer-checked proof of the lemma

This last section is a brief tour of how the Unique Fixed Edge Lemma (Lemma 4.5) was checked by a computer. If you've never seen formal verification before, this will be your first taste; it's optional reading.

The proof assistant we'll look at is Lean 4, paired with a community mathematics library called Mathlib. Mathlib contains tens of thousands of formalized definitions and theorems, including a substantial graph theory library. The full proof of the Unique Fixed Edge Lemma is 380 lines of Lean code and contains zero unfinished steps. Let's translate the key pieces.

Setting up the definitions

The first thing we need is the formal definition of "color-swapping automorphism." In Lean:

/-- σ is color-swapping w.r.t. a Bool-coloring c if it flips every vertex's color. -/
def IsColorSwapping (c : G.Coloring Bool) (σ : G ≃g G) : Prop :=
  ∀ v : V, c (σ v) = !c v

A few things to note:

• G ≃g G reads as "graph isomorphism from G to itself" — i.e., a graph automorphism. Lean uses the notation ≃g for graph isomorphisms; the g distinguishes them from set bijections (≃) or group isomorphisms (≃*).
• G.Coloring Bool is a function that 2-colors the vertices of G using Bool (true / false) as the two colors. For a tree, this coloring is uniquely determined up to swapping the colors.
• The condition is that for every vertex v, the color of σ v equals the boolean negation of the color of v. The exclamation mark ! is Lean's notation for boolean negation.

And the definition of a fixed edge:

/-- An edge is fixed by σ if σ maps it to itself (swapping its endpoints). -/
def IsFixedEdge (σ : G ≃g G) (e : Sym2 V) : Prop :=
  Sym2.map σ e = e

Edges of a graph on vertex type V are unordered pairs, which Lean represents as elements of the type Sym2 V. The function Sym2.map σ applies σ to both endpoints of an edge. The condition for a fixed edge is that the result equals the original.

A small warm-up lemma: σ has no fixed vertices

This is Observation 4.3 from §4. In Lean:

theorem IsColorSwapping.no_fixed_vertex (hσ : IsColorSwapping c σ) (v : V) :
    σ v ≠ v := by
  intro h
  have := hσ v       -- pulls out the fact c (σ v) = !c v
  rw [h] at this   -- substitutes σ v ↦ v, giving c v = !c v
  simp at this     -- simp recognizes the contradiction

Let's translate this line by line:

• intro h says "assume the negation we want to refute" — i.e., suppose σ v = v.
• have := hσ v instantiates the hypothesis hσ at v, giving us the fact c (σ v) = !c v.
• rw [h] at this rewrites using the assumption h (σ v = v) inside the hypothesis this, transforming it to c v = !c v.
• simp at this recognizes that c v = !c v is absurd (since boolean negation has no fixed point), and closes the goal automatically.

The Lean proof has the same three logical steps as the prose: introduce the assumption, derive the color equation, observe the contradiction. The notation is unfamiliar but the structure mirrors what you'd write on paper.

The main lemma: existence of a fixed edge

The mathematical content here is the parity argument from §4: the tree has 2k − 1 edges (an odd number), the action of σ on edges decomposes into orbits, and odd-cardinality permutation actions must fix at least one element. The Lean proof uses a Mathlib lemma called Equiv.Perm.exists_fixed_point_of_prime that captures exactly this kind of parity argument for prime-power-order group actions.

theorem IsTree.exists_fixed_edge (hT : G.IsTree)
    (hσ : IsColorSwapping c σ) :
    ∃ e ∈ G.edgeSet, IsFixedEdge σ e := by
  classical
  let σ_edge : Equiv.Perm G.edgeSet := σ.mapEdgeSet
  -- Decompose orderOf σ = 2^a * m with m odd
  obtain ⟨a, m, hm_odd, hk_eq⟩ := Nat.exists_eq_two_pow_mul_odd hk_ne
  -- |G.edgeSet| is odd (Task 1), so 2 ∤ |G.edgeSet|
  have h_not_dvd : ¬ 2 ∣ Fintype.card G.edgeSet := …
  -- Apply Equiv.Perm.exists_fixed_point_of_prime to σ_edge^m
  obtain ⟨⟨e, he⟩, hfe⟩ := Equiv.Perm.exists_fixed_point_of_prime h_not_dvd hpow
  -- Now we have an edge fixed by σ^m. We need it fixed by σ itself —
  -- a "bridge argument" closes this gap.
  …

The piece that surprised me — and that the formalization process exposed — is that the natural simplifying assumption σ² = identity turns out to be false in general! Color-swapping automorphisms can have order 4 or 8 or 16 — not just 2. The counterexample is the symmetric "double caterpillar" tree: a central edge with two isomorphic branches on each side, where σ swaps the central edge's endpoints AND simultaneously swaps the two branches on each side, giving order 4.

This forces a more sophisticated argument: decompose the order of σ as 2^a · m with m odd, work with σ^m (whose order is a power of 2), and use a counting lemma about prime-power permutation actions to find an edge fixed by σ^m. The remaining gap — from "σ^m-fixed" to "σ-fixed" — is closed by the same kind of bridge argument we used in §4.

The uniqueness half

The uniqueness half of the lemma is our §4 proof, formalized. The Lean version follows the same three-step structure: pick two distinct fixed edges, delete the first one, observe that σ swaps the two resulting components, and derive a contradiction from the existence of the second fixed edge.

theorem IsTree.fixed_edge_unique (hT : G.IsTree)
    (hσ : IsColorSwapping c σ)
    {e₁ e₂ : Sym2 V} (he₁ : e₁ ∈ G.edgeSet) (he₂ : e₂ ∈ G.edgeSet)
    (hf₁ : IsFixedEdge σ e₁) (hf₂ : IsFixedEdge σ e₂) :
    e₁ = e₂ := by
  obtain ⟨a, a', rfl⟩ := Sym2.ind (fun u v => ⟨u, v, rfl⟩) e₁
  obtain ⟨b, b', rfl⟩ := Sym2.ind (fun u v => ⟨u, v, rfl⟩) e₂
  …
  -- Bridge argument: delete e₁, show that σ swaps the two resulting
  -- components, derive that b, b' must lie in the same component
  -- (because they're connected by edge e₂) and in different components
  -- (because σ swaps them), giving the contradiction.
  …

The full uniqueness proof in Lean is about 110 lines, most of it the technical machinery of stating "delete an edge and reason about the resulting components" formally. The mathematical content fits in the five sentences of §4's proof. There's a real gap between informal proof complexity and formal proof complexity, and one of the things you learn from formalization is which lemmas are easy on paper but hard in Lean (anything involving paths, cycles, or "obvious" connectivity statements) and which lemmas are hard on paper but easy in Lean (anything that reduces to algebra or simp).

The main theorem

With both halves in place, the main theorem is two lines:

theorem IsTree.unique_fixed_edge (hT : G.IsTree)
    (hσ : IsColorSwapping c σ) :
    ∃! e, e ∈ G.edgeSet ∧ IsFixedEdge σ e := by
  obtain ⟨e, he, hfe⟩ := hT.exists_fixed_edge hσ
  exact ⟨e, ⟨he, hfe⟩, fun e' ⟨he', hfe'⟩ => hT.fixed_edge_unique hσ he' he hfe' hfe⟩

The notation ∃! means "there exists a unique" — exactly the existence-and-uniqueness statement we want. The proof says: get a fixed edge from the existence theorem; close the uniqueness obligation by appealing to the uniqueness theorem.

What this gives us

Running #print axioms IsTree.unique_fixed_edge in Lean reports that the theorem depends on three axioms: propext (propositional extensionality), Classical.choice (the axiom of choice), and Quot.sound (the quotient construction). These are the standard axioms underlying classical mathematics in Lean — nothing exotic, no additional assumptions, no unfinished steps. The Lean kernel has checked that the proof is correct, in the most pedantic sense possible.

What does this buy us? The main thing is citability: the proof exists as a digital artifact that anyone can verify in seconds by running the Lean compiler. For a small lemma like this, formal verification is overkill; for a large or contentious result, it's invaluable. As an undergraduate, you don't need to learn Lean to do mathematics, but it's worth knowing that the option exists. Several major recent results — the four-color theorem, the Kepler conjecture, Liquid Tensor Experiment — have been formally verified, and the technology is becoming more accessible every year.

§9. Further reading

This tutorial scratches the surface of several large subjects. If you'd like to go deeper, here are some starting points.

• The OEIS itself at oeis.org. Browse around. Several hundred sequences in the "Wiseman density" neighborhood — see the cross-references on A322111 — admit similar tree-decomposition arguments. Many of them are wide open.
• Generating functions and species. The standard reference is Flajolet & Sedgewick, Analytic Combinatorics (Cambridge, 2009), available free online. For a more elementary treatment, see Wilf's generatingfunctionology, also free online. Tutorial 10 of this series gives a friendly intro to Pólya enumeration.
• Membrane computing. The bipartite tree structure with multiset weights has a beautiful interpretation as a "P system" (named after Gheorghe Păun) — a model of computation inspired by the biological cell. Păun's tutorial in the Proceedings of the Brainstorming Workshop on Uncertainty in Membrane Computing (Palma de Mallorca, 2004) is the canonical reference. Self-dual P systems (those invariant under swapping membranes and objects) are an essentially unstudied subclass; the present tutorial is, as far as I know, the first to count them.
• Lean 4 and formal verification. Start with the textbook Mathematics in Lean (free online), which walks you from "what is a proof" through real analysis in Lean. The community is friendly and active on the Lean Zulip chat. If you prefer videos, Kevin Buzzard's "Xena Project" lectures are a great entry point for math undergraduates.
• Graph automorphisms and Burnside. A first course in algebra or combinatorics is likely to cover the orbit-counting theorem (Burnside / Cauchy-Frobenius). The structural arguments in §4 are in the same spirit. For a deeper dive, see Cameron's Permutation Groups (LMS Student Texts, 1999).

End of Tutorial #14. Next in the series: Tutorial #15, "Lattice paths and the cycle lemma."