Chain-weight ledger for one opened edge

The primitive-pairing augmentation appends copies of the two marked endpoint labels. This introduces exactly two final chain edges. The equality below exposes those factors; later R-324 estimates pay their inverse with the extra ε⁴ available from the strengthened high-frequency symbol bound.

theorem Anderson4D.heppChainWeight_eq_finPred {t : PlaneTree} {m : ℕ} (z : HeppLeaf t → Fin 4 → ℤ) (w : Fin m → HeppLeaf t) : heppChainWeight z w = ∏ i : Fin (m - 1), latticeEdgeWeight (z (w ⟨↑i, ⋯⟩)) (z (w ⟨↑i + 1, ⋯⟩))

Rewrite the project's adjacency-index product as the equivalent product over predecessor indices.

theorem Anderson4D.heppChainWeight_snoc {t : PlaneTree} (k : ℕ) (z : HeppLeaf t → Fin 4 → ℤ) (u : Fin (k + 2) → HeppLeaf t) : heppChainWeight z u = heppChainWeight z (Fin.init u) * latticeEdgeWeight (z (u ⟨k, ⋯⟩)) (z (u ⟨k + 1, ⋯⟩))

Peel the final edge from a nontrivial chain.

theorem Anderson4D.heppChainWeight_openEdgeAugmentedWord {t : PlaneTree} {m : ℕ} (hm : 0 < m) (z : HeppLeaf t → Fin 4 → ℤ) (w : Fin m → HeppLeaf t) (a b : Fin m) : heppChainWeight z (openEdgeAugmentedWord w a b) = heppChainWeight z w * latticeEdgeWeight (z (w ⟨m - 1, ⋯⟩)) (z (w a)) * latticeEdgeWeight (z (w a)) (z (w b))

Appending the two dummy copies introduces exactly the final edges last → a and a → b.

theorem Anderson4D.znorm_sub_le_two_mul_of_box {M : ℕ} {x y : Fin 4 → ℤ} (hx : ∀ (i : Fin 4), |x i| ≤ ↑M) (hy : ∀ (i : Fin 4), |y i| ≤ ↑M) : znorm (x - y) ≤ 2 * ↑M

Two points of the admissible lattice box are at sup distance at most 2M.

theorem Anderson4D.one_le_boxPenalty_mul_latticeEdgeWeight {M : ℕ} {x y : Fin 4 → ℤ} (hx : ∀ (i : Fin 4), |x i| ≤ ↑M) (hy : ∀ (i : Fin 4), |y i| ≤ ↑M) : 1 ≤ (1 + (2 * ↑M) ^ 2) * latticeEdgeWeight x y

One lattice-box penalty reverses one of the two extra appended edge weights.

theorem Anderson4D.heppChainWeight_le_boxPenalty_sq_mul_openEdgeAugmented {t : PlaneTree} {m : ℕ} (hm : 0 < m) {Nm : t.HeppMarking} {M : ℕ} (z : HeppLeaf t → Fin 4 → ℤ) (hadm : IsAdmissible Nm M z) (w : Fin m → HeppLeaf t) (a b : Fin m) : heppChainWeight z w ≤ (1 + (2 * ↑M) ^ 2) ^ 2 * heppChainWeight z (openEdgeAugmentedWord w a b)

The original open-edge chain is controlled by the augmented primitive chain with the explicit square box penalty.