Filtered-sum forms of the paper weights

The paper-facing statements package side conditions into if-weighted summands. Internal permutation-sum proofs instead use paperSumFiltered. This file supplies the exact conversion and nonnegativity lemmas at that boundary.

theorem Anderson4D.latticeEdgeWeight_nonneg (x y : Fin 4 → ℤ) : 0 ≤ latticeEdgeWeight x y

theorem Anderson4D.heppChainWeight_nonneg {t : PlaneTree} {m : ℕ} (z : HeppLeaf t → Fin 4 → ℤ) (w : Fin m → HeppLeaf t) : 0 ≤ heppChainWeight z w

theorem Anderson4D.heppChainWeightExcept_nonneg {t : PlaneTree} {m : ℕ} (z : HeppLeaf t → Fin 4 → ℤ) (O : Finset (AdjacentIndex m)) (w : Fin m → HeppLeaf t) : 0 ≤ heppChainWeightExcept z O w

theorem Anderson4D.primitiveChainWeight_nonneg {t : PlaneTree} {m : ℕ} (z : HeppLeaf t → Fin 4 → ℤ) (w : Fin m → HeppLeaf t) : 0 ≤ primitiveChainWeight z w

theorem Anderson4D.primitiveSeparatedChainWeight_nonneg {t : PlaneTree} {m : ℕ} (z : HeppLeaf t → Fin 4 → ℤ) (w : Fin m → HeppLeaf t) : 0 ≤ primitiveSeparatedChainWeight z w

theorem Anderson4D.singleScaleChainWeight_nonneg {t : PlaneTree} {m : ℕ} (z : HeppLeaf t → Fin 4 → ℤ) (O : Finset (AdjacentIndex m)) (w : Fin m → HeppLeaf t) : 0 ≤ singleScaleChainWeight z O w

theorem Anderson4D.paperSum_primitiveChainWeight {t : PlaneTree} {m : ℕ} (mu : t.Multiplicities) (z : HeppLeaf t → Fin 4 → ℤ) : paperSum (leafMultiplicity mu) (primitiveChainWeight z) = paperSumFiltered (leafMultiplicity mu) NoProperLeafBlock (heppChainWeight z)

The left side of Proposition 5.7 as a filtered paperSum.

theorem Anderson4D.paperSum_primitiveSeparatedChainWeight {t : PlaneTree} {m : ℕ} (mu : t.Multiplicities) (z : HeppLeaf t → Fin 4 → ℤ) : paperSum (leafMultiplicity mu) (primitiveSeparatedChainWeight z) = paperSumFiltered (leafMultiplicity mu) (fun (w : Fin m → HeppLeaf t) => NoProperLeafBlock w ∧ NoAdjacentEqual w) (heppChainWeight z)

The left side of Proposition 5.9 as a doubly filtered paperSum.

theorem Anderson4D.paperSum_singleScaleChainWeight {t : PlaneTree} {m : ℕ} (mu : t.Multiplicities) (z : HeppLeaf t → Fin 4 → ℤ) (O : Finset (AdjacentIndex m)) : paperSum (leafMultiplicity mu) (singleScaleChainWeight z O) = paperSumFiltered (leafMultiplicity mu) (NoAdjacentOutside O) (heppChainWeightExcept z O)

The left side of Proposition 5.10 as a filtered paperSum.