THE CATALAN SCALPEL

Infrastructure for the Catalan recurrence C_{n+1} = Σ C_k · C_{n-k}.

The key insight: vertex 0 pairs with some odd vertex 2k+1, partitioning the remaining 2n vertices into two independent noncrossing domains:

• Inside: {1, ..., 2k} of size 2k (supporting C_k noncrossing pairings)
• Outside: {2k+2, ..., 2n+1} of size 2(n-k) (supporting C_{n-k})

Our shiftTwoEquiv / contractZeroOne is the boundary case k = 0.

Architecture:

1. insideEquiv: Fin(2k) ≃ {i : Fin(2(n+1)) | 0 < i < 2k+1}
2. outsideEquiv: Fin(2(n-k)) ≃ {i : Fin(2(n+1)) | 2k+1 < i}
3. Parity theorem: p(0) is always odd for noncrossing p
4. catalanEquiv: NoncrossingPairing(n+1) ≃ Σ k, NCP(k) × NCP(n-k)

1. The Translation Dictionaries

2. Arc-Crossing ↔ Recursive Noncrossing Bridge

Two definitions of "noncrossing":

• Recursive (our IsNoncrossing): peelable via adjacent pairs
• Arc-based (¬HasCrossing): no two chords interleave

The bridge connects them, using several helper lemmas:

• finRotate_val: value-level characterization of finRotate
• general_shadow: shadow closure for arbitrary arcs
• no_crossing_has_adjacent: every crossing-free pairing has an adjacent pair
• HasCrossing_conj_forward: rotation preserves crossings (5-case analysis)
• contraction_crossing_lifts: contraction preserves crossings

def Pairing.HasCrossing {n : ℕ} (p : Pairing n) : Prop

A pairing has a crossing if two arcs interleave on the interval: ∃ a < b < p(a) < p(b).

Equations

• p.HasCrossing = ∃ (a : Fin (2 * n)) (b : Fin (2 * n)), ↑a < ↑b ∧ ↑b < ↑(↑p a) ∧ ↑(↑p a) < ↑(↑p b)

Helper lemmas for the bridge

Forward crossing projection lemmas

The Bridge Theorems

theorem IsNoncrossing_imp_no_crossing {n : ℕ} (p : Pairing n) (h : p.IsNoncrossing) : ¬p.HasCrossing

Bridge direction 1: recursive noncrossing implies no arc crossings. Proof: induction on n. An adjacent pair cannot participate in any crossing. Any crossing among other vertices lifts to a crossing in the contracted pairing, contradicting the induction hypothesis.

theorem no_crossing_imp_IsNoncrossing {n : ℕ} (p : Pairing n) (h : ¬p.HasCrossing) : p.IsNoncrossing

Bridge direction 2: no arc crossings implies recursive noncrossing. Proof: find an adjacent pair (by no_crossing_has_adjacent), delete it, and show the contracted pairing is also crossing-free (contrapositively: a crossing in the contracted pairing lifts to one in the original).

4. The Parity Theorem

The shadow-closure lemma is proved from ¬ HasCrossing using only order logic and injectivity. The parity theorem combines this closure with the even-cardinality lemma for fixed-point-free involutions.

theorem shadow_closed_of_no_crossing {n : ℕ} (p : Pairing n) (h_nc : ¬p.HasCrossing) (x : Fin (2 * n)) (hx_pos : 0 < ↑x) (hx_shadow : ↑x < ↑(↑p ⟨0, ⋯⟩)) : 0 < ↑(↑p x) ∧ ↑(↑p x) < ↑(↑p ⟨0, ⋯⟩)

Shadow closure: if p has no crossings, the shadow of the chord (0, p(0)) is closed under p. Proof: p(x) > 0 by involution, p(x) < p(0) by contradiction (otherwise 0 < x < p(0) < p(x) is a crossing).

theorem noncrossing_mapsTo_shadow {n : ℕ} {p : Pairing n} (h_nc : p.IsNoncrossing) (x : Fin (2 * n)) (hx_low : 0 < ↑x) (hx_high : ↑x < ↑(↑p ⟨0, ⋯⟩)) : 0 < ↑(↑p x) ∧ ↑(↑p x) < ↑(↑p ⟨0, ⋯⟩)

Shadow closure from the recursive noncrossing definition, via the bridge.

theorem noncrossing_zero_target_odd {n : ℕ} (p : Pairing (n + 1)) (h_nc : p.IsNoncrossing) : Odd ↑(↑p ⟨0, ⋯⟩)

Vertex 0 always pairs with an odd vertex in a noncrossing pairing.

Proof by contradiction: if p(0) is even = 2k, define the shadow S = {i : Fin(2(n+1)) | 0 < i < 2k}. Its cardinality is 2k - 1 (odd). Shadow closure shows S is closed under p. Since p is a fixed-point-free involution, S must have even cardinality. Parity contradiction.

4. The Catalan Equivalence

The full bijection NoncrossingPairing(n+1) ≃ Σ k, NCP(k) × NCP(n-k) that yields the Catalan recurrence when we take cardinalities.

def NoncrossingPairing (n : ℕ) : Type

Noncrossing pairings: the subtype of pairings that are noncrossing.

Equations

• NoncrossingPairing n = { p : Pairing n // p.IsNoncrossing }

Helper: extracting k from p(0) = 2k+1

noncomputable def extractK {n : ℕ} (p : Pairing (n + 1)) (h_nc : p.IsNoncrossing) : Fin (n + 1)

For a noncrossing pairing p on 2(n+1) points, p(0) = 2k+1 for some k < n+1. Returns k as a Fin (n+1).

Equations

• extractK p h_nc = ⟨↑(↑p ⟨0, ⋯⟩) / 2, ⋯⟩

theorem extractK_spec {n : ℕ} (p : Pairing (n + 1)) (h_nc : p.IsNoncrossing) : ↑(↑p ⟨0, ⋯⟩) = 2 * ↑(extractK p h_nc) + 1

The target of 0 equals 2 * extractK + 1.

theorem extractK_le {n : ℕ} (p : Pairing (n + 1)) (h_nc : p.IsNoncrossing) : ↑(extractK p h_nc) ≤ n

extractK gives a value ≤ n (so k ≤ n).

Helper: shadow closure for outside complement

theorem outside_closed_of_noncrossing {n : ℕ} (p : Pairing (n + 1)) (h_nc : p.IsNoncrossing) (x : Fin (2 * (n + 1))) (hx : 2 * ↑(extractK p h_nc) + 1 < ↑x) : 2 * ↑(extractK p h_nc) + 1 < ↑(↑p x)

The outside complement {i | 2k+1 < i} is closed under p when p is noncrossing and p(0) = 2k+1.

Proof: p(x) cannot be 0 (involution would force p(0)=x, but p(0)<x). p(x) cannot equal p(0) (injectivity, x≠0). p(x) cannot be in the shadow (shadow closure would force x into the shadow). So p(x) > 2k+1.

Helper: the inside pairing

Given a noncrossing pairing p on 2(n+1) with p(0) = 2k+1, the shadow
{1,...,2k} is closed under p. Restricting p to this interval and
translating via insideEquiv gives a noncrossing pairing on 2k points.

The construction requires:
1. Building the restricted permutation (shadow closure + involution → bijection)
2. Proving it's a pairing (inherited involution + fpf)
3. Proving it's noncrossing (no crossing lifts to crossing of p) 

noncomputable def restrictInsidePerm {n : ℕ} (p : Pairing (n + 1)) (h_nc : p.IsNoncrossing) : Equiv.Perm (Fin (2 * ↑(extractK p h_nc)))

The restricted permutation on the inside interval Fin(2k). Maps j to p(j+1) - 1. The involution of p provides the inverse.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def insidePairing {n : ℕ} (p : Pairing (n + 1)) (h_nc : p.IsNoncrossing) : NoncrossingPairing ↑(extractK p h_nc)

The inside noncrossing pairing extracted from a noncrossing pairing p on 2(n+1) points with p(0) = 2k+1.

Equations

• insidePairing p h_nc = ⟨⟨restrictInsidePerm p h_nc, ⋯⟩, ⋯⟩

noncomputable def restrictOutsidePerm {n : ℕ} (p : Pairing (n + 1)) (h_nc : p.IsNoncrossing) : Equiv.Perm (Fin (2 * (n - ↑(extractK p h_nc))))

The restricted permutation on the outside interval Fin(2(n-k)). Maps j to p(j + 2k + 2) - (2k + 2).

Equations

• One or more equations did not get rendered due to their size.

noncomputable def outsidePairing {n : ℕ} (p : Pairing (n + 1)) (h_nc : p.IsNoncrossing) : NoncrossingPairing (n - ↑(extractK p h_nc))

The outside noncrossing pairing extracted from a noncrossing pairing p on 2(n+1) points with p(0) = 2k+1.

Equations

• outsidePairing p h_nc = ⟨⟨restrictOutsidePerm p h_nc, ⋯⟩, ⋯⟩

Assembly: the inverse direction

Given k and noncrossing pairings on the inside and outside intervals, assemble a noncrossing pairing on 2(n+1) points.

noncomputable def assembleF (n : ℕ) (k : Fin (n + 1)) (p_in : Equiv.Perm (Fin (2 * ↑k))) (p_out : Equiv.Perm (Fin (2 * (n - ↑k)))) : Fin (2 * (n + 1)) → Fin (2 * (n + 1))

The assembly function: given k, p_in on Fin(2k), p_out on Fin(2(n-k)), build the permutation on Fin(2(n+1)) that sends 0↔2k+1 and translates p_in to the inside interval and p_out to the outside.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def assemblePerm (n : ℕ) (k : Fin (n + 1)) (p_in : Equiv.Perm (Fin (2 * ↑k))) (p_out : Equiv.Perm (Fin (2 * (n - ↑k)))) (hinv_in : ∀ (x : Fin (2 * ↑k)), p_in (p_in x) = x) (hinv_out : ∀ (x : Fin (2 * (n - ↑k))), p_out (p_out x) = x) : Equiv.Perm (Fin (2 * (n + 1)))

Build the assembled Perm from the involutive function.

Equations

• assemblePerm n k p_in p_out hinv_in hinv_out = Function.Involutive.toPerm (assembleF n k p_in p_out) ⋯

noncomputable def catalanAssemble (n : ℕ) (x : (k : Fin (n + 1)) × NoncrossingPairing ↑k × NoncrossingPairing (n - ↑k)) : NoncrossingPairing (n + 1)

The inverse of catalanDecompose: assemble a noncrossing pairing from k and independent inside/outside pairings.

Equations

• catalanAssemble n x = ⟨⟨assemblePerm n x.fst ↑↑x.snd.1 ↑↑x.snd.2 ⋯ ⋯, ⋯⟩, ⋯⟩

Round-trip lemmas for the Catalan equivalence

The Catalan equivalence

noncomputable def catalanDecompose (n : ℕ) (p : NoncrossingPairing (n + 1)) : (k : Fin (n + 1)) × NoncrossingPairing ↑k × NoncrossingPairing (n - ↑k)

The Catalan decomposition (forward direction): a noncrossing pairing on 2(n+1) points decomposes into k and independent noncrossing pairings on the inside and outside intervals.

Equations

• catalanDecompose n p = ⟨extractK ↑p ⋯, (insidePairing ↑p ⋯, outsidePairing ↑p ⋯)⟩

noncomputable def catalanEquiv (n : ℕ) : NoncrossingPairing (n + 1) ≃ (k : Fin (n + 1)) × NoncrossingPairing ↑k × NoncrossingPairing (n - ↑k)

The Catalan decomposition: a noncrossing pairing on 2(n+1) points decomposes into a choice of chord target k and independent noncrossing pairings on the inside and outside intervals.

Equations

• One or more equations did not get rendered due to their size.

5. Counting: NoncrossingPairing n has catalan n elements

genus_zero_count conceptually belongs with the genus/noncrossing story in GenusNoncrossing.lean, but is proved here because it requires catalanEquiv and the finitary cardinality machinery. The import direction (CatalanRecurrence imports GenusNoncrossing) makes this the only valid home.

@[implicit_reducible]

instance instDecidableIsNoncrossing {n : ℕ} (p : Pairing n) : Decidable p.IsNoncrossing

IsNoncrossing is decidable (via the genus characterization).

Equations

• instDecidableIsNoncrossing p = decidable_of_iff (p.genus = 0) ⋯

@[implicit_reducible]

instance instFintypeNoncrossingPairing {n : ℕ} : Fintype (NoncrossingPairing n)

Equations

• instFintypeNoncrossingPairing = Subtype.fintype Pairing.IsNoncrossing

theorem card_noncrossingPairing_eq_catalan (n : ℕ) : Fintype.card (NoncrossingPairing n) = catalan n

The number of noncrossing pairings on 2n points equals the nth Catalan number.

theorem Pairing.genus_zero_count {n : ℕ} : Fintype.card { p : Pairing n // p.genus = 0 } = catalan n

Corollary: the number of genus-zero pairings equals Cₙ.