Common corners for two-ended string hooks

This file constructs the signed path obtained by applying a maximal hook at both endpoints of a nontrivial string. The signs at the two seams block relations from crossing the whole word, while the nonempty original word prevents a new inverse pair from spanning both seams.

def MagnitudeConjecture.BoundQuiver.StringWord.Word.leftHookBasePath {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C : Word R} (left : C.LeftHookExtension) : SignedPath left.reverseResult.target C.target

The explicit path of a left hook, ending at the old right endpoint.

def MagnitudeConjecture.BoundQuiver.StringWord.Word.twoHookPath {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C rightResult : Word R} (right : C.HookExtension rightResult) (left : C.LeftHookExtension) : SignedPath left.reverseResult.target rightResult.target

The explicit signed path obtained by adjoining the left-hook suffix in reverse order and the right-hook suffix in forward order.

def MagnitudeConjecture.BoundQuiver.StringWord.Word.twoHookReversePath {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C rightResult : Word R} (right : C.HookExtension rightResult) (left : C.LeftHookExtension) : SignedPath rightResult.target left.reverseResult.target

The same two-ended path written directly in the reverse orientation.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.leftHookPath_isString {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C : Word R} (left : C.LeftHookExtension) : IsString R ((Quiver.Path.reverse left.hook.tail.toRightExtension.suffixPath).comp ((Quiver.Hom.toPath (negativeArrow left.hook.arrow)).comp C.path))

The left one-ended hook certifies the left part of the explicit two-hook path.

def MagnitudeConjecture.BoundQuiver.StringWord.Word.leftHookBaseWord {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C : Word R} (left : C.LeftHookExtension) : Word R

Bundle the explicit left-hook path as a word.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.leftHookBaseWord_eq_result {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C : Word R} (left : C.LeftHookExtension) : leftHookBaseWord left = left.result

The explicit left-hook word is the transported reversal-based result.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.rightHookPath_isString {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C rightResult : Word R} (right : C.HookExtension rightResult) : IsString R (Quiver.Path.comp C.path ((Quiver.Hom.toPath (positiveArrow right.arrow)).comp right.tail.toRightExtension.suffixPath))

The right one-ended hook certifies the right part of the explicit two-hook path.

def MagnitudeConjecture.BoundQuiver.StringWord.Word.rightHookReverseBasePath {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C rightResult : Word R} (right : C.HookExtension rightResult) : SignedPath rightResult.target C.source

The reversed explicit right-hook path, ending at the old left endpoint.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.rightHookReverseBasePath_isString {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C rightResult : Word R} (right : C.HookExtension rightResult) : IsString R (rightHookReverseBasePath right)

The right hook certifies its explicit reversed base path.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.rightHookReverseBasePath_eq {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C rightResult : Word R} (right : C.HookExtension rightResult) : rightHookReverseBasePath right = (Quiver.Path.reverse right.tail.toRightExtension.suffixPath).comp ((Quiver.Hom.toPath (negativeArrow right.arrow)).comp (Quiver.Path.reverse C.path))

Expanded form of the reversed right-hook path.

def MagnitudeConjecture.BoundQuiver.StringWord.Word.rightHookReverseBaseWord {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C rightResult : Word R} (right : C.HookExtension rightResult) : Word R

Bundle the reversed explicit right-hook path as a word.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.rightHookReverseBaseWord_eq_reverseResult {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C rightResult : Word R} (right : C.HookExtension rightResult) : rightHookReverseBaseWord right = reverse R rightResult

The explicit reversed right-hook word is the reversal of the hook result.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.twoHookReversePath_isString {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C rightResult : Word R} (right : C.HookExtension rightResult) (left : C.LeftHookExtension) (hC : 0 < length R C) : IsString R (twoHookReversePath right left)

The directly written reverse two-hook path is a string whenever the original word is nonempty.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.twoHookPath_isString {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C rightResult : Word R} (right : C.HookExtension rightResult) (left : C.LeftHookExtension) (hC : 0 < length R C) : IsString R (twoHookPath right left)

Hooks at both ends of a nontrivial string produce a valid common-corner path.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.twoHookPath_isString_of_leftHookResult_extension {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C rightResult : Word R} (right : C.HookExtension rightResult) (left : C.LeftHookExtension) (hext : IsString R (Quiver.Path.comp (leftHookBasePath left) (Quiver.Hom.toPath (positiveArrow right.arrow)))) : IsString R (twoHookPath right left)

If the right-hook boundary already extends the full left-hook result, the two hook arms glue through the nonempty overlap consisting of the base word and that boundary letter.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.exists_hook_twoHookPath_isString_of_leftHookResult_not_startsOnPeak {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (hR : IsAdmissible R) {C : Word R} (left : C.LeftHookExtension) (hnotPeak : ¬left.result.StartsOnPeak) : ∃ (rightResult : Word R) (right : C.HookExtension rightResult), IsString R (twoHookPath right left)

If a left-hook result is not a right peak, one of its positive boundary extensions induces a right hook on the original word and hence a valid two-hook corner.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.twoHookPath_isString_of_length_zero {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C rightResult : Word R} (right : C.HookExtension rightResult) (left : C.LeftHookExtension) (hC : length R C = 0) (hboundary : ¬positiveArrow right.arrow ≍ Quiver.reverse (negativeArrow left.hook.arrow)) : IsString R (twoHookPath right left)

At a length-zero word, two hooks still glue when their adjacent signed boundary letters do not cancel.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.twoHookReversePath_reverse {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C rightResult : Word R} (right : C.HookExtension rightResult) (left : C.LeftHookExtension) : Quiver.Path.reverse (twoHookReversePath right left) = twoHookPath right left

Reversing the directly written reverse path recovers the forward two-hook path.

structure MagnitudeConjecture.BoundQuiver.StringWord.Word.TwoHookRightCorner {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C rightResult : Word R} (right : C.HookExtension rightResult) (left : C.LeftHookExtension) : Type u

The common word together with its right positive-boundary extension from the left-hook result.

• corner : Word R
• extension : left.result.PositiveBoundaryExtension self.corner
• steps_eq : self.extension.toRightExtension.steps = right.steps
• source_eq : self.corner.source = left.reverseResult.target
• target_eq : self.corner.target = rightResult.target
• path_cast_eq : Quiver.Path.cast ⋯ ⋯ self.corner.path = twoHookPath right left

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.twoHookRightCorner {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C rightResult : Word R} (right : C.HookExtension rightResult) (left : C.LeftHookExtension) (hpath : IsString R (twoHookPath right left)) : TwoHookRightCorner right left

Replay the right-hook tail after the explicit left-hook word.

def MagnitudeConjecture.BoundQuiver.StringWord.Word.twoHookCornerWord {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C rightResult : Word R} (right : C.HookExtension rightResult) (left : C.LeftHookExtension) (hpath : IsString R (twoHookPath right left)) : Word R

The canonical bundled common-corner word.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.TwoHookRightCorner.corner_eq_twoHookCornerWord {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C rightResult : Word R} (right : C.HookExtension rightResult) (left : C.LeftHookExtension) (hpath : IsString R (twoHookPath right left)) (corner : TwoHookRightCorner right left) : corner.corner = twoHookCornerWord right left hpath

The replayed right corner is the canonical bundled two-hook word.

structure MagnitudeConjecture.BoundQuiver.StringWord.Word.TwoHookLeftCorner {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C rightResult : Word R} (right : C.HookExtension rightResult) (left : C.LeftHookExtension) : Type u

The common reversed word together with the positive-boundary extension whose reversal is a left extension of the right-hook result.

• reverseCorner : Word R
• extension : rightResult.LeftPositiveBoundaryExtension
• reverseResult_eq : self.extension.reverseResult = self.reverseCorner
• steps_eq : self.extension.steps = left.steps
• source_eq : self.reverseCorner.source = rightResult.target
• target_eq : self.reverseCorner.target = left.reverseResult.target
• path_cast_eq : Quiver.Path.cast ⋯ ⋯ self.reverseCorner.path = twoHookReversePath right left

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.twoHookLeftCorner {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C rightResult : Word R} (right : C.HookExtension rightResult) (left : C.LeftHookExtension) (hpath : IsString R (twoHookPath right left)) : TwoHookLeftCorner right left

Replay the left-hook tail after the reversed explicit right-hook word.

def MagnitudeConjecture.BoundQuiver.StringWord.Word.twoHookReverseCornerWord {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C rightResult : Word R} (right : C.HookExtension rightResult) (left : C.LeftHookExtension) (hpath : IsString R (twoHookPath right left)) : Word R

The canonical bundled common corner in reverse orientation.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.TwoHookLeftCorner.reverseCorner_eq_twoHookReverseCornerWord {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C rightResult : Word R} (right : C.HookExtension rightResult) (left : C.LeftHookExtension) (hpath : IsString R (twoHookPath right left)) (corner : TwoHookLeftCorner right left) : corner.reverseCorner = twoHookReverseCornerWord right left hpath

The replayed left corner is the canonical reverse-oriented two-hook word.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.twoHookReverseCornerWord_reverse {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C rightResult : Word R} (right : C.HookExtension rightResult) (left : C.LeftHookExtension) (hpath : IsString R (twoHookPath right left)) : reverse R (twoHookReverseCornerWord right left hpath) = twoHookCornerWord right left hpath

The two canonical orientations of the common corner are reversals of one another.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.TwoHookLeftCorner.result_eq_twoHookCornerWord {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C rightResult : Word R} (right : C.HookExtension rightResult) (left : C.LeftHookExtension) (hpath : IsString R (twoHookPath right left)) (corner : TwoHookLeftCorner right left) : corner.extension.result = twoHookCornerWord right left hpath

The left replay has the same forward-oriented result as the canonical two-hook corner.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.twoHookSquare {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C rightResult : Word R} (right : C.HookExtension rightResult) (left : C.LeftHookExtension) (hpath : IsString R (twoHookPath right left)) : C.PositiveBoundarySquare

Hooks at both ends of a nonempty word form a coherent positive-boundary square with the canonical two-hook word as common corner.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.twoHookSquare_shortComplex_exact {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C rightResult : Word R} (right : C.HookExtension rightResult) (left : C.LeftHookExtension) (hpath : IsString R (twoHookPath right left)) (hmono : IsMonomial R) : ((twoHookSquare right left hpath).shortComplex hmono).Exact

The canonical two-hook square gives an exact short complex of string modules.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.twoHookSquareOfPositiveLength {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C rightResult : Word R} (right : C.HookExtension rightResult) (left : C.LeftHookExtension) (hC : 0 < length R C) : C.PositiveBoundarySquare

The canonical two-hook square for a positive-length base word.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.twoHookSquareOfLengthZero {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C rightResult : Word R} (right : C.HookExtension rightResult) (left : C.LeftHookExtension) (hC : length R C = 0) (hboundary : ¬positiveArrow right.arrow ≍ Quiver.reverse (negativeArrow left.hook.arrow)) : C.PositiveBoundarySquare

The canonical two-hook square at a length-zero word whose two signed boundary letters do not cancel.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.twoHookSquareOfPositiveLength_shortComplex_exact {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C rightResult : Word R} (right : C.HookExtension rightResult) (left : C.LeftHookExtension) (hC : 0 < length R C) (hmono : IsMonomial R) : ((twoHookSquareOfPositiveLength right left hC).shortComplex hmono).Exact

The positive-length two-hook square gives an exact canonical short complex.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.twoHookSquareOfLengthZero_shortComplex_exact {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C rightResult : Word R} (right : C.HookExtension rightResult) (left : C.LeftHookExtension) (hC : length R C = 0) (hboundary : ¬positiveArrow right.arrow ≍ Quiver.reverse (negativeArrow left.hook.arrow)) (hmono : IsMonomial R) : ((twoHookSquareOfLengthZero right left hC hboundary).shortComplex hmono).Exact

The noncancelling length-zero two-hook square gives an exact canonical short complex.