Factored target for Proposition 5.7

The final run-compression argument uses the same factorial/leaf/scale summand repeatedly. Naming it keeps the profile, factorial, and constant ledgers independent while preserving the frozen statement definitionally.

noncomputable def Anderson4D.permSumSummand (n : ℕ) {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (W : Finset t.VPos) : ℝ

One summand of the Proposition 5.7 right-hand side, without its global constant power.

Equations

• Anderson4D.permSumSummand n Nm mu W = (↑(n - W.card).factorial * ∏ l : Anderson4D.HeppLeaf t, Anderson4D.sqrtFactorial (Anderson4D.leafMultiplicity mu l)) * Anderson4D.permSumScaleTail Nm W

theorem Anderson4D.permSumSummand_nonneg (n : ℕ) {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (W : Finset t.VPos) : 0 ≤ permSumSummand n Nm mu W

theorem Anderson4D.permSumRHS_eq_factored (C : ℝ) (n : ℕ) (t : PlaneTree) (Nm : t.HeppMarking) (mu : t.Multiplicities) : permSumRHS C n t Nm mu = C ^ n * ∑ W ∈ (nonrootBranches t).powerset, permSumSummand n Nm mu W

The frozen right-hand side is the global power times the named nonnegative W-sum.

theorem Anderson4D.sum_permSumSummand_nonneg (n : ℕ) {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) : 0 ≤ ∑ W ∈ (nonrootBranches t).powerset, permSumSummand n Nm mu W

The target sum without its global constant is nonnegative.