Raw-count fixed-endpoint fibres for one open edge

The old open word may have singleton endpoint labels, so it need not belong to the valid-word fibre of any Multiplicities record. The correct source fibre is instead determined by:

• the literal occurrence counts of a surjective reference word;
• its two selected endpoint labels; and
• equality of labels along every unmarked pairing edge.

Dummy augmentation makes all counts even and at least two. The whole raw source fibre then injects into the single augmented valid-word fibre defined by the reference word, where Proposition 5.7 applies.

def Anderson4D.openEdgeRawCountFixedEndpointFiber {t : PlaneTree} {m : ℕ} (κ : PartialPairing (Fin m)) (a b : Fin m) (reference : Fin m → HeppLeaf t) : Finset (Fin m → HeppLeaf t)

The correct old-word fibre: raw counts, fixed selected endpoint labels, and the unmarked pairing constraint.

Equations

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

@[simp]

theorem Anderson4D.mem_openEdgeRawCountFixedEndpointFiber {t : PlaneTree} {m : ℕ} {κ : PartialPairing (Fin m)} {a b : Fin m} {reference w : Fin m → HeppLeaf t} : w ∈ openEdgeRawCountFixedEndpointFiber κ a b reference ↔ (∀ (l : HeppLeaf t), wordFiberCount w l = wordFiberCount reference l) ∧ w a = reference a ∧ w b = reference b ∧ ∀ (i : Fin m), i ≠ a → i ≠ b → w i = w (κ i)

theorem Anderson4D.reference_mem_openEdgeRawCountFixedEndpointFiber {t : PlaneTree} {m : ℕ} (κ : PartialPairing (Fin m)) (a b : Fin m) (reference : Fin m → HeppLeaf t) (hrespect : ∀ (i : Fin m), i ≠ a → i ≠ b → reference i = reference (κ i)) : reference ∈ openEdgeRawCountFixedEndpointFiber κ a b reference

The reference word belongs to its own raw-count fibre whenever it obeys the unmarked pairing constraint.

theorem Anderson4D.surjective_of_wordFiberCount_eq_surjective {α : Type u_1} [Fintype α] [DecidableEq α] {m : ℕ} (reference w : Fin m → α) (href : Function.Surjective reference) (hcount : ∀ (x : α), wordFiberCount w x = wordFiberCount reference x) : Function.Surjective w

A word with the raw occurrence profile of a surjective reference is itself surjective.

theorem Anderson4D.surjective_of_mem_openEdgeRawCountFixedEndpointFiber {t : PlaneTree} {m : ℕ} {κ : PartialPairing (Fin m)} {a b : Fin m} {reference w : Fin m → HeppLeaf t} (href : Function.Surjective reference) (hw : w ∈ openEdgeRawCountFixedEndpointFiber κ a b reference) : Function.Surjective w

Every member of a raw-count fibre over a surjective reference is surjective.

theorem Anderson4D.wordFiberCount_openEdgeAugmentedWord_eq_of_rawProfile_endpoints {α : Type u_1} [DecidableEq α] {m : ℕ} (reference w : Fin m → α) (a b : Fin m) (hcount : ∀ (x : α), wordFiberCount w x = wordFiberCount reference x) (ha : w a = reference a) (hb : w b = reference b) (x : α) : wordFiberCount (openEdgeAugmentedWord w a b) x = wordFiberCount (openEdgeAugmentedWord reference a b) x

Equal old raw counts and equal selected endpoint labels give equal augmented raw counts.

theorem Anderson4D.openEdgeArbitraryMultiplicities_eq_of_rawProfile_endpoints {t : PlaneTree} {m : ℕ} (κ : PartialPairing (Fin m)) (a b : Fin m) (hκab : κ a = b) (hab : a ≠ b) (hfull : κ.IsFull) (reference w : Fin m → HeppLeaf t) (href : Function.Surjective reference) (hwSurj : Function.Surjective w) (hrefRespect : ∀ (i : Fin m), i ≠ a → i ≠ b → reference i = reference (κ i)) (hwRespect : ∀ (i : Fin m), i ≠ a → i ≠ b → w i = w (κ i)) (hcount : ∀ (l : HeppLeaf t), wordFiberCount w l = wordFiberCount reference l) (ha : w a = reference a) (hb : w b = reference b) : openEdgeArbitraryMultiplicities κ a b hκab hab hfull w hwSurj hwRespect = openEdgeArbitraryMultiplicities κ a b hκab hab hfull reference href hrefRespect

All words in one raw-count fixed-endpoint fibre induce literally the same arbitrary augmented Multiplicities profile.

theorem Anderson4D.openEdgeAugmentedWord_injective_raw {α : Type u_1} {m : ℕ} (a b : Fin m) : Function.Injective fun (w : Fin m → α) => openEdgeAugmentedWord w a b

Dummy augmentation is injective because the old word is retained on the initial segment.

theorem Anderson4D.rawWordSum_le_paperSum_of_nonneg {α : Type u_1} [Fintype α] [DecidableEq α] {q : ℕ} (mult : α → ℕ) (F : (Fin q → α) → ℝ) (hF : ∀ (u : Fin q → α), 0 ≤ F u) : wordSum mult F ≤ paperSum mult F

The factorial-prefactored paper sum dominates its nonnegative valid-word sum.

theorem Anderson4D.rawCountFixedEndpointFiberSum_le_boxPenalty_mul_permSumRHS {C : ℝ} (hperm : PermSumEstimate C) {t : PlaneTree} {m M : ℕ} (reference : Fin m → HeppLeaf t) (href : Function.Surjective reference) (κ : PartialPairing (Fin m)) (a b : Fin m) (hm : 0 < m) (hκab : κ a = b) (hab : a < b) (hfull : κ.IsFull) (hprimitive : IsPrimitive κ) (hrefRespect : ∀ (i : Fin m), i ≠ a → i ≠ b → reference i = reference (κ 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 ∧ ∑ w ∈ openEdgeRawCountFixedEndpointFiber κ a b reference, heppChainWeight z w ≤ (1 + (2 * ↑M) ^ 2) ^ 2 * permSumRHS C n t Nm (openEdgeArbitraryMultiplicities κ a b hκab ⋯ hfull reference href hrefRespect)

The complete raw-count fixed-endpoint fibre is bounded by one augmented Proposition 5.7 right-hand side. The explicit square box penalty is left for the selected high covariance coefficient to pay.