GENUS ZERO ↔ NONCROSSING

The combinatorial heart of the Wigner semicircle law: a pairing of {0, ..., 2n-1} has genus zero if and only if it is noncrossing. Consequently, the number of genus-zero pairings equals the Catalan number Cₙ.

Key design choices:

• Pairing n as a subtype (no dependent proof parameters)
• Equiv.Perm.numCycles counting ALL cycles including fixed points
• finRotate for the long cycle (not cycleOf)
• Recursive noncrossing predicate, with a separate bridge to arc crossings
• Three-stage proof decomposition via cycle count bound

1. Total Cycle Count

Mathlib's cycleType.card counts only nontrivial cycles (length ≥ 2). The genus formula needs ALL cycles, including fixed points (1-cycles). We define numCycles as the sum of nontrivial cycles and fixed points.

Using cycleType.card alone gives wrong genera. For γπ = (1,3,5)(2)(4)(6), cycleType.card = 1 but numCycles = 4. The genus formula requires 4, not 1.

def Equiv.Perm.numCycles {α : Type u_1} [Fintype α] [DecidableEq α] (σ : Perm α) : ℕ

Total number of cycles of a permutation, including fixed points.

Equations

• σ.numCycles = σ.cycleType.card + Fintype.card ↑(Function.fixedPoints ⇑σ)

2. The Long Cycle

The canonical cyclic permutation on Fin (2n), sending i ↦ i + 1 mod 2n. Mathlib provides this as finRotate. Key properties we need:

• It is a single (2n)-cycle for n ≥ 1.
• isCycle_finRotate and cycleType_finRotate are available.

def longCycle (n : ℕ) : Equiv.Perm (Fin (2 * n))

The long cycle γ on Fin (2n).

Equations

• longCycle n = finRotate (2 * n)

theorem longCycle_isCycle {n : ℕ} (hn : 1 ≤ n) : (longCycle n).IsCycle

For n ≥ 1, the long cycle is a single cycle of length 2n.

3. Pairings as a Subtype

A pairing is a fixed-point-free involution. Making it a subtype avoids carrying proof terms through every definition and theorem.

def IsPairing {n : ℕ} (π : Equiv.Perm (Fin (2 * n))) : Prop

A permutation is a pairing if it is an involution with no fixed points.

Equations

• IsPairing π = (π ^ 2 = 1 ∧ ∀ (x : Fin (2 * n)), π x ≠ x)

def Pairing (n : ℕ) : Type

The type of pairings of Fin (2n).

Equations

• Pairing n = { π : Equiv.Perm (Fin (2 * n)) // IsPairing π }

@[implicit_reducible]

instance instCoeOutPairingPermFinHMulNatOfNat (n : ℕ) : CoeOut (Pairing n) (Equiv.Perm (Fin (2 * n)))

Equations

• instCoeOutPairingPermFinHMulNatOfNat n = { coe := Subtype.val }

4. Genus

Genus is defined as a plain function on pairings. For a pairing π, the composition γπ is a permutation of Fin(2n), and its total cycle count determines the genus via:

genus(π) = (n + 1 - numCycles(γ * π)) / 2

We prove separately that for pairings: (a) numCycles(γ * π) ≤ n + 1, so the numerator is nonneg (b) the numerator is always even, so division is exact

def Pairing.genus {n : ℕ} (p : Pairing n) : ℕ

The genus of a pairing.

Equations

• p.genus = (n + 1 - (longCycle n * ↑p).numCycles) / 2

Transposition bound infrastructure

The key structural fact: multiplying a permutation by a single transposition changes numCycles by at most 1. This is the fundamental property of the Cayley distance on the symmetric group.

We prove this via cycle_induction_on, analyzing how swap(a,b) interacts with the cycle decomposition of σ. The three cases are: (1) σ = 1 (trivial) (2) σ is a single cycle (swap splits or shortens) (3) σ = c * d with c, d disjoint (reduce to sub-cases)

theorem Pairing.numCycles_le {n : ℕ} (p : Pairing n) : (longCycle n * ↑p).numCycles ≤ n + 1

For any pairing, numCycles(γπ) ≤ n + 1.

Sign-based parity infrastructure

The parity of numCycles(γπ) matches the parity of n + 1. This follows from the sign equation sign(γπ) = sign(γ) * sign(π) = (-1)^(n+1), combined with sign(σ) = (-1)^(σ.support.card + σ.cycleType.card).

theorem Pairing.genus_exact {n : ℕ} (p : Pairing n) (hn : 1 ≤ n) : 2 * p.genus = n + 1 - (longCycle n * ↑p).numCycles

For any pairing with n ≥ 1, (n + 1 - numCycles(γπ)) is even. False for n = 0: numCycles on Fin 0 is 0, but 2 * 0 ≠ 1.

5. Noncrossing Predicate (Recursive)

A noncrossing pairing is defined recursively:

• The empty pairing (n = 0) is noncrossing.
• A pairing on 2n points is noncrossing if there exists an adjacent pair (i, i+1 mod 2n) in the pairing whose removal yields a noncrossing pairing on 2(n-1) points.

"Adjacent" means: π(i) = finRotate(i), i.e., π sends some element to its cyclic successor.

This definition is better for Lean than the "no crossing arcs" formulation because:

1. It is structurally recursive (induction is immediate).
2. It aligns with Catalan recursion.
3. It avoids the cyclic-order normalization headaches.

def Pairing.hasAdjacentAt {n : ℕ} (p : Pairing n) (i : Fin (2 * n)) : Prop

An adjacent pair in a pairing: a point i such that π(i) = i + 1 mod 2n.

Equations

• p.hasAdjacentAt i = (↑p i = (finRotate (2 * n)) i)

noncomputable def Pairing.deleteAdjacent {n : ℕ} (p : Pairing (n + 1)) (i : Fin (2 * (n + 1))) (h : p.hasAdjacentAt i) : Pairing n

Deletion of an adjacent pair: given a pairing with π(i) = i+1, remove the pair {i, i+1} and reindex to get a pairing on 2(n-1) points.

This requires careful construction. The idea:

1. Let j = finRotate(i) = i + 1 mod 2n.
2. Define the restriction of π to Fin(2n) \ {i, j}.
3. Identify Fin(2n) \ {i, j} with Fin(2(n-1)) via an order-preserving map.
4. Show the resulting permutation is again a pairing.

This is the most technically demanding definition in the file. It requires building the injection Fin(2n-2) ↪ Fin(2n) that skips i and j, and proving the conjugated permutation is a fixed-point-free involution.

Equations

• p.deleteAdjacent i h = ⟨SemicircleCore.contractZeroOne (finRotate (2 * (n + 1)) ^ (2 * (n + 1) - ↑i) * ↑p * (finRotate (2 * (n + 1)) ^ (2 * (n + 1) - ↑i))⁻¹) ⋯ ⋯, ⋯⟩

def Pairing.IsNoncrossing {n : ℕ} : Pairing n → Prop

Recursive noncrossing predicate.

Equations

• x_2.IsNoncrossing = True
• p.IsNoncrossing = ∃ (i : Fin (2 * (n + 1))) (h : p.hasAdjacentAt i), (p.deleteAdjacent i h).IsNoncrossing

6. The Bridge Theorem (Three Stages)

We prove the equivalence in stages:

Stage A: numCycles(γπ) ≤ n + 1 for all pairings (upper bound) Stage B: numCycles(γπ) = n + 1 → noncrossing (equality → noncrossing) Stage C: noncrossing → numCycles(γπ) = n + 1 (noncrossing → equality)

Then genus = 0 ↔ numCycles = n + 1 ↔ noncrossing.

theorem numCycles_delete_adjacent {n : ℕ} (hn : 1 ≤ n) (p : Pairing (n + 1)) (i : Fin (2 * (n + 1))) (h : p.hasAdjacentAt i) : (longCycle (n + 1) * ↑p).numCycles = (longCycle n * ↑(p.deleteAdjacent i h)).numCycles + 1

The cycle-splitting lemma: removing an adjacent pair from a pairing decreases numCycles(γπ) by 1. Equivalently, the pairing with the adjacent pair has one more cycle than the contracted one. Requires n ≥ 1 so the target Pairing n is on ≥ 2 elements.

Helpers for Stage B: fixed points imply adjacent pairs

theorem Pairing.maxCycles_imp_noncrossing {n : ℕ} (p : Pairing n) (h : (longCycle n * ↑p).numCycles = n + 1) : p.IsNoncrossing

Stage B: If the cycle count achieves its maximum, the pairing is noncrossing.

Proof: by induction on n. The key insight is that numCycles = n+1 forces the composition gamma*pi to have fixed points (at least 2). Each fixed point yields an adjacent pair via the involution property. After deleting that adjacent pair, the cycle-splitting lemma gives numCycles = n for the contracted pairing, and induction applies.

theorem Pairing.noncrossing_imp_maxCycles {n : ℕ} (p : Pairing n) (hn : 1 ≤ n) (h : p.IsNoncrossing) : (longCycle n * ↑p).numCycles = n + 1

Stage C: Noncrossing pairings achieve maximum cycle count.

Proof: induction on n using the recursive noncrossing definition. Base case (n = 1): direct computation — the unique pairing on Fin 2 composed with the long cycle gives the identity, which has 2 cycles. Inductive step: if p is noncrossing, it has an adjacent pair at some i. Deleting this pair gives a noncrossing pairing p' on 2n points with numCycles(γ' * p') = n + 1 by induction. The cycle-splitting lemma gives numCycles(γπ) = numCycles(γ'π') + 1.

Requires n ≥ 1: on Fin 0, numCycles = 0 ≠ 1 = 0 + 1.

7. Main Theorem and Corollary

theorem Pairing.genus_zero_iff_noncrossing {n : ℕ} (p : Pairing n) : p.genus = 0 ↔ p.IsNoncrossing

The Bridge Theorem: genus zero ↔ noncrossing.

@[implicit_reducible]

instance instDecidablePredPermFinHMulNatOfNatIsPairing {n : ℕ} : DecidablePred IsPairing

Equations

• instDecidablePredPermFinHMulNatOfNatIsPairing x✝ = instDecidablePredPermFinHMulNatOfNatIsPairing._aux_1 x✝

@[implicit_reducible]

instance instFintypePairing {n : ℕ} : Fintype (Pairing n)

Equations

• instFintypePairing = Subtype.fintype IsPairing

8. Proof Dependencies and Estimated Effort

Lemmas that need building (not in Mathlib):

1. numCycles_eq_num_orbits — total cycles = orbits of ⟨σ⟩-action
2. Pairing.deleteAdjacent — the deletion/reindexing construction
3. numCycles_insert_adjacent — the cycle-splitting lemma
4. Pairing.numCycles_le — upper bound on cycles for pairings
5. Pairing.maxCycles_imp_noncrossing — contrapositive via crossing→merger
6. Pairing.noncrossing_imp_maxCycles — induction via deletion

What Mathlib provides:

• finRotate and isCycle_finRotate for the long cycle
• Equiv.Perm.cycleType for nontrivial cycle structure
• Function.fixedPoints and Fintype.card for fixed point count
• catalan and catalan_succ for Catalan numbers
• Basic Fin arithmetic and Perm algebra

Estimated scope: 800–1500 lines of Lean 4.

The hardest part:

The deletion/reindexing machinery (Lemma 2 above). Removing two points from Fin(2n) and reindexing to Fin(2(n-1)) while preserving the pairing structure requires building an explicit embedding Fin(2n-2) ↪ Fin(2n) and conjugating the permutation through it. This is conceptually simple but technically fiddly in dependent type theory. It is exactly the kind of thing an autoformalization agent (Gauss, Aristotle) handles well with human scaffolding.

The most satisfying part:

Once the bridge theorem compiles, the connection to the semicircle law becomes a clean chain: E[Tr(W^{2n})/N] → trace expansion → pairing sum → genus filter → genus 0 = noncrossing = Catalan → semicircle moments Each arrow is a separate formalizable step, and this file handles the crucial middle link.