The first arm edge in right hook and cohook factorizations

For a strict-growth factorization of a right hook through a literal string, the outward edge of the selected full-target interval forces the first factor component to continue across the hook's actual first new position. Both orientation-preserving and orientation-reversing overlaps are retained.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.HookExtension.firstComponent_support_inputPosition {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D M : Word R} (hook : C.HookExtension D) (hmono : IsMonomial R) (first : D.BoundaryFreeMorphismCoefficientComponent M) (second : M.BoundaryFreeMorphismCoefficientComponent C) (houtput : second.HasFullOutputSupport) (hne : D.morphismCoefficientAt C hmono hmono (CategoryTheory.CategoryStruct.comp (D.boundaryFreeMorphismCoefficientComponentMap M hmono hmono first) (M.boundaryFreeMorphismCoefficientComponentMap C hmono hmono second)) (↑(hook.moduleMapComponent hmono)).representative ≠ 0) {x : Q} (i : C.PositionAt x) : Relation.EqvGen (D.MorphismCoefficientStep M) (↑first).representative ⟨x, (hook.toPositiveBoundaryExtension.toRightExtension.position i, second.inputPosition ⋯ i)⟩

Pointwise factorization alignment identifies the first component above the position selected by the full-output-support second component.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.HookExtension.exists_firstNewPosition_support_of_component_pair_of_length_lt {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D M : Word R} (hook : C.HookExtension D) (hmono : IsMonomial R) (first : D.BoundaryFreeMorphismCoefficientComponent M) (second : M.BoundaryFreeMorphismCoefficientComponent C) (houtput : second.HasFullOutputSupport) (hne : D.morphismCoefficientAt C hmono hmono (CategoryTheory.CategoryStruct.comp (D.boundaryFreeMorphismCoefficientComponentMap M hmono hmono first) (M.boundaryFreeMorphismCoefficientComponentMap C hmono hmono second)) (↑(hook.moduleMapComponent hmono)).representative ≠ 0) (hlength : length R C < length R M) : ∃ (j : M.PositionAt hook.vertex), (j.index = (second.inputPosition ⋯ C.targetPosition).index + 1 ∨ j.index + 1 = (second.inputPosition ⋯ C.targetPosition).index) ∧ Relation.EqvGen (D.MorphismCoefficientStep M) (↑first).representative ⟨hook.vertex, (hook.toPositiveBoundaryExtension.firstNewPosition, j)⟩

In the strict-growth branch, the first factor component continues across the actual first new position of the right hook.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.CohookExtension.secondComponent_support_outputPosition {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D M : Word R} (cohook : C.CohookExtension D) (hmono : IsMonomial R) (first : C.BoundaryFreeMorphismCoefficientComponent M) (second : M.BoundaryFreeMorphismCoefficientComponent D) (hinput : first.HasFullInputSupport) (hne : C.morphismCoefficientAt D hmono hmono (CategoryTheory.CategoryStruct.comp (C.boundaryFreeMorphismCoefficientComponentMap M hmono hmono first) (M.boundaryFreeMorphismCoefficientComponentMap D hmono hmono second)) (↑(cohook.moduleMapComponent hmono)).representative ≠ 0) {x : Q} (i : C.PositionAt x) : Relation.EqvGen (M.MorphismCoefficientStep D) (↑second).representative ⟨x, (first.outputPosition ⋯ i, cohook.toNegativeBoundaryExtension.toRightExtension.position i)⟩

Pointwise factorization alignment identifies the second component below the position selected by the full-input-support first component.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.CohookExtension.exists_firstNewPosition_support_of_component_pair_of_length_lt {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D M : Word R} (cohook : C.CohookExtension D) (hmono : IsMonomial R) (first : C.BoundaryFreeMorphismCoefficientComponent M) (second : M.BoundaryFreeMorphismCoefficientComponent D) (hinput : first.HasFullInputSupport) (hne : C.morphismCoefficientAt D hmono hmono (CategoryTheory.CategoryStruct.comp (C.boundaryFreeMorphismCoefficientComponentMap M hmono hmono first) (M.boundaryFreeMorphismCoefficientComponentMap D hmono hmono second)) (↑(cohook.moduleMapComponent hmono)).representative ≠ 0) (hlength : length R C < length R M) : ∃ (i : M.PositionAt cohook.vertex), (i.index = (first.outputPosition ⋯ C.targetPosition).index + 1 ∨ i.index + 1 = (first.outputPosition ⋯ C.targetPosition).index) ∧ Relation.EqvGen (M.MorphismCoefficientStep D) (↑second).representative ⟨cohook.vertex, (i, cohook.toNegativeBoundaryExtension.firstNewPosition)⟩

In the strict-growth branch, the second factor component continues across the actual first new position of the right cohook.