Fixed-datum scalar and skipped-set assembly

For one raw collapse datum, this file combines the exact factor audit, the final scalar inequality, and the injective W ↦ W' regrouping. The result has exactly the global coefficient and W'-sum of the original-tree induction right-hand side.

theorem Anderson4D.inductiveRHSSummand_nonneg (m : ℕ) (t : PlaneTree) (Nm : t.HeppMarking) (mu : t.Multiplicities) (compound W : Finset t.VPos) : 0 ≤ inductiveRHSSummand m t Nm mu compound W

Every named summand of the factored induction right-hand side is nonnegative.

theorem Anderson4D.two_pow_mul_sum_combinedCollapseTerm_le_inductiveRHSSum (C0 D : ℝ) (hC0 : 1000 < C0) (hD : D = Real.exp (C0 ^ 10)) {t : PlaneTree} (ht : t.isValid = true) (hroot : t.rootV ∈ t.BranchNodes) (Nm : t.HeppMarking) (mu : t.Multiplicities) (compound : Finset t.VPos) (r : t.VPos) (hr : r ∈ nonrootBranches t) (d : RawCollapseData (InsideLeaf r) (OutsideLeaf r)) (hSpec : CollapseMultiplicitySpec (splitLeafMultiplicity mu r) d) (hblocks : 2 ≤ d.blocks.length) : 2 ^ d.insideLength * ∑ W ∈ (nonrootBranches (t.contractAt ↑r)).powerset, combinedCollapseTerm C0 D d.insideLength (collapseCutCount d) d.collapsed.length Nm mu compound r ⋯ W ≤ C0 ^ totalMultiplicity mu * D ^ t.BranchNodes.card * ∑ W' ∈ (nonrootBranches t).powerset, inductiveRHSSummand (totalMultiplicity mu) t Nm mu compound W'

Final fixed-datum scalar and W-sum bound.