Leaf payoff ledger for the end of Proposition 5.10

The inner estimate supplies one inverse-square parent scale per labeled copy. The outer majority estimate supplies originalOuterLeafPayoff. This file combines those two products exactly into the simple/compound factorial and scale products printed in (5.89).

theorem Anderson4D.globalFactorialOuterPayoff_eq {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (compound : Finset t.VPos) : ∏ l : HeppLeaf t, sqrtFactorial (leafMultiplicity mu l) * originalOuterLeafPayoff Nm mu compound l = (∏ l ∈ simpleLeaves t compound, sqrtFactorial (mu.m l) * ↑(scaleN Nm (PlaneTree.parentV l)) ^ (2 * (mu.m l - 2))) * ∏ l ∈ compoundLeaves t compound, factorialThreeQuarters (mu.m l)

The global factorial/outer-payoff product, split over the exact simple and compound leaf partition.

theorem Anderson4D.globalBaseScaleFactorialOuterPayoff_eq {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (compound : Finset t.VPos) : (∏ l : HeppLeaf t, ↑(scaleN Nm (PlaneTree.parentV ↑l)) ^ (-2 * ↑(leafMultiplicity mu l))) * ∏ l : HeppLeaf t, sqrtFactorial (leafMultiplicity mu l) * originalOuterLeafPayoff Nm mu compound l = (((∏ l ∈ simpleLeaves t compound, sqrtFactorial (mu.m l)) * ∏ l ∈ compoundLeaves t compound, factorialThreeQuarters (mu.m l)) * ∏ l ∈ simpleLeaves t compound, ↑(scaleN Nm (PlaneTree.parentV l)) ^ (-4)) * ∏ l ∈ compoundLeaves t compound, ↑(scaleN Nm (PlaneTree.parentV l)) ^ (-2 * ↑(mu.m l))

Exact (5.88)-to-(5.89) leaf ledger. One inverse-square parent-scale factor per labeled copy combines with the outer payoff to leave exponent -4 on simple leaves and exponent -2m_l on compound leaves.