Mixed-sign strings are not uniserial

A change of orientation in a string word exposes two literal subwords whose coordinate inclusions are incomparable. This is the word-level converse needed to identify a uniserial classified string with one of the pure-sign endpoint words.

def MagnitudeConjecture.BoundQuiver.StringWord.Word.signedArrowSign {Q : Type u} [Quiver Q] {x y : Q} : SignedArrow x y → Bool

The Boolean sign of one letter of the symmetrified quiver.

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.signedArrowSign_positive {Q : Type u} [Quiver Q] [Fintype Q] {x y : Q} (a : x ⟶ y) : signedArrowSign (positiveArrow a) = false

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.signedArrowSign_negative {Q : Type u} [Quiver Q] [Fintype Q] {x y : Q} (a : x ⟶ y) : signedArrowSign (negativeArrow a) = true

structure MagnitudeConjecture.BoundQuiver.StringWord.Word.AdjacentSignChange {Q : Type u} [Quiver Q] {x y : Q} (p : SignedPath x y) : Type u

A literal pair of consecutive letters with different signs.

• leftVertex : Q
• centerVertex : Q
• rightVertex : Q
• leftPath : SignedPath x self.leftVertex
• earlier : SignedArrow self.leftVertex self.centerVertex
• later : SignedArrow self.centerVertex self.rightVertex
• rightPath : SignedPath self.rightVertex y
• path_eq : p = ((Quiver.Path.cons self.leftPath self.earlier).cons self.later).comp self.rightPath
• sign_ne : signedArrowSign self.earlier ≠ signedArrowSign self.later

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.adjacentSignChange_of_mem_signedPathSigns {Q : Type u} [Quiver Q] [Fintype Q] {x y : Q} (p : SignedPath x y) (hpositive : false ∈ signedPathSigns p) (hnegative : true ∈ signedPathSigns p) : Nonempty (AdjacentSignChange p)

A signed path containing both signs has two consecutive letters with different signs.

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.signedPathSigns_length {Q : Type u} [Quiver Q] [Fintype Q] {x y : Quiver.Symmetrify Q} (p : Quiver.Path x y) : (signedPathSigns p).length = p.length

The sign list has one entry for every path letter.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.isPurePositive_iff_signedPathSigns_eq {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} [Fintype Q] (hR : IsAdmissible R) (C : Word R) : IsPurePositive hR C ↔ signedPathSigns C.path = List.replicate (length R C) false

The sign-list description of a pure-positive word is an equivalence.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.isPureNegative_iff_signedPathSigns_eq {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} [Fintype Q] (hR : IsAdmissible R) (C : Word R) : IsPureNegative hR C ↔ signedPathSigns C.path = List.replicate (length R C) true

The sign-list description of a pure-negative word is an equivalence.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.NegativeBoundaryExtension.finiteModuleInclusion {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} [Fintype Q] {L C : Word R} (left : L.NegativeBoundaryExtension C) (hmono : IsMonomial R) : L.finiteRightModule hmono ⟶ C.finiteRightModule hmono

A negative-boundary prefix inclusion, bundled in the finite-dimensional module category.

instance MagnitudeConjecture.BoundQuiver.StringWord.Word.NegativeBoundaryExtension.finiteModuleInclusion_mono {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} [Fintype Q] {L C : Word R} (left : L.NegativeBoundaryExtension C) (hmono : IsMonomial R) : CategoryTheory.Mono (left.finiteModuleInclusion hmono)

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.LeftNegativeBoundaryExtension.finiteModuleInclusion {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} [Fintype Q] {S : Word R} (right : S.LeftNegativeBoundaryExtension) (hmono : IsMonomial R) : S.finiteRightModule hmono ⟶ right.result.finiteRightModule hmono

A negative left-boundary suffix inclusion, bundled in the finite- dimensional module category.

instance MagnitudeConjecture.BoundQuiver.StringWord.Word.LeftNegativeBoundaryExtension.finiteModuleInclusion_mono {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} [Fintype Q] {S : Word R} (right : S.LeftNegativeBoundaryExtension) (hmono : IsMonomial R) : CategoryTheory.Mono (right.finiteModuleInclusion hmono)

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.not_isUniserialObject_of_separated_negativeBoundaries {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} [Fintype Q] {L S : Word R} (right : S.LeftNegativeBoundaryExtension) (left : L.NegativeBoundaryExtension right.result) (hmono : IsMonomial R) (hstart : 0 < right.steps) (hend : length R L < right.steps + length R S) : ¬IsUniserialObject (right.result.finiteRightModule hmono)

A prefix and suffix entering a word through negative boundaries give incomparable subobjects when each contains a position absent from the other. The numerical hypotheses state precisely that the left source occurs before the suffix starts and that the right target occurs after the prefix ends.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.not_isUniserialObject_of_mixed_signedPathSigns {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} [Fintype Q] (C : Word R) (hmono : IsMonomial R) (hpositive : false ∈ signedPathSigns C.path) (hnegative : true ∈ signedPathSigns C.path) : ¬IsUniserialObject (C.finiteRightModule hmono)

A literal finite string module whose word contains both signs is not uniserial.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.isPurePositive_or_isPureNegative_of_isUniserialObject {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} [Fintype Q] (hR : IsAdmissible R) (C : Word R) (hmono : IsMonomial R) (hC : IsUniserialObject (C.finiteRightModule hmono)) : IsPurePositive hR C ∨ IsPureNegative hR C

A uniserial literal finite string has only one sign: it is a pure positive or a pure negative endpoint word.