Across-half pairings and the factorial bound in paper (5.10)

This file isolates the finite combinatorics used in the master decomposition. For a fixed half A ⊆ Fin m, an across pairing is a bijection from A to its complement. A pairing respects a word when paired positions carry the same letter. Restricting such a pairing to each letter fiber gives an injective map into a family of fiberwise equivalences. Consequently the number of compatible pairings is at most

∏ a, (mult a / 2)!.

Together with the definitional factorial ledger paperSum, this is exactly the factor in (5.10).

@[reducible, inline]

abbrev Anderson4D.AcrossPairing {m : ℕ} (A : Finset (Fin m)) : Type

A pairing across a fixed half A: a bijection from A to its complement.

Equations

• Anderson4D.AcrossPairing A = (↥A ≃ ↥Aᶜ)

def Anderson4D.RespectsWord {α : Type u_1} {m : ℕ} (A : Finset (Fin m)) (w : Fin m → α) (κ : AcrossPairing A) : Prop

An across pairing respects w when paired positions carry the same letter.

Equations

• Anderson4D.RespectsWord A w κ = ∀ (j : ↥A), w ↑j = w ↑(κ j)

@[implicit_reducible]

instance Anderson4D.instDecidablePredAcrossPairingRespectsWord {α : Type u_1} [DecidableEq α] {m : ℕ} (A : Finset (Fin m)) (w : Fin m → α) : DecidablePred (RespectsWord A w)

Equations

• Anderson4D.instDecidablePredAcrossPairingRespectsWord A w κ = Anderson4D.instDecidablePredAcrossPairingRespectsWord._aux_1 A w κ

def Anderson4D.compatibleAcrossPairings {α : Type u_1} [DecidableEq α] {m : ℕ} (A : Finset (Fin m)) (w : Fin m → α) : Finset (AcrossPairing A)

The finite set of across pairings compatible with a word.

Equations

• Anderson4D.compatibleAcrossPairings A w = Finset.filter (Anderson4D.RespectsWord A w) Finset.univ

@[simp]

theorem Anderson4D.mem_compatibleAcrossPairings {α : Type u_1} [DecidableEq α] {m : ℕ} {A : Finset (Fin m)} {w : Fin m → α} {κ : AcrossPairing A} : κ ∈ compatibleAcrossPairings A w ↔ RespectsWord A w κ

@[reducible, inline]

abbrev Anderson4D.leftFiber {α : Type u_1} [DecidableEq α] {m : ℕ} (A : Finset (Fin m)) (w : Fin m → α) (a : α) : Type

Positions in A carrying the letter a.

Equations

• Anderson4D.leftFiber A w a = ↥({j ∈ A | w j = a})

@[reducible, inline]

abbrev Anderson4D.rightFiber {α : Type u_1} [DecidableEq α] {m : ℕ} (A : Finset (Fin m)) (w : Fin m → α) (a : α) : Type

Positions outside A carrying the letter a.

Equations

• Anderson4D.rightFiber A w a = ↥({j ∉ A | w j = a})

def Anderson4D.restrictFiberEquiv {α : Type u_1} [DecidableEq α] {m : ℕ} (A : Finset (Fin m)) (w : Fin m → α) (κ : AcrossPairing A) (hκ : RespectsWord A w κ) (a : α) : leftFiber A w a ≃ rightFiber A w a

A compatible across pairing restricts to an equivalence on every letter fiber.

Equations

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

def Anderson4D.compatibleToFiberEquivs {α : Type u_1} [DecidableEq α] {m : ℕ} (A : Finset (Fin m)) (w : Fin m → α) : { κ : AcrossPairing A // RespectsWord A w κ } → (a : α) → leftFiber A w a ≃ rightFiber A w a

Compatible pairings inject into the family of their letter-fiber restrictions.

Equations

• Anderson4D.compatibleToFiberEquivs A w κ a = Anderson4D.restrictFiberEquiv A w ↑κ ⋯ a

theorem Anderson4D.compatibleToFiberEquivs_injective {α : Type u_1} [DecidableEq α] {m : ℕ} (A : Finset (Fin m)) (w : Fin m → α) : Function.Injective (compatibleToFiberEquivs A w)

theorem Anderson4D.card_leftFiber {α : Type u_1} [DecidableEq α] {m : ℕ} (A : Finset (Fin m)) (w : Fin m → α) (a : α) : Fintype.card (leftFiber A w a) = {j ∈ A | w j = a}.card

theorem Anderson4D.card_rightFiber {α : Type u_1} [DecidableEq α] {m : ℕ} (A : Finset (Fin m)) (w : Fin m → α) (a : α) : Fintype.card (rightFiber A w a) = {j ∉ A | w j = a}.card

theorem Anderson4D.card_leftFiber_add_card_rightFiber {α : Type u_1} [DecidableEq α] {m : ℕ} (A : Finset (Fin m)) (w : Fin m → α) (a : α) : Fintype.card (leftFiber A w a) + Fintype.card (rightFiber A w a) = {j : Fin m | w j = a}.card

theorem Anderson4D.even_mult_of_compatibleAcrossPairing {α : Type u_1} [Fintype α] [DecidableEq α] {m : ℕ} (A : Finset (Fin m)) (mult : α → ℕ) {w : Fin m → α} (hw : w ∈ validWords mult) (κ : AcrossPairing A) (hκ : RespectsWord A w κ) (a : α) : Even (mult a)

If a valid word admits a compatible across pairing, every prescribed letter multiplicity is even. This is the multiplicity clause of paper Lemma 5.5.

theorem Anderson4D.card_compatibleAcrossPairings_le {α : Type u_1} [Fintype α] [DecidableEq α] {m : ℕ} (A : Finset (Fin m)) (mult : α → ℕ) {w : Fin m → α} (hw : w ∈ validWords mult) : (compatibleAcrossPairings A w).card ≤ ∏ a : α, (mult a / 2).factorial

Fiber-counting bound: a compatible pairing has at most ∏ a, (mult a / 2)! possibilities.

def Anderson4D.pairedWordSum {α : Type u_1} [Fintype α] [DecidableEq α] {m : ℕ} (mult : α → ℕ) (A : Finset (Fin m)) (F : (Fin m → α) → ℝ) : ℝ

The left side of paper (5.10): sum over distinct multiset words, weighted by the number of compatible across-half pairings.

Equations

• Anderson4D.pairedWordSum mult A F = ∑ w ∈ Anderson4D.validWords mult, ↑(Anderson4D.compatibleAcrossPairings A w).card * F w

theorem Anderson4D.pairedWordSum_le_halfFactorial_mul_wordSum {α : Type u_1} [Fintype α] [DecidableEq α] {m : ℕ} (mult : α → ℕ) (A : Finset (Fin m)) (F : (Fin m → α) → ℝ) (hF : ∀ (w : Fin m → α), 0 ≤ F w) : pairedWordSum mult A F ≤ (∏ a : α, ↑(mult a / 2).factorial) * wordSum mult F

Word-level form of the factorial estimate underlying paper (5.10).

theorem Anderson4D.pairedWordSum_le_paperSum {α : Type u_1} [Fintype α] [DecidableEq α] {m : ℕ} (mult : α → ℕ) (A : Finset (Fin m)) (F : (Fin m → α) → ℝ) (hF : ∀ (w : Fin m → α), 0 ≤ F w) : pairedWordSum mult A F ≤ (∏ a : α, ↑(mult a / 2).factorial / ↑(mult a).factorial) * paperSum mult F

Paper (5.10), exact factorial normalization.

The labeled normalization is paperSum mult F = (∏ a, mult a!) * wordSum mult F. The compatible-pairing count cancels it to the printed factor ∏ a, (mult a / 2)! / mult a!.