Paired-vector form of paper Lemma 5.5

The general realizing-tree construction only needs every value to occur at least twice. Paper Lemma 5.5 starts from a fixed bijection κ : A ≃ Aᶜ; this stronger input forces the leaf multiplicities to be even. This module packages that paper-facing corollary, including the uniform branch-scale bound from ExistenceBounds.

theorem Anderson4D.exists_realizing_tree_of_across_pairing (M m : ℕ) (hm : 1 ≤ m) (A : Finset (Fin m)) (y : Fin m → Fin 4 → ℤ) (hy : y ∈ rdec_boundedTuples M m) (κ : AcrossPairing A) (hκ : RespectsWord A y κ) : ∃ (t : PlaneTree) (_ : t.isValid = true) (Nm : t.HeppMarking) (mu : t.Multiplicities), y ∈ realizedTuples t Nm mu M m ∧ t.leafCount ≤ m ∧ (∀ v ∈ t.BranchNodes, ↑(scaleN Nm v) ≤ 4 * ↑M) ∧ ∀ l ∈ t.Leaves, Even (mu.m l)

Paper Lemma 5.5, paired-vector form. A bounded word admitting a pairing across A/Aᶜ is realized by a valid marked Hepp tree. Every branch scale is at most 4M, and every leaf multiplicity is even.