Simple/compound leaf-factor ledger under collapse

The leaf factors in (5.45) split over the inside and outside leaf carriers. The contracted tree contributes the same outside factors plus exactly one new compound-marker factor ((s+1)!)^(3/4).

noncomputable def Anderson4D.paperLeafFactor {t : PlaneTree} (mu : t.Multiplicities) (compound : Finset t.VPos) (l : HeppLeaf t) : ℝ

Unified version of the paper's simple/compound leaf factor.

Equations

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

noncomputable def Anderson4D.paperLeafProduct {t : PlaneTree} (mu : t.Multiplicities) (compound : Finset t.VPos) : ℝ

Product of all unified leaf factors.

Equations

• Anderson4D.paperLeafProduct mu compound = ∏ l : Anderson4D.HeppLeaf t, Anderson4D.paperLeafFactor mu compound l

theorem Anderson4D.paperLeafProduct_eq_simple_mul_compound {t : PlaneTree} (mu : t.Multiplicities) (compound : Finset t.VPos) : paperLeafProduct mu compound = (∏ l ∈ simpleLeaves t compound, sqrtFactorial (mu.m l)) * ∏ l ∈ compoundLeaves t compound, factorialThreeQuarters (mu.m l)

The unified product is exactly the two leaf products printed in (5.33)/(5.39).

noncomputable def Anderson4D.insidePaperLeafProduct {t : PlaneTree} (mu : t.Multiplicities) (compound : Finset t.VPos) (r : t.VPos) : ℝ

Product of original factors over inside leaves.

Equations

• Anderson4D.insidePaperLeafProduct mu compound r = ∏ l : Anderson4D.InsideLeaf r, Anderson4D.paperLeafFactor mu compound ↑l

noncomputable def Anderson4D.outsidePaperLeafProduct {t : PlaneTree} (mu : t.Multiplicities) (compound : Finset t.VPos) (r : t.VPos) : ℝ

Product of original factors over outside leaves.

Equations

• Anderson4D.outsidePaperLeafProduct mu compound r = ∏ l : Anderson4D.OutsideLeaf r, Anderson4D.paperLeafFactor mu compound ↑l

theorem Anderson4D.paperLeafProduct_eq_inside_mul_outside {t : PlaneTree} (mu : t.Multiplicities) (compound : Finset t.VPos) (r : t.VPos) : paperLeafProduct mu compound = insidePaperLeafProduct mu compound r * outsidePaperLeafProduct mu compound r

Original leaf factors split exactly into inside and outside products.

theorem Anderson4D.paperLeafFactor_restrict {t : PlaneTree} (mu : t.Multiplicities) (compound : Finset t.VPos) (r : t.VPos) (l : HeppLeaf (t.subtreeAt ↑r)) : paperLeafFactor (restrictMultiplicities mu r) (restrictCompound r compound) l = paperLeafFactor mu compound ↑((restrictLeafEquiv r) l)

Restriction preserves the unified factor of each inside leaf.

theorem Anderson4D.paperLeafProduct_restrict {t : PlaneTree} (mu : t.Multiplicities) (compound : Finset t.VPos) (r : t.VPos) : paperLeafProduct (restrictMultiplicities mu r) (restrictCompound r compound) = insidePaperLeafProduct mu compound r

The restricted tree's leaf product is exactly the original inside product.

@[simp]

theorem Anderson4D.paperLeafFactor_contract_marker {t : PlaneTree} (mu : t.Multiplicities) (compound : Finset t.VPos) (r : t.VPos) (s : ℕ) (hs : 1 ≤ s) : paperLeafFactor (contractMultiplicities mu r s hs) (contractCompound r compound) (contractMarkerLeaf r) = factorialThreeQuarters (s + 1)

The contracted marker contributes exactly its compound factor.

@[simp]

theorem Anderson4D.paperLeafFactor_contract_outside {t : PlaneTree} (mu : t.Multiplicities) (compound : Finset t.VPos) (r : t.VPos) (s : ℕ) (hs : 1 ≤ s) (l : OutsideLeaf r) : paperLeafFactor (contractMultiplicities mu r s hs) (contractCompound r compound) (contractOutsideLeaf r l) = paperLeafFactor mu compound ↑l

Every contracted outside leaf retains its original leaf factor.

theorem Anderson4D.paperLeafProduct_contract {t : PlaneTree} (mu : t.Multiplicities) (compound : Finset t.VPos) (r : t.VPos) (s : ℕ) (hs : 1 ≤ s) : paperLeafProduct (contractMultiplicities mu r s hs) (contractCompound r compound) = factorialThreeQuarters (s + 1) * outsidePaperLeafProduct mu compound r

Contracted leaf product = marker factor × original outside product.

theorem Anderson4D.paperLeafProduct_restrict_mul_contract {t : PlaneTree} (mu : t.Multiplicities) (compound : Finset t.VPos) (r : t.VPos) (s : ℕ) (hs : 1 ≤ s) : paperLeafProduct (restrictMultiplicities mu r) (restrictCompound r compound) * paperLeafProduct (contractMultiplicities mu r s hs) (contractCompound r compound) = paperLeafProduct mu compound * factorialThreeQuarters (s + 1)

Complete leaf-factor ledger used in (5.45).