Pure-sign exceptional string endpoints

The exhaustive endpoint classification leaves a pure-positive alternative on the right and a pure-negative alternative on the left. This file makes those alternatives literal at the level of signed-path signs, proves that they overlap only for a vertex word, and packages the endpoint alternatives so that a pure case is reached only at a peak.

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.signedPathSigns_reverse {Q : Type u} [Quiver Q] {x y : Quiver.Symmetrify Q} (p : Quiver.Path x y) : signedPathSigns p.reverse = List.map (fun (x : Bool) => !x) (signedPathSigns p).reverse

Reversing a signed path reverses the sign list and complements every sign. Recall that signedPathSigns lists letters from the end backwards.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.PositiveExtension.signedPathSigns_eq {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (arm : C.PositiveExtension D) : signedPathSigns D.path = List.replicate arm.steps false ++ signedPathSigns C.path

A positive arm prepends one false sign for every appended letter.

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

A pure-positive word has only positive signed letters.

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

A pure-negative word has only negative signed letters.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.isPurePositive_of_length_eq_zero {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (hR : IsAdmissible R) (C : Word R) (hlength : length R C = 0) : IsPurePositive hR C

Every length-zero word is the trivial word at its source and hence is purely positive.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.isPurePositive_and_isPureNegative_iff_length_eq_zero {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (hR : IsAdmissible R) (C : Word R) : IsPurePositive hR C ∧ IsPureNegative hR C ↔ length R C = 0

A word is simultaneously pure-positive and pure-negative exactly when it is a vertex word.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.IsPurePositive.not_isPureNegative_of_length_pos {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (hR : IsAdmissible R) {C : Word R} (hpositive : IsPurePositive hR C) (hlength : 0 < length R C) : ¬IsPureNegative hR C

A nontrivial pure-positive word cannot also be pure-negative.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.exists_hook_or_cohookDeletion_or_isPurePositive_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)) ∨ (∃ (D : Word R), Nonempty (C.CohookDeletion D)) ∨ IsPurePositive hR C ∧ C.StartsOnPeak

Endpoint classification with the alternatives prioritized: the pure right-end exception is returned only together with maximality at that end.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.exists_leftHook_or_leftCohookDeletion_or_isPureNegative_endsOnPeak {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 ∧ C.EndsOnPeak

The reversed prioritized endpoint classification: the pure left-end exception is returned only together with maximality at that end.