Concrete incidence data for the fixed-tree form of (5.6)

The denominator in paper (5.6) counts only the finite pair consisting of branch exponents and leaf multiplicities. In particular, neither an admissible embedding nor a word witnessing a realization is part of the finite carrier below. Its multiplicities are arbitrary values at least two; the evenness supplied later by an across-pairing is not part of this count.

@[reducible, inline]

abbrev Anderson4D.ValidRealizationData (t : PlaneTree) (M m : ℕ) : Type

Valid restricted realization data for a fixed tree and tuple length. Embedding and word witnesses deliberately remain in the incidence relation, not in this finite type.

Equations

• Anderson4D.ValidRealizationData t M m = { d : t.RealizationData M m // d.IsValid }

def Anderson4D.validRealizationDataFinset (t : PlaneTree) (M m : ℕ) : Finset (ValidRealizationData t M m)

The finite carrier of all valid restricted realization data.

Equations

• Anderson4D.validRealizationDataFinset t M m = Finset.univ

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

Incidence of restricted data with a tuple, via the canonical marking and multiplicity bundles determined by the validity proof.

Equations

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

@[implicit_reducible]

noncomputable instance Anderson4D.validRealizationDataDecidableRel (t : PlaneTree) (M m : ℕ) : DecidableRel fun (d : ValidRealizationData t M m) (y : Fin m → Fin 4 → ℤ) => d.Realizes y

Equations

• Anderson4D.validRealizationDataDecidableRel t M m x✝¹ x✝ = Classical.propDecidable ((fun (d : Anderson4D.ValidRealizationData t M m) (y : Fin m → Fin 4 → ℤ) => d.Realizes y) x✝¹ x✝)

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

The restricted data incident to y for a fixed tree.

Equations

• Anderson4D.treeRealizationFiber t M m y = {d ∈ Anderson4D.validRealizationDataFinset t M m | d.Realizes y}

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

The concrete fixed-tree symmetry denominator in (5.6).

Equations

• Anderson4D.treeSymDenom t M m y = (Anderson4D.treeRealizationFiber t M m y).card

theorem Anderson4D.treeRealizationFiber_eq_realizationFiber (t : PlaneTree) (M m : ℕ) (y : Fin m → Fin 4 → ℤ) : treeRealizationFiber t M m y = realizationFiber (validRealizationDataFinset t M m) (fun (d : ValidRealizationData t M m) (y : Fin m → Fin 4 → ℤ) => d.Realizes y) y

theorem Anderson4D.treeSymDenom_eq_symDenom (t : PlaneTree) (M m : ℕ) (y : Fin m → Fin 4 → ℤ) : treeSymDenom t M m y = symDenom (validRealizationDataFinset t M m) (fun (d : ValidRealizationData t M m) (y : Fin m → Fin 4 → ℤ) => d.Realizes y) y

theorem Anderson4D.ValidRealizationData.realizes_precomp_perm_iff {t : PlaneTree} {M m : ℕ} (d : ValidRealizationData t M m) (σ : Equiv.Perm (Fin m)) (y : Fin m → Fin 4 → ℤ) : (d.Realizes fun (j : Fin m) => y (σ j)) ↔ d.Realizes y

Realization incidence is invariant under permuting tuple indices.

theorem Anderson4D.treeSymDenom_precomp_perm (t : PlaneTree) (M m : ℕ) (σ : Equiv.Perm (Fin m)) (y : Fin m → Fin 4 → ℤ) : (treeSymDenom t M m fun (j : Fin m) => y (σ j)) = treeSymDenom t M m y

Consequently the concrete symmetry denominator is invariant under permuting the indices of the tuple.

theorem Anderson4D.realizesTuple_congr_restricted {t : PlaneTree} {Nm Nm' : t.HeppMarking} {mu mu' : t.Multiplicities} {M m : ℕ} {y : Fin m → Fin 4 → ℤ} (hNm : Nm.EqOnBranch Nm') (hmu : mu.EqOnLeaves mu') : RealizesTuple t Nm mu M y ↔ RealizesTuple t Nm' mu' M y

RealizesTuple is insensitive to junk marking values off branch nodes and junk multiplicity values off leaves.

theorem Anderson4D.multiplicities_total_of_realizesTuple {t : PlaneTree} {Nm : t.HeppMarking} {mu : t.Multiplicities} {M m : ℕ} {y : Fin m → Fin 4 → ℤ} (h : RealizesTuple t Nm mu M y) : ∑ l : ↥t.Leaves, mu.m ↑l = m

Every concrete realization witness forces the total leaf multiplicity to equal the tuple length.

theorem Anderson4D.treeSymDenom_pos_of_realizesTuple {t : PlaneTree} {M m : ℕ} {y : Fin m → Fin 4 → ℤ} (ht : t.isValid = true) (Nm : t.HeppMarking) (mu : t.Multiplicities) (hscale : ∀ v ∈ t.BranchNodes, ↑(scaleN Nm v) ≤ 4 * ↑M) (htotal : ∑ l : ↥t.Leaves, mu.m ↑l = m) (hreal : RealizesTuple t Nm mu M y) : 0 < treeSymDenom t M m y

An actual valid-tree realization by bounded bundle data contributes an element to the concrete incidence fiber, so its denominator is positive.

theorem Anderson4D.treeSymDenom_pos_of_realizesTuple_autoTotal {t : PlaneTree} {M m : ℕ} {y : Fin m → Fin 4 → ℤ} (ht : t.isValid = true) (Nm : t.HeppMarking) (mu : t.Multiplicities) (hscale : ∀ v ∈ t.BranchNodes, ↑(scaleN Nm v) ≤ 4 * ↑M) (hreal : RealizesTuple t Nm mu M y) : 0 < treeSymDenom t M m y

Convenience form in which the total-multiplicity equation is recovered from the realization word itself; no parity hypothesis is needed.

theorem Anderson4D.treeSymDenom_pos_of_realizesTuple_even {t : PlaneTree} {M m : ℕ} {y : Fin m → Fin 4 → ℤ} (ht : t.isValid = true) (Nm : t.HeppMarking) (mu : t.Multiplicities) (hscale : ∀ v ∈ t.BranchNodes, ↑(scaleN Nm v) ≤ 4 * ↑M) (_heven : ∀ (l : ↥t.Leaves), Even (mu.m ↑l)) (hreal : RealizesTuple t Nm mu M y) : 0 < treeSymDenom t M m y

Paired-vector compatibility wrapper. Evenness remains available as an extra property, but does not alter the general denominator.

theorem Anderson4D.exists_treeSymDenom_pos_of_across_pairing (M m : ℕ) (hm : 1 ≤ m) (A : Finset (Fin m)) (y : Fin m → Fin 4 → ℤ) (hy : y ∈ rdec_boundedTuples M m) (κ : AcrossPairing A) (hκ : RespectsWord A y κ) : ∃ (t : PlaneTree), t.isValid = true ∧ 0 < treeSymDenom t M m y

The paired-vector existence theorem supplies a valid tree whose concrete fixed-tree denominator is positive.

theorem Anderson4D.sum_eq_sum_tree_incidence_div (t : PlaneTree) (M m : ℕ) (Y : Finset (Fin m → Fin 4 → ℤ)) (F : (Fin m → Fin 4 → ℤ) → ℝ) (hcover : ∀ y ∈ Y, ∃ (d : ValidRealizationData t M m), d.Realizes y) : ∑ y ∈ Y, F y = ∑ d ∈ validRealizationDataFinset t M m, ∑ y ∈ Y with d.Realizes y, F y / ↑(treeSymDenom t M m y)

Fixed-tree finite-incidence resummation, the abstract content of paper (5.6), specialized to the restricted realization data above.