The pairing sum over perfect matchings of Fin m

Category: 1-Mathlib (CSD-free; staged for upstream).

A perfect matching of Fin m is a fixed-point-free involution σ : Fin m → Fin m; its pairs are {i, σ i}. The pairing sum of a weight c : Fin m → Fin m → R is the sum over perfect matchings of the product over pairs, each pair {i, σ i} with i < σ i weighted c i (σ i) — the combinatorial skeleton of Wick's theorem (the hafnian when c is symmetric).

• IsPerfectMatching σ — ∀ i, σ (σ i) = i ∧ σ i ≠ i; pairingSum c — the sum over {σ // IsPerfectMatching σ} of ∏ i, if i < σ i then c i (σ i) else 1;
• pairingSum_zero (m = 0: the empty matching, value 1), pairingSum_one (m = 1: no matching, value 0);
• ★ pairingSum_succ_succ — the first-contraction recursion: for m = n + 2, pairingSum c = ∑ j : Fin (n + 1), c 0 j.succ · pairingSum (c ∘ emb j), where emb j : Fin n ↪ Fin (n + 2) is the order embedding onto the complement of {0, j.succ} (emb j a = (j.succAbove a).succ). A matching of Fin (n + 2) is the pair {0, j.succ} together with a matching of the rest, and the weights multiply (glue, the bijection glue_bijective);
• pairingSum_cast — transport along m = m';
• ★ card_isPerfectMatching_even / card_isPerfectMatching_odd — the number of perfect matchings of Fin (2n) is (2n − 1)‼, of Fin (2n + 1) zero: the pairing sum of the constant weight 1.

References: G. C. Wick, The evaluation of the collision matrix, Phys. Rev. 80, 268 (1950) (the pairing sum); CV/WickTime.lean (wickSum, the same recursion on words of the lattice field, and wickSum_eq_pairingSum); specs/BACKLOG.md #36(b)(iv′); specs/future-work.md.

Perfect matchings

def Fin.IsPerfectMatching {m : ℕ} (σ : Fin m → Fin m) : Prop

A perfect matching of Fin m: a fixed-point-free involution.

Equations

• Fin.IsPerfectMatching σ = ∀ (i : Fin m), σ (σ i) = i ∧ σ i ≠ i

@[instance_reducible]

instance Fin.instDecidablePredForallIsPerfectMatching {m : ℕ} : DecidablePred IsPerfectMatching

Equations

• Fin.instDecidablePredForallIsPerfectMatching σ = Fin.instDecidablePredForallIsPerfectMatching._aux_1 σ

def Fin.pairingSum {m : ℕ} {R : Type u_1} [CommSemiring R] (c : Fin m → Fin m → R) : R

The pairing sum of a weight c: over perfect matchings σ, the product over the pairs {i, σ i}, i < σ i, of c i (σ i).

Equations

• Fin.pairingSum c = ∑ σ : { σ : Fin m → Fin m // Fin.IsPerfectMatching σ }, ∏ i : Fin m, if i < ↑σ i then c i (↑σ i) else 1

@[instance_reducible]

instance Fin.instUniqueSubtypeIsPerfectMatchingZero : Unique { σ : Fin 0 → Fin 0 // IsPerfectMatching σ }

Equations

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

instance Fin.instIsEmptySubtypeIsPerfectMatchingOne : IsEmpty { σ : Fin 1 → Fin 1 // IsPerfectMatching σ }

theorem Fin.pairingSum_zero {R : Type u_1} [CommSemiring R] (c : Fin 0 → Fin 0 → R) : pairingSum c = 1

Fin 0 has one perfect matching, the empty one: the pairing sum is 1.

theorem Fin.pairingSum_one {R : Type u_1} [CommSemiring R] (c : Fin 1 → Fin 1 → R) : pairingSum c = 0

Fin 1 has no perfect matching: the pairing sum is 0.

The first-contraction recursion

def Fin.emb {n : ℕ} (j : Fin (n + 1)) (a : Fin n) : Fin (n + 2)

The order embedding of Fin n onto the complement of {0, j.succ} in Fin (n + 2).

Equations

• j.emb a = (j.succAbove a).succ

theorem Fin.emb_ne_zero {n : ℕ} (j : Fin (n + 1)) (a : Fin n) : j.emb a ≠ 0

theorem Fin.emb_ne_succ {n : ℕ} (j : Fin (n + 1)) (a : Fin n) : j.emb a ≠ j.succ

theorem Fin.emb_injective {n : ℕ} (j : Fin (n + 1)) : Function.Injective j.emb

theorem Fin.emb_lt_emb_iff {n : ℕ} (j : Fin (n + 1)) {a b : Fin n} : j.emb a < j.emb b ↔ a < b

theorem Fin.exists_emb_eq {n : ℕ} (j : Fin (n + 1)) {i : Fin (n + 2)} (h0 : i ≠ 0) (hj : i ≠ j.succ) : ∃ (a : Fin n), j.emb a = i

Every element of Fin (n + 2) other than 0 and j.succ is emb j a for a unique a.

def Fin.glue {n : ℕ} (j : Fin (n + 1)) (τ : Fin n → Fin n) : Fin (n + 2) → Fin (n + 2)

Gluing the pair {0, j.succ} onto a matching τ of the rest.

Equations

• j.glue τ = Fin.cons j.succ (j.insertNth 0 fun (a : Fin n) => j.emb (τ a))

@[simp]

theorem Fin.glue_zero {n : ℕ} (j : Fin (n + 1)) (τ : Fin n → Fin n) : j.glue τ 0 = j.succ

@[simp]

theorem Fin.glue_succ_self {n : ℕ} (j : Fin (n + 1)) (τ : Fin n → Fin n) : j.glue τ j.succ = 0

@[simp]

theorem Fin.glue_emb {n : ℕ} (j : Fin (n + 1)) (τ : Fin n → Fin n) (a : Fin n) : j.glue τ (j.emb a) = j.emb (τ a)

theorem Fin.cases_emb {n : ℕ} (j : Fin (n + 1)) {p : Fin (n + 2) → Prop} (h0 : p 0) (hj : p j.succ) (he : ∀ (a : Fin n), p (j.emb a)) (i : Fin (n + 2)) : p i

Case analysis on Fin (n + 2): 0, j.succ, or emb j a.

theorem Fin.glue_isPerfectMatching {n : ℕ} (j : Fin (n + 1)) {τ : Fin n → Fin n} (hτ : IsPerfectMatching τ) : IsPerfectMatching (j.glue τ)

def Fin.glueMap {n : ℕ} (j : Fin (n + 1)) : { τ : Fin n → Fin n // IsPerfectMatching τ } → { σ : Fin (n + 2) → Fin (n + 2) // IsPerfectMatching σ }

The gluing map from pairs (partner of 0, matching of the rest) to matchings.

Equations

• j.glueMap τ = ⟨j.glue ↑τ, ⋯⟩

def Fin.glueSigma {n : ℕ} : (_ : Fin (n + 1)) × { τ : Fin n → Fin n // IsPerfectMatching τ } → { σ : Fin (n + 2) → Fin (n + 2) // IsPerfectMatching σ }

The gluing map on the sigma type.

Equations

• Fin.glueSigma p = p.fst.glueMap p.snd

theorem Fin.glueSigma_injective {n : ℕ} : Function.Injective glueSigma

theorem Fin.glueSigma_surjective {n : ℕ} : Function.Surjective glueSigma

theorem Fin.glueSigma_bijective {n : ℕ} : Function.Bijective glueSigma

theorem Fin.prod_glue {n : ℕ} {R : Type u_1} [CommSemiring R] (c : Fin (n + 2) → Fin (n + 2) → R) (j : Fin (n + 1)) (τ : Fin n → Fin n) : (∏ i : Fin (n + 2), if i < j.glue τ i then c i (j.glue τ i) else 1) = c 0 j.succ * ∏ a : Fin n, if a < τ a then c (j.emb a) (j.emb (τ a)) else 1

The weight of a glued matching: the pair {0, j.succ} times the weight of the rest.

theorem Fin.pairingSum_succ_succ {n : ℕ} {R : Type u_1} [CommSemiring R] (c : Fin (n + 2) → Fin (n + 2) → R) : pairingSum c = ∑ j : Fin (n + 1), c 0 j.succ * pairingSum fun (a b : Fin n) => c (j.emb a) (j.emb b)

★ The first-contraction recursion. A perfect matching of Fin (n + 2) is the pair {0, j.succ} together with a perfect matching of the complement, and the weights multiply.

Transport and counting

theorem Fin.pairingSum_cast {R : Type u_1} [CommSemiring R] {m m' : ℕ} (h : m = m') (c : Fin m' → Fin m' → R) : (pairingSum fun (a b : Fin m) => c (Fin.cast h a) (Fin.cast h b)) = pairingSum c

Transport of the pairing sum along m = m'.

theorem Fin.pairingSum_one_eq_card (m : ℕ) : (pairingSum fun (x x_1 : Fin m) => 1) = Fintype.card { σ : Fin m → Fin m // IsPerfectMatching σ }

The pairing sum of the constant weight 1 counts the perfect matchings.

theorem Fin.card_isPerfectMatching_even (n : ℕ) : Fintype.card { σ : Fin (2 * n) → Fin (2 * n) // IsPerfectMatching σ } = (2 * n - 1).doubleFactorial

★ Fin (2n) has (2n − 1)‼ perfect matchings.

theorem Fin.card_isPerfectMatching_odd (n : ℕ) : Fintype.card { σ : Fin (2 * n + 1) → Fin (2 * n + 1) // IsPerfectMatching σ } = 0

Fin (2n + 1) has no perfect matching.