Exhaustive endpoint operations for string words

Reading a word from left to right, either every letter is positive or there is a last negative letter followed by a positive arm. At a peak, the latter factorization is exactly a maximal cohook which can be deleted. Away from a peak, admissibility extends a valid positive boundary arrow to a maximal hook. Reversal gives the corresponding classification at the left endpoint.

def MagnitudeConjecture.BoundQuiver.StringWord.Word.IsPurePositive {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (hR : IsAdmissible R) (C : Word R) : Prop

A word all of whose letters are positive, packaged as an extension of the trivial word at its source.

def MagnitudeConjecture.BoundQuiver.StringWord.Word.IsPureNegative {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (hR : IsAdmissible R) (C : Word R) : Prop

A word all of whose letters are negative, expressed by reversing it to a pure positive word.

structure MagnitudeConjecture.BoundQuiver.StringWord.Word.CohookFactorization {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) : Type u

A decomposition at the last negative letter of a word: an arbitrary prefix, one negative letter, and a (possibly empty) positive tail.

• base : Word R
• vertex : Q
• arrow : self.vertex ⟶ self.base.target
• valid : IsString R (Quiver.Path.comp self.base.path (Quiver.Hom.toPath (negativeArrow self.arrow)))
• tail : (append R self.base (negativeArrow self.arrow) ⋯).PositiveExtension C

def MagnitudeConjecture.BoundQuiver.StringWord.Word.CohookFactorization.toCohookDeletion {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C : Word R} (F : C.CohookFactorization) (hpeak : C.StartsOnPeak) : C.CohookDeletion F.base

If the final word is on a peak, its last-negative-letter factorization is a maximal cohook reattachment and hence a cohook deletion.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.rightExtensionFromVertex_nonempty_path {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (hR : IsAdmissible R) {x y : Q} (p : SignedPath x y) (h : IsString R p) : Nonempty ((vertex R hR x).RightExtension (ofStringPath p h))

Every certified path is obtained from the trivial word at its source by an arbitrary right extension.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.rightExtensionFromVertex_nonempty {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (hR : IsAdmissible R) (C : Word R) : Nonempty ((vertex R hR C.source).RightExtension C)

Every word is obtained from the trivial word at its source by an arbitrary right extension.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.RightExtension.isPurePositive_or_cohookFactorization {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (extension : C.RightExtension D) : Nonempty (C.PositiveExtension D) ∨ Nonempty D.CohookFactorization

An arbitrary right extension is either purely positive or its final negative letter determines a negative-letter/positive-tail factorization of the result.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.isPurePositive_or_cohookFactorization {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (hR : IsAdmissible R) (C : Word R) : IsPurePositive hR C ∨ Nonempty C.CohookFactorization

Every word is either purely positive or has a last negative letter followed by a positive tail.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.exists_hook_or_cohookDeletion_or_isPurePositive {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (hR : IsAdmissible R) (C : Word R) : (∃ (D : Word R), Nonempty (C.HookExtension D)) ∨ (∃ (D : Word R), Nonempty (C.CohookDeletion D)) ∨ IsPurePositive hR C

Exhaustive operation at the right endpoint: a word admits a maximal hook, admits a maximal cohook deletion, or is purely positive.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.exists_hook_iff_not_startsOnPeak {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (hR : IsAdmissible R) (C : Word R) : (∃ (D : Word R), Nonempty (C.HookExtension D)) ↔ ¬C.StartsOnPeak

A right hook exists exactly when the word does not start on a peak.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.exists_cohookDeletion_of_startsOnPeak_of_not_isPurePositive {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (hR : IsAdmissible R) (C : Word R) (hpeak : C.StartsOnPeak) (hpure : ¬IsPurePositive hR C) : ∃ (D : Word R), Nonempty (C.CohookDeletion D)

A non-pure-positive word on a right peak has a maximal cohook which can be deleted.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.exists_leftHook_or_leftCohookDeletion_or_isPureNegative {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (hR : IsAdmissible R) (C : Word R) : Nonempty C.LeftHookExtension ∨ (∃ (D : Word R), Nonempty (C.LeftCohookDeletion D)) ∨ IsPureNegative hR C

Exhaustive operation at the left endpoint, obtained by reversal: a word admits a maximal left hook, admits a maximal left cohook deletion, or is purely negative.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.exists_leftHook_iff_not_endsOnPeak {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (hR : IsAdmissible R) (C : Word R) : Nonempty C.LeftHookExtension ↔ ¬C.EndsOnPeak

A left hook exists exactly when the word does not end on a peak.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.exists_leftCohookDeletion_of_endsOnPeak_of_not_isPureNegative {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (hR : IsAdmissible R) (C : Word R) (hpeak : C.EndsOnPeak) (hpure : ¬IsPureNegative hR C) : ∃ (D : Word R), Nonempty (C.LeftCohookDeletion D)

A non-pure-negative word on a left peak has a maximal left cohook which can be deleted.