Run merging and the paper's chain weight

This file connects the list-level run-merging API to the exact adjacent-index product used in Propositions 5.7 and 5.9. It verifies the observation before paper (5.35): merging a constant run does not change the inverse-square chain weight, because every removed internal edge has weight one.

def Anderson4D.chainLeftIndex {m : ℕ} (i : Fin m.pred) : Fin m

The left endpoint associated with an index in a chain of length m.

Equations

• Anderson4D.chainLeftIndex i = ⟨↑i, ⋯⟩

def Anderson4D.chainRightIndex {m : ℕ} (i : Fin m.pred) : Fin m

The right endpoint associated with an index in a chain of length m.

Equations

• Anderson4D.chainRightIndex i = ⟨↑i + 1, ⋯⟩

def Anderson4D.indexedChainProduct {α : Type u_1} {R : Type u_2} [CommMonoid R] {m : ℕ} (edge : α → α → R) (w : Fin m → α) : R

Fin-indexed form of a consecutive-edge product.

Equations

• Anderson4D.indexedChainProduct edge w = ∏ i : Fin m.pred, edge (w (Anderson4D.chainLeftIndex i)) (w (Anderson4D.chainRightIndex i))

theorem Anderson4D.listChainProduct_ofFn {α : Type u_1} {R : Type u_2} [CommMonoid R] {m : ℕ} (edge : α → α → R) (w : Fin m → α) : listChainProduct edge (List.ofFn w) = indexedChainProduct edge w

List and Fin-indexed consecutive-edge products agree.

def Anderson4D.adjacentIndexEquiv (m : ℕ) : AdjacentIndex m ≃ Fin m.pred

The paper's adjacency-index carrier is canonically Fin (m-1).

Equations

• One or more equations did not get rendered due to their size.

theorem Anderson4D.heppChainWeight_eq_indexed {t : PlaneTree} {m : ℕ} (z : HeppLeaf t → Fin 4 → ℤ) (w : Fin m → HeppLeaf t) : heppChainWeight z w = indexedChainProduct latticeEdgeWeight fun (i : Fin m) => z (w i)

theorem Anderson4D.heppChainWeight_eq_listChainProduct {t : PlaneTree} {m : ℕ} (z : HeppLeaf t → Fin 4 → ℤ) (w : Fin m → HeppLeaf t) : heppChainWeight z w = listChainProduct latticeEdgeWeight (List.ofFn fun (i : Fin m) => z (w i))

@[simp]

theorem Anderson4D.latticeEdgeWeight_self (x : Fin 4 → ℤ) : latticeEdgeWeight x x = 1

theorem Anderson4D.latticePointChainProduct_mergeEqualRuns {α : Type u_1} [DecidableEq α] (z : α → Fin 4 → ℤ) (l : List α) : listChainProduct latticeEdgeWeight (mergeEqualRuns (List.map z l)) = listChainProduct latticeEdgeWeight (List.map z l)

Exact weight invariance under merging all adjacent equal leaves.

theorem Anderson4D.latticeChainProduct_mergeLetterRuns {α : Type u_1} [DecidableEq α] (z : α → Fin 4 → ℤ) (l : List α) : listChainProduct latticeEdgeWeight (List.map z (mergeEqualRuns l)) = listChainProduct latticeEdgeWeight (List.map z l)

Paper (5.35): merge equal leaf letters first, then evaluate their lattice locations. The inverse-square chain weight is unchanged.