Nesting nonoverlapping cohook deletions

If maximal cohooks can be deleted from both ends of a string and their total length does not exceed the string length, then the deletions are independent: after deleting the right cohook, the original left cohook can still be deleted. The proof identifies the remaining middle substring and replays the left cohook on it.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.exists_leftCohookDeletion_after_right_of_steps_add_le {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C L D : Word R} (leftDeletion : C.LeftCohookDeletion D) (rightDeletion : C.CohookDeletion L) (hnonoverlap : leftDeletion.steps + rightDeletion.steps ≤ length R C) : ∃ (E : Word R), Nonempty (L.LeftCohookDeletion E)

If cohooks at the two ends occupy no more than the whole source word, deleting the right cohook leaves a word from which the left cohook can still be deleted.

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

The signs of a cohook result consist of its positive tail, its initial negative boundary letter, and the signs of the base word, in the reverse order used by signedPathSigns.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.LeftCohookDeletion.signedPathSigns_eq {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (deletion : C.LeftCohookDeletion D) : signedPathSigns C.path = List.map (fun (x : Bool) => !x) (signedPathSigns (reverse R D).path).reverse ++ false :: List.replicate deletion.cohook.tail.steps true

A left cohook deletion gives the complementary suffix description of the original word's sign list.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.LeftCohookDeletion.signedPathSigns_eq_base {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (deletion : C.LeftCohookDeletion D) : signedPathSigns C.path = signedPathSigns D.path ++ false :: List.replicate deletion.cohook.tail.steps true

In the original orientation, a left cohook deletion displays the signs of the shortened word followed by its negative boundary letter and positive tail.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.overlappingCohookDeletion_rigidity {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C L D : Word R} (leftDeletion : C.LeftCohookDeletion D) (rightDeletion : C.CohookDeletion L) (hoverlap : length R C < leftDeletion.steps + rightDeletion.steps) : rightDeletion.cohook.tail.steps = length R D + 1 ∧ leftDeletion.cohook.tail.steps = length R L + 1 ∧ signedPathSigns C.path = List.replicate rightDeletion.cohook.tail.steps false ++ List.replicate leftDeletion.cohook.tail.steps true

If two endpoint cohook deletions overlap, each positive cohook tail runs one letter past the opposite shortened word, and the source has exactly one negative-to-positive sign change.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.overlappingCohookDeletion_residual_signs {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C L D : Word R} (leftDeletion : C.LeftCohookDeletion D) (rightDeletion : C.CohookDeletion L) (hoverlap : length R C < leftDeletion.steps + rightDeletion.steps) : signedPathSigns L.path = List.replicate (length R L) true ∧ signedPathSigns D.path = List.replicate (length R D) false

In the overlap case, the right-shortened word is entirely negative and the left-shortened word is entirely positive.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.exists_peak_path_decomposition_of_overlappingCohookDeletions {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C L D : Word R} (leftDeletion : C.LeftCohookDeletion D) (rightDeletion : C.CohookDeletion L) (hoverlap : length R C < leftDeletion.steps + rightDeletion.steps) : ∃ (u : Q) (leftArm : Quiver.Path u C.source) (rightArm : Quiver.Path u C.target), C.path = (Quiver.Path.reverse (positivePath leftArm)).comp (positivePath rightArm) ∧ leftArm.length = leftDeletion.cohook.tail.steps ∧ rightArm.length = rightDeletion.cohook.tail.steps

The rigid overlap word is a literal two-arm wedge. Both arms are ordinary surviving paths starting at one common displayed vertex; traversing the left arm backwards and then the right arm forwards recovers the source word. Their lengths are exactly the two positive cohook tails.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.cohookDeletion_steps_add_eq_length_add_two_of_overlap {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C L D : Word R} (leftDeletion : C.LeftCohookDeletion D) (rightDeletion : C.CohookDeletion L) (hoverlap : length R C < leftDeletion.steps + rightDeletion.steps) : leftDeletion.steps + rightDeletion.steps = length R C + 2

Overlapping left and right cohooks share exactly their two boundary letters: their deletion lengths exceed the word length by precisely two.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.cohookDeletion_overlap_iff_steps_add_eq_length_add_two {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C L D : Word R} (leftDeletion : C.LeftCohookDeletion D) (rightDeletion : C.CohookDeletion L) : length R C < leftDeletion.steps + rightDeletion.steps ↔ leftDeletion.steps + rightDeletion.steps = length R C + 2

The strict overlap inequality is equivalent to the exact two-letter overlap formula.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.cohookDeletion_nesting_or_overlap {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C L D : Word R} (leftDeletion : C.LeftCohookDeletion D) (rightDeletion : C.CohookDeletion L) : (∃ (E : Word R), Nonempty (L.LeftCohookDeletion E)) ∨ leftDeletion.steps + rightDeletion.steps = length R C + 2 ∧ signedPathSigns C.path = List.replicate rightDeletion.cohook.tail.steps false ++ List.replicate leftDeletion.cohook.tail.steps true

Two endpoint cohook deletions either nest to give successive deletions, or have the rigid two-letter overlap and one-change sign pattern.