Multiplicity ledger for one opened edge

Closing one covariance edge appends copies of its two endpoint labels. This file records only the resulting finite counting facts:

• every letter count is the old count plus the two endpoint indicators;
• the total count is m + 2;
• a full augmented pairing respecting the augmented word makes every letter count even; and
• these counts package as the Multiplicities and order hypotheses consumed by PermSumEstimate.

There are no geometric or analytic hypotheses in this module.

def Anderson4D.wordFiberCount {α : Type u_1} [DecidableEq α] {m : ℕ} (w : Fin m → α) (x : α) : ℕ

Number of occurrences of x in a finite word.

Equations

• Anderson4D.wordFiberCount w x = {i : Fin m | w i = x}.card

theorem Anderson4D.wordFiberCount_openEdgeAugmentedWord {α : Type u_1} [DecidableEq α] {m : ℕ} (w : Fin m → α) (a b : Fin m) (x : α) : wordFiberCount (openEdgeAugmentedWord w a b) x = (wordFiberCount w x + if w a = x then 1 else 0) + if w b = x then 1 else 0

The occurrence count of a letter after closing one open edge is the old count plus one copy of each endpoint label.

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

Every old word fibre injects into the corresponding augmented fibre.

theorem Anderson4D.wordFiberFactorialLedger_le_openEdgeAugmented {α : Type u_1} [Fintype α] [DecidableEq α] {m : ℕ} (w : Fin m → α) (a b : Fin m) : ∏ x : α, ↑(wordFiberCount w x).factorial ≤ ∏ x : α, ↑(wordFiberCount (openEdgeAugmentedWord w a b) x).factorial

Consequently, the full factorial ledger of the open word is dominated by the factorial ledger after dummy closure.

theorem Anderson4D.sum_wordFiberCount {α : Type u_1} [Fintype α] [DecidableEq α] {m : ℕ} (w : Fin m → α) : ∑ x : α, wordFiberCount w x = m

The counts of all letters in a word sum to its length.

theorem Anderson4D.sum_wordFiberCount_openEdgeAugmentedWord {α : Type u_1} [Fintype α] [DecidableEq α] {m : ℕ} (w : Fin m → α) (a b : Fin m) : ∑ x : α, wordFiberCount (openEdgeAugmentedWord w a b) x = m + 2

In particular, the augmented word has total length m + 2.

def Anderson4D.PartialPairing.restrictWordFiber {α : Type u_1} [DecidableEq α] {m : ℕ} (κ : PartialPairing (Fin m)) (w : Fin m → α) (hrespect : κ.RespectsWord w) (x : α) : PartialPairing { i : Fin m // w i = x }

Restriction of a word-respecting pairing to one word fibre.

Equations

• κ.restrictWordFiber w hrespect x = { toFun := fun (i : { i : Fin m // w i = x }) => ⟨κ ↑i, ⋯⟩, involutive := ⋯ }

theorem Anderson4D.PartialPairing.restrictWordFiber_isFull {α : Type u_1} [DecidableEq α] {m : ℕ} {κ : PartialPairing (Fin m)} {w : Fin m → α} (hfull : κ.IsFull) (hrespect : κ.RespectsWord w) (x : α) : (κ.restrictWordFiber w hrespect x).IsFull

Fullness is inherited by every word fibre.

theorem Anderson4D.even_wordFiberCount_of_full_respectsWord {α : Type u_1} [DecidableEq α] {m : ℕ} {κ : PartialPairing (Fin m)} {w : Fin m → α} (hfull : κ.IsFull) (hrespect : κ.RespectsWord w) (x : α) : Even (wordFiberCount w x)

Every letter fibre of a full word-respecting pairing has even cardinality.

theorem Anderson4D.even_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 → α) (hrespect : ∀ (i : Fin m), i ≠ a → i ≠ b → w i = w (κ i)) (x : α) : Even (wordFiberCount (openEdgeAugmentedWord w a b) x)

Closing one open edge makes every augmented letter multiplicity even, provided every unmarked old edge respects the old word.

Packaging for PermSumEstimate

def Anderson4D.openEdgeAugmentedLeafMultiplicity {t : PlaneTree} {m : ℕ} (w : Fin m → HeppLeaf t) (a b : Fin m) : HeppLeaf t → ℕ

Leaf multiplicities read directly from the augmented word.

Equations

• Anderson4D.openEdgeAugmentedLeafMultiplicity w a b l = Anderson4D.wordFiberCount (Anderson4D.openEdgeAugmentedWord w a b) l

def Anderson4D.openEdgeAugmentedMultiplicities {t : PlaneTree} {m : ℕ} (mu : t.Multiplicities) (w : Fin m → HeppLeaf t) (hw : w ∈ validWords (leafMultiplicity mu)) (a b : Fin m) : t.Multiplicities

The augmented counts form a Multiplicities bundle whenever the old word realizes an existing multiplicity profile.

Equations

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

@[simp]

theorem Anderson4D.leafMultiplicity_openEdgeAugmentedMultiplicities {t : PlaneTree} {m : ℕ} (mu : t.Multiplicities) (w : Fin m → HeppLeaf t) (hw : w ∈ validWords (leafMultiplicity mu)) (a b : Fin m) (l : HeppLeaf t) : leafMultiplicity (openEdgeAugmentedMultiplicities mu w hw a b) l = openEdgeAugmentedLeafMultiplicity w a b l

theorem Anderson4D.openEdgeAugmentedWord_mem_packagedValidWords {t : PlaneTree} {m : ℕ} (mu : t.Multiplicities) (w : Fin m → HeppLeaf t) (hw : w ∈ validWords (leafMultiplicity mu)) (a b : Fin m) : openEdgeAugmentedWord w a b ∈ validWords (leafMultiplicity (openEdgeAugmentedMultiplicities mu w hw a b))

The augmented word realizes exactly its packaged multiplicities.

theorem Anderson4D.totalMultiplicity_openEdgeAugmentedMultiplicities {t : PlaneTree} {m : ℕ} (mu : t.Multiplicities) (w : Fin m → HeppLeaf t) (hw : w ∈ validWords (leafMultiplicity mu)) (a b : Fin m) : totalMultiplicity (openEdgeAugmentedMultiplicities mu w hw a b) = m + 2

The packaged total multiplicity is exactly the augmented length.

theorem Anderson4D.even_leafMultiplicity_openEdgeAugmentedMultiplicities {t : PlaneTree} {m : ℕ} (mu : t.Multiplicities) (w : Fin m → HeppLeaf t) (hw : w ∈ validWords (leafMultiplicity mu)) (κ : PartialPairing (Fin m)) (a b : Fin m) (hκab : κ a = b) (hab : a ≠ b) (hfull : κ.IsFull) (hrespect : ∀ (i : Fin m), i ≠ a → i ≠ b → w i = w (κ i)) (l : HeppLeaf t) : Even (leafMultiplicity (openEdgeAugmentedMultiplicities mu w hw a b) l)

The packaged leaf multiplicities are all even under the one-open-edge pairing hypotheses.

theorem Anderson4D.exists_openEdgeAugmentedPermSumMultiplicityData {t : PlaneTree} {m : ℕ} (mu : t.Multiplicities) (w : Fin m → HeppLeaf t) (hw : w ∈ validWords (leafMultiplicity mu)) (κ : PartialPairing (Fin m)) (a b : Fin m) (hm : 0 < m) (hκab : κ a = b) (hab : a ≠ b) (hfull : κ.IsFull) (hrespect : ∀ (i : Fin m), i ≠ a → i ≠ b → w i = w (κ i)) : ∃ (n : ℕ), 2 ≤ n ∧ totalMultiplicity (openEdgeAugmentedMultiplicities mu w hw a b) = 2 * n ∧ (∀ (l : HeppLeaf t), Even (leafMultiplicity (openEdgeAugmentedMultiplicities mu w hw a b) l)) ∧ openEdgeAugmentedWord w a b ∈ validWords (leafMultiplicity (openEdgeAugmentedMultiplicities mu w hw a b))

Exact order, total-multiplicity, parity, and valid-word certificate needed to instantiate PermSumEstimate on the augmented word.