Applying the inductive estimate after run compression

This module combines the compressed P-5.9 right-hand side with the factorial comparison (5.37). The result is expressed in the fixed P-5.7 W-sum; profile and expansion counting are deliberately left to the final finite-sum assembly.

theorem Anderson4D.mergeLedgerRatio_mul_inductiveRHSSummand_le {t : PlaneTree} {M n : ℕ} (ht : t.isValid = true) (hroot : t.rootV ∈ t.BranchNodes) (Nm : t.HeppMarking) (mu : t.Multiplicities) (w : Fin M → HeppLeaf t) (hvalid : w ∈ validWords (leafMultiplicity mu)) (hprimitive : NoProperLeafBlock w) (htotal : totalMultiplicity mu = 2 * n) (W : Finset t.VPos) (hW : W ⊆ nonrootBranches t) : mergeLedgerRatio (leafMultiplicity mu) (leafMultiplicity (mergedMultiplicities hroot mu w hvalid hprimitive)) * inductiveRHSSummand (mergedWordList w).length t Nm (mergedMultiplicities hroot mu w hvalid hprimitive) ∅ W ≤ 4 ^ n * permSumSummand n Nm mu W

Pointwise conversion of a compressed P-5.9 summand into the P-5.7 factorial/leaf/scale summand.

theorem Anderson4D.mergeLedgerRatio_mul_inductiveRHS_le {C0 D : ℝ} {t : PlaneTree} {M n : ℕ} (hC0 : 0 ≤ C0) (hD : 0 ≤ D) (ht : t.isValid = true) (hroot : t.rootV ∈ t.BranchNodes) (Nm : t.HeppMarking) (mu : t.Multiplicities) (w : Fin M → HeppLeaf t) (hvalid : w ∈ validWords (leafMultiplicity mu)) (hprimitive : NoProperLeafBlock w) (htotal : totalMultiplicity mu = 2 * n) : mergeLedgerRatio (leafMultiplicity mu) (leafMultiplicity (mergedMultiplicities hroot mu w hvalid hprimitive)) * inductiveRHS C0 D (mergedWordList w).length t Nm (mergedMultiplicities hroot mu w hvalid hprimitive) ∅ ≤ C0 ^ (mergedWordList w).length * D ^ t.BranchNodes.card * 4 ^ n * ∑ W ∈ (nonrootBranches t).powerset, permSumSummand n Nm mu W

The full compressed P-5.9 right-hand side, restored to the original factorial normalization, is bounded by the P-5.7 target sum with the explicit (5.37) loss.