Scale-tail ledger for the P-5.9 to P-5.7 merge

At compound = ∅, paper (5.31) identifies the squared parent-ratio part of the P-5.9 branch power with the branch/root scale power in P-5.7. The remaining W-complement ratio is unchanged.

noncomputable def Anderson4D.permSumScaleTail {t : PlaneTree} (Nm : t.HeppMarking) (W : Finset t.VPos) : ℝ

The scale and parent-ratio tail printed in P-5.7, equation (5.15).

Equations

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

theorem Anderson4D.allSimple_scale_ratio_tail_eq_permSumScaleTail {t : PlaneTree} (ht : t.isValid = true) (hroot : t.rootV ∈ t.BranchNodes) (Nm : t.HeppMarking) (mu : t.Multiplicities) (W : Finset t.VPos) : singleScaleBranchPower Nm mu ∅ * originalParentRatioFactor Nm W = permSumScaleTail Nm W

Paper (5.31), specialized to a Hepp marking. No incidence or parity hypothesis is needed: validity and the root-branch condition are precisely the assumptions of the existing combinatorial identity, while positivity of all branch scales follows from the marking.

@[simp]

theorem Anderson4D.paperLeafProduct_empty {t : PlaneTree} (mu : t.Multiplicities) : paperLeafProduct mu ∅ = ∏ l : HeppLeaf t, sqrtFactorial (leafMultiplicity mu l)

With no compound leaves, the named leaf product is the P-5.7 product of square-root factorials over all leaves.

theorem Anderson4D.inductiveRHSSummand_empty_eq_permSumScaleTail (m : ℕ) {t : PlaneTree} (ht : t.isValid = true) (hroot : t.rootV ∈ t.BranchNodes) (Nm : t.HeppMarking) (mu : t.Multiplicities) (W : Finset t.VPos) : inductiveRHSSummand m t Nm mu ∅ W = (sqrtFactorial (m - 2 * W.card) * ∏ l : HeppLeaf t, sqrtFactorial (leafMultiplicity mu l)) * permSumScaleTail Nm W

A P-5.9 summand at compound = ∅ is exactly the factorial/leaf factor and scale tail appearing in P-5.7.