Run compression preserves the filtered chain weight

Equal-letter edges have lattice weight one. Consequently the Hepp-chain weight is unchanged by run compression; primitivity transport and the destutter chain condition identify the two filtered weights used in Propositions 5.7 and 5.9.

theorem Anderson4D.heppChainWeight_mergedWord {t : PlaneTree} {M : ℕ} (z : HeppLeaf t → Fin 4 → ℤ) (w : Fin M → HeppLeaf t) : heppChainWeight z (mergedWord w) = heppChainWeight z w

Exact Hepp-chain-weight invariance under run compression.

theorem Anderson4D.heppChainWeight_listWord_mergedWordList {t : PlaneTree} {M : ℕ} (z : HeppLeaf t → Fin 4 → ℤ) (w : Fin M → HeppLeaf t) : heppChainWeight z (listWord (mergedWordList w)) = heppChainWeight z w

List-facing form used by the profile regrouping: evaluating the compressed representative list has the original chain weight.

theorem Anderson4D.primitiveSeparatedChainWeight_mergedWord_of_primitive {t : PlaneTree} {M : ℕ} (z : HeppLeaf t → Fin 4 → ℤ) (w : Fin M → HeppLeaf t) (hprimitive : NoProperLeafBlock w) : primitiveSeparatedChainWeight z (mergedWord w) = primitiveChainWeight z w

On a primitive original word, the P-5.7 weight is exactly the P-5.9 primitive-and-separated weight of its run compression.