Factorial normalization across run compression

paperSum carries the labeled-copy factorial ledger. When the multiplicity changes from ml to sl, the quotient of the two ledgers converts the compressed paperSum back to the original normalization.

noncomputable def Anderson4D.mergeLedgerRatio {α : Type u_1} [Fintype α] (ml sl : α → ℕ) : ℝ

Quotient of the original and compressed labeled-copy ledgers.

Equations

• Anderson4D.mergeLedgerRatio ml sl = ∏ a : α, ↑(ml a).factorial / ↑(sl a).factorial

theorem Anderson4D.mergeLedgerRatio_nonneg {α : Type u_1} [Fintype α] (ml sl : α → ℕ) : 0 ≤ mergeLedgerRatio ml sl

theorem Anderson4D.mergeLedgerRatio_mul_paperSum {α : Type u_1} [Fintype α] [DecidableEq α] {M : ℕ} (ml sl : α → ℕ) (F : (Fin M → α) → ℝ) : mergeLedgerRatio ml sl * paperSum sl F = (∏ a : α, ↑(ml a).factorial) * wordSum sl F

The quotient ledger times the compressed paperSum is the original factorial product times the compressed raw word sum.