Even-multiplicity incidence for the paper's paired decomposition

The denominator in paper (5.6) ranges over branch-scale and leaf-multiplicity data whose leaf multiplicities are even. The general incidence carrier in Incidence is useful for Proposition 5.6, where arbitrary multiplicities at least two occur. This file supplies the paired specialization and proves that, for a tuple equipped with an across-half pairing, its general and paired incidence fibers have the same cardinality.

def Anderson4D.pairedValidRealizationDataFinset (t : PlaneTree) (M m : ℕ) : Finset (t.PairedValidRealizationData M m)

The finite carrier of restricted realization data with even leaf multiplicities, exactly as in the denominator of paper (5.6).

Equations

• Anderson4D.pairedValidRealizationDataFinset t M m = Finset.univ

def Anderson4D.PairedDataRealizes {t : PlaneTree} {M m : ℕ} (d : t.PairedValidRealizationData M m) (y : Fin m → Fin 4 → ℤ) : Prop

Incidence of paired restricted data with a tuple.

Equations

• Anderson4D.PairedDataRealizes d y = Anderson4D.RealizesTuple t ((↑d).toHeppMarking ⋯) ((↑d).toMultiplicities ⋯) M y

@[implicit_reducible]

noncomputable instance Anderson4D.pairedValidRealizationDataDecidableRel (t : PlaneTree) (M m : ℕ) : DecidableRel fun (d : t.PairedValidRealizationData M m) (y : Fin m → Fin 4 → ℤ) => PairedDataRealizes d y

Equations

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

noncomputable def Anderson4D.pairedTreeRealizationFiber (t : PlaneTree) (M m : ℕ) (y : Fin m → Fin 4 → ℤ) : Finset (t.PairedValidRealizationData M m)

The even restricted data incident to y for a fixed tree.

Equations

• Anderson4D.pairedTreeRealizationFiber t M m y = {d ∈ Anderson4D.pairedValidRealizationDataFinset t M m | Anderson4D.PairedDataRealizes d y}

noncomputable def Anderson4D.pairedTreeSymDenom (t : PlaneTree) (M m : ℕ) (y : Fin m → Fin 4 → ℤ) : ℕ

The exact even-multiplicity symmetry denominator in paper (5.6).

Equations

• Anderson4D.pairedTreeSymDenom t M m y = (Anderson4D.pairedTreeRealizationFiber t M m y).card

def Anderson4D.pairedDataToValid {t : PlaneTree} {M m : ℕ} (d : t.PairedValidRealizationData M m) : ValidRealizationData t M m

Forget parity while retaining general validity.

Equations

• Anderson4D.pairedDataToValid d = ⟨↑d, ⋯⟩

@[simp]

theorem Anderson4D.pairedDataToValid_val {t : PlaneTree} {M m : ℕ} (d : t.PairedValidRealizationData M m) : ↑(pairedDataToValid d) = ↑d

theorem Anderson4D.pairedDataRealizes_toValid_iff {t : PlaneTree} {M m : ℕ} (d : t.PairedValidRealizationData M m) (y : Fin m → Fin 4 → ℤ) : (pairedDataToValid d).Realizes y ↔ PairedDataRealizes d y

Forgetting parity does not change the realization predicate.

theorem Anderson4D.ValidRealizationData.isEven_of_realizes_of_acrossPairing {t : PlaneTree} {M m : ℕ} (d : ValidRealizationData t M m) {y : Fin m → Fin 4 → ℤ} (hreal : d.Realizes y) (A : Finset (Fin m)) (κ : AcrossPairing A) (hκ : RespectsWord A y κ) : (↑d).IsEven

A realization of a tuple carrying an across-half pairing necessarily has even leaf multiplicities. This is the converse parity bridge needed to identify the two incidence fibers.

def Anderson4D.validDataToPairedOfAcrossPairing {t : PlaneTree} {M m : ℕ} (d : ValidRealizationData t M m) {y : Fin m → Fin 4 → ℤ} (hreal : d.Realizes y) (A : Finset (Fin m)) (κ : AcrossPairing A) (hκ : RespectsWord A y κ) : t.PairedValidRealizationData M m

Promote incident general data to paired-valid data using an across-half pairing on the realized tuple.

Equations

• Anderson4D.validDataToPairedOfAcrossPairing d hreal A κ hκ = ⟨↑d, ⋯⟩

@[simp]

theorem Anderson4D.validDataToPairedOfAcrossPairing_val {t : PlaneTree} {M m : ℕ} (d : ValidRealizationData t M m) {y : Fin m → Fin 4 → ℤ} (hreal : d.Realizes y) (A : Finset (Fin m)) (κ : AcrossPairing A) (hκ : RespectsWord A y κ) : ↑(validDataToPairedOfAcrossPairing d hreal A κ hκ) = ↑d

noncomputable def Anderson4D.treeRealizationFiberEquivPaired {t : PlaneTree} {M m : ℕ} {y : Fin m → Fin 4 → ℤ} (A : Finset (Fin m)) (κ : AcrossPairing A) (hκ : RespectsWord A y κ) : ↥(treeRealizationFiber t M m y) ≃ ↥(pairedTreeRealizationFiber t M m y)

On a paired tuple, forgetting and reconstructing parity gives an equivalence between the general and even incidence fibers.

Equations

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

theorem Anderson4D.treeSymDenom_eq_pairedTreeSymDenom {t : PlaneTree} {M m : ℕ} {y : Fin m → Fin 4 → ℤ} (A : Finset (Fin m)) (κ : AcrossPairing A) (hκ : RespectsWord A y κ) : treeSymDenom t M m y = pairedTreeSymDenom t M m y

For a tuple with an across-half pairing, allowing arbitrary multiplicities in the auxiliary denominator adds no incident data: every realizing multiplicity is automatically even.

theorem Anderson4D.pairedTreeSymDenom_pos_of_general {t : PlaneTree} {M m : ℕ} {y : Fin m → Fin 4 → ℤ} (A : Finset (Fin m)) (κ : AcrossPairing A) (hκ : RespectsWord A y κ) (hpos : 0 < treeSymDenom t M m y) : 0 < pairedTreeSymDenom t M m y

The paired denominator has the same orbit-stabilizer lower bound as the general denominator, by the preceding exact identification.

theorem Anderson4D.card_aut_le_pairedTreeSymDenom_mul_card_autHeppMarked {t : PlaneTree} {M m : ℕ} {y : Fin m → Fin 4 → ℤ} (ht : t.isValid = true) (Nm : t.HeppMarking) (mu : t.Multiplicities) (hreal : RealizesTuple t Nm mu M y) (A : Finset (Fin m)) (κ : AcrossPairing A) (hκ : RespectsWord A y κ) : Fintype.card t.Aut ≤ pairedTreeSymDenom t M m y * Fintype.card ↥(t.AutHeppMarked Nm)

Paper (5.12) with the exact even-multiplicity denominator from (5.6), in division-free form.

theorem Anderson4D.sum_eq_sum_paired_tree_incidence_div (t : PlaneTree) (M m : ℕ) (Y : Finset (Fin m → Fin 4 → ℤ)) (F : (Fin m → Fin 4 → ℤ) → ℝ) (hcover : ∀ y ∈ Y, ∃ (d : t.PairedValidRealizationData M m), PairedDataRealizes d y) : ∑ y ∈ Y, F y = ∑ d ∈ pairedValidRealizationDataFinset t M m, ∑ y ∈ Y with PairedDataRealizes d y, F y / ↑(pairedTreeSymDenom t M m y)

Fixed-tree finite-incidence resummation with the exact even denominator printed in paper (5.6).