Tree-facing factorial comparison after run compression

This module specializes the numerical factorial estimate (5.37) to the original and run-compressed multiplicities of one primitive valid Hepp-leaf word. In particular, it discharges the coordinatewise, total-mass, and skipped-branch hypotheses needed by mergeFactorialBefore_le_four_pow.

theorem Anderson4D.mergedMultiplicity_le_leafMultiplicity_of_valid {t : PlaneTree} {M : ℕ} (mu : t.Multiplicities) (w : Fin M → HeppLeaf t) (hvalid : w ∈ validWords (leafMultiplicity mu)) (l : HeppLeaf t) : mergedMultiplicity w l ≤ leafMultiplicity mu l

Run compression cannot increase the multiplicity of any leaf in a word with the prescribed original multiplicities.

theorem Anderson4D.two_mul_card_le_mergedWordList_length {t : PlaneTree} {M : ℕ} (ht : t.isValid = true) (hroot : t.rootV ∈ t.BranchNodes) (mu : t.Multiplicities) (w : Fin M → HeppLeaf t) (hvalid : w ∈ validWords (leafMultiplicity mu)) (hprimitive : NoProperLeafBlock w) (W : Finset t.VPos) (hW : W ⊆ nonrootBranches t) : 2 * W.card ≤ (mergedWordList w).length

A subset of non-root branches is paid for by the total run-compressed multiplicity. The off-marker branch/leaf count uses the lower bound two built into mergedMultiplicities.

theorem Anderson4D.merged_factorial_leaf_product_le_four_pow {t : PlaneTree} {M n : ℕ} (ht : t.isValid = true) (hroot : t.rootV ∈ t.BranchNodes) (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) : (sqrtFactorial ((mergedWordList w).length - 2 * W.card) * ∏ l : HeppLeaf t, sqrtFactorial (leafMultiplicity (mergedMultiplicities hroot mu w hvalid hprimitive) l)) * ∏ l : HeppLeaf t, ↑(leafMultiplicity mu l).factorial / ↑(leafMultiplicity (mergedMultiplicities hroot mu w hvalid hprimitive) l).factorial ≤ 4 ^ n * ↑(n - W.card).factorial * ∏ l : HeppLeaf t, sqrtFactorial (leafMultiplicity mu l)

Tree-facing form of paper (5.37).

The left side is exactly the compressed P-5.9 factorial/leaf factor, multiplied by the factorial-ledger ratios that recover the original multiplicities. The right side is the P-5.7 factorial/leaf factor with the explicit uniform loss 4^n.