Augmented multiplicities from an arbitrary open-edge word

An open-edge word need not itself have leaf multiplicities at least two: when the endpoint labels differ, either endpoint label may occur only once. The two dummy copies supply exactly the missing multiplicities. This file constructs the paper-facing Multiplicities record directly from the augmented word, without assuming an old Multiplicities profile.

Surjectivity of the old word makes every augmented leaf fibre positive. The augmented full word-respecting pairing makes every fibre even. Hence every augmented multiplicity is at least two.

Positivity and parity of the actual augmented counts

theorem Anderson4D.one_le_wordFiberCount_of_surjective {α : Type u_1} [DecidableEq α] {m : ℕ} {w : Fin m → α} (hsurj : Function.Surjective w) (x : α) : 1 ≤ wordFiberCount w x

Every letter occurs at least once in a surjective finite word.

theorem Anderson4D.one_le_wordFiberCount_openEdgeAugmentedWord {α : Type u_1} [DecidableEq α] {m : ℕ} (w : Fin m → α) (hsurj : Function.Surjective w) (a b : Fin m) (x : α) : 1 ≤ wordFiberCount (openEdgeAugmentedWord w a b) x

Every augmented letter fibre is positive when the old word is surjective.

theorem Anderson4D.two_le_wordFiberCount_openEdgeAugmentedWord {α : Type u_1} [DecidableEq α] {m : ℕ} (κ : PartialPairing (Fin m)) (a b : Fin m) (hκab : κ a = b) (hab : a ≠ b) (hfull : κ.IsFull) (w : Fin m → α) (hsurj : Function.Surjective w) (hrespect : ∀ (i : Fin m), i ≠ a → i ≠ b → w i = w (κ i)) (x : α) : 2 ≤ wordFiberCount (openEdgeAugmentedWord w a b) x

Positivity plus the full word-respecting augmented pairing upgrades every actual augmented leaf count to at least two.

Direct construction of the augmented Multiplicities

def Anderson4D.wordFiberMultiplicities {t : PlaneTree} {q : ℕ} (u : Fin q → HeppLeaf t) (htwo : ∀ (l : HeppLeaf t), 2 ≤ wordFiberCount u l) : t.Multiplicities

A word whose every leaf count is at least two defines the canonical paper-facing multiplicity record from its actual fibre counts.

Equations

• Anderson4D.wordFiberMultiplicities u htwo = { m := fun (v : t.VPos) => if hv : v ∈ t.Leaves then Anderson4D.wordFiberCount u ⟨v, hv⟩ else 0, two_le := ⋯ }

@[simp]

theorem Anderson4D.leafMultiplicity_wordFiberMultiplicities {t : PlaneTree} {q : ℕ} (u : Fin q → HeppLeaf t) (htwo : ∀ (l : HeppLeaf t), 2 ≤ wordFiberCount u l) (l : HeppLeaf t) : leafMultiplicity (wordFiberMultiplicities u htwo) l = wordFiberCount u l

def Anderson4D.openEdgeArbitraryMultiplicities {t : PlaneTree} {m : ℕ} (κ : PartialPairing (Fin m)) (a b : Fin m) (hκab : κ a = b) (hab : a ≠ b) (hfull : κ.IsFull) (w : Fin m → HeppLeaf t) (hsurj : Function.Surjective w) (hrespect : ∀ (i : Fin m), i ≠ a → i ≠ b → w i = w (κ i)) : t.Multiplicities

The augmented multiplicity record constructed without any old profile.

Equations

• Anderson4D.openEdgeArbitraryMultiplicities κ a b hκab hab hfull w hsurj hrespect = Anderson4D.wordFiberMultiplicities (Anderson4D.openEdgeAugmentedWord w a b) ⋯

@[simp]

theorem Anderson4D.leafMultiplicity_openEdgeArbitraryMultiplicities {t : PlaneTree} {m : ℕ} (κ : PartialPairing (Fin m)) (a b : Fin m) (hκab : κ a = b) (hab : a ≠ b) (hfull : κ.IsFull) (w : Fin m → HeppLeaf t) (hsurj : Function.Surjective w) (hrespect : ∀ (i : Fin m), i ≠ a → i ≠ b → w i = w (κ i)) (l : HeppLeaf t) : leafMultiplicity (openEdgeArbitraryMultiplicities κ a b hκab hab hfull w hsurj hrespect) l = wordFiberCount (openEdgeAugmentedWord w a b) l

theorem Anderson4D.totalMultiplicity_openEdgeArbitraryMultiplicities {t : PlaneTree} {m : ℕ} (κ : PartialPairing (Fin m)) (a b : Fin m) (hκab : κ a = b) (hab : a ≠ b) (hfull : κ.IsFull) (w : Fin m → HeppLeaf t) (hsurj : Function.Surjective w) (hrespect : ∀ (i : Fin m), i ≠ a → i ≠ b → w i = w (κ i)) : totalMultiplicity (openEdgeArbitraryMultiplicities κ a b hκab hab hfull w hsurj hrespect) = m + 2

The directly constructed augmented profile has total length m + 2.

theorem Anderson4D.even_leafMultiplicity_openEdgeArbitraryMultiplicities {t : PlaneTree} {m : ℕ} (κ : PartialPairing (Fin m)) (a b : Fin m) (hκab : κ a = b) (hab : a ≠ b) (hfull : κ.IsFull) (w : Fin m → HeppLeaf t) (hsurj : Function.Surjective w) (hrespect : ∀ (i : Fin m), i ≠ a → i ≠ b → w i = w (κ i)) (l : HeppLeaf t) : Even (leafMultiplicity (openEdgeArbitraryMultiplicities κ a b hκab hab hfull w hsurj hrespect) l)

Every leaf multiplicity of the directly constructed profile is even.

theorem Anderson4D.openEdgeAugmentedWord_mem_arbitraryValidWords {t : PlaneTree} {m : ℕ} (κ : PartialPairing (Fin m)) (a b : Fin m) (hκab : κ a = b) (hab : a ≠ b) (hfull : κ.IsFull) (w : Fin m → HeppLeaf t) (hsurj : Function.Surjective w) (hrespect : ∀ (i : Fin m), i ≠ a → i ≠ b → w i = w (κ i)) : openEdgeAugmentedWord w a b ∈ validWords (leafMultiplicity (openEdgeArbitraryMultiplicities κ a b hκab hab hfull w hsurj hrespect))

The augmented word realizes exactly the directly constructed profile.

theorem Anderson4D.exists_openEdgeArbitraryPermSumMultiplicityData {t : PlaneTree} {m : ℕ} (κ : PartialPairing (Fin m)) (a b : Fin m) (hκab : κ a = b) (hab : a ≠ b) (hfull : κ.IsFull) (w : Fin m → HeppLeaf t) (hsurj : Function.Surjective w) (hrespect : ∀ (i : Fin m), i ≠ a → i ≠ b → w i = w (κ i)) : ∃ (n : ℕ), 2 ≤ n ∧ totalMultiplicity (openEdgeArbitraryMultiplicities κ a b hκab hab hfull w hsurj hrespect) = 2 * n ∧ (∀ (l : HeppLeaf t), Even (leafMultiplicity (openEdgeArbitraryMultiplicities κ a b hκab hab hfull w hsurj hrespect) l)) ∧ openEdgeAugmentedWord w a b ∈ validWords (leafMultiplicity (openEdgeArbitraryMultiplicities κ a b hκab hab hfull w hsurj hrespect))

Exact order, total, parity, and valid-word certificate needed to apply PermSumEstimate, with no old multiplicity hypothesis.

Direct fixed-word use of Proposition 5.7

theorem Anderson4D.openEdgeArbitraryAugmented_chain_le_permSumRHS {C : ℝ} (hperm : PermSumEstimate C) {t : PlaneTree} {m M : ℕ} (κ : PartialPairing (Fin m)) (a b : Fin m) (hκab : κ a = b) (hab : a < b) (hfull : κ.IsFull) (hprimitive : IsPrimitive κ) (w : Fin m → HeppLeaf t) (hsurj : Function.Surjective w) (hrespect : ∀ (i : Fin m), i ≠ a → i ≠ b → w i = w (κ i)) (Nm : t.HeppMarking) (z : HeppLeaf t → Fin 4 → ℤ) (ht : t.isValid = true) (hroot : t.rootV ∈ t.BranchNodes) (hadm : IsAdmissible Nm M z) : ∃ (n : ℕ), 2 ≤ n ∧ heppChainWeight z (openEdgeAugmentedWord w a b) ≤ permSumRHS C n t Nm (openEdgeArbitraryMultiplicities κ a b hκab ⋯ hfull w hsurj hrespect)

A single arbitrary open-edge word, after dummy closure, is controlled by the literal Proposition 5.7 right-hand side for its actual augmented profile.