Propagating string graph components along one-sign arms

Support at the two endpoint indices fills the complete intervening word by component convexity. Boundary-freeness propagates endpoint support through a negative source arm or, dually, through a positive target arm.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.BoundaryFreeMorphismCoefficientComponent.hasFullInputSupport_of_endpoint_support {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (component : C.BoundaryFreeMorphismCoefficientComponent D) (j₀ : D.PositionAt C.source) (jₙ : D.PositionAt C.target) (h₀ : Relation.EqvGen (C.MorphismCoefficientStep D) (↑component).representative ⟨C.source, (C.sourcePosition, j₀)⟩) (hₙ : Relation.EqvGen (C.MorphismCoefficientStep D) (↑component).representative ⟨C.target, (C.targetPosition, jₙ)⟩) : component.HasFullInputSupport

Support above the two source-word endpoints fills every source position of a coefficient component.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.BoundaryFreeMorphismCoefficientComponent.hasFullOutputSupport_of_endpoint_support {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (component : C.BoundaryFreeMorphismCoefficientComponent D) (i₀ : C.PositionAt D.source) (iₙ : C.PositionAt D.target) (h₀ : Relation.EqvGen (C.MorphismCoefficientStep D) (↑component).representative ⟨D.source, (i₀, D.sourcePosition)⟩) (hₙ : Relation.EqvGen (C.MorphismCoefficientStep D) (↑component).representative ⟨D.target, (iₙ, D.targetPosition)⟩) : component.HasFullOutputSupport

Support below the two target-word endpoints fills every target position of a coefficient component.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.BoundaryFreeMorphismCoefficientComponent.hasFullInputSupport_of_support_at_endpoint_indices {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (component : C.BoundaryFreeMorphismCoefficientComponent D) {p₀ pₙ : C.MorphismCoefficientPosition D} (h₀ : Relation.EqvGen (C.MorphismCoefficientStep D) (↑component).representative p₀) (hₙ : Relation.EqvGen (C.MorphismCoefficientStep D) (↑component).representative pₙ) (hp₀ : p₀.inputIndex = 0) (hpₙ : pₙ.inputIndex = length R C) : component.HasFullInputSupport

Support at source-index zero and source-index C.length fills every source position, without requiring the two witnesses to be presented using the named endpoint positions.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.BoundaryFreeMorphismCoefficientComponent.hasFullOutputSupport_of_support_at_endpoint_indices {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (component : C.BoundaryFreeMorphismCoefficientComponent D) {p₀ pₙ : C.MorphismCoefficientPosition D} (h₀ : Relation.EqvGen (C.MorphismCoefficientStep D) (↑component).representative p₀) (hₙ : Relation.EqvGen (C.MorphismCoefficientStep D) (↑component).representative pₙ) (hp₀ : p₀.outputIndex = 0) (hpₙ : pₙ.outputIndex = length R D) : component.HasFullOutputSupport

Support at target-index zero and target-index D.length fills every target position, without requiring the two witnesses to be presented using the named endpoint positions.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.NegativeExtension.exists_target_support_of_base_target_support {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {B E D M : Word R} (arm : B.NegativeExtension E) (suffix : E.RightExtension D) (component : D.BoundaryFreeMorphismCoefficientComponent M) (j₀ : M.PositionAt B.target) (h₀ : Relation.EqvGen (D.MorphismCoefficientStep M) (↑component).representative ⟨B.target, ((arm.toRightExtension.trans suffix).position B.targetPosition, j₀)⟩) : ∃ (jₙ : M.PositionAt E.target), Relation.EqvGen (D.MorphismCoefficientStep M) (↑component).representative ⟨E.target, (suffix.position E.targetPosition, jₙ)⟩

If a component from the final word supports the embedded base endpoint, then it supports the embedded final endpoint of every negative arm.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.PositiveExtension.exists_target_support_of_base_target_support {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {B E D M : Word R} (arm : B.PositiveExtension E) (suffix : E.RightExtension D) (component : M.BoundaryFreeMorphismCoefficientComponent D) (i₀ : M.PositionAt B.target) (h₀ : Relation.EqvGen (M.MorphismCoefficientStep D) (↑component).representative ⟨B.target, (i₀, (arm.toRightExtension.trans suffix).position B.targetPosition)⟩) : ∃ (iₙ : M.PositionAt E.target), Relation.EqvGen (M.MorphismCoefficientStep D) (↑component).representative ⟨E.target, (iₙ, suffix.position E.targetPosition)⟩

If a component into the final word supports the embedded base endpoint, then it supports the embedded final endpoint of every positive arm.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.HookExtension.firstComponent_hasFullInputSupport_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) : first.HasFullInputSupport

In a strict-growth right-hook factorization, propagation through the negative tail makes the selected first component cover the complete hook word.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.CohookExtension.secondComponent_hasFullOutputSupport_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) : second.HasFullOutputSupport

In a strict-growth right-cohook factorization, propagation through the positive tail makes the selected second component cover the complete cohook word.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.HookExtension.firstFactor_isIso_of_intermediate_length_eq_result {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D M : Word R} (hook : C.HookExtension D) (hmono : IsMonomial R) (f : D.rightModule hmono ⟶ M.rightModule hmono) (g : M.rightModule hmono ⟶ C.rightModule hmono) (hfactor : CategoryTheory.CategoryStruct.comp f g = hook.moduleMap hmono) (hlength : length R M = length R D) : CategoryTheory.IsIso f

If the intermediate string has the hook result's length, the first factor of a right-hook factorization is an isomorphism.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.CohookExtension.secondFactor_isIso_of_intermediate_length_eq_result {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D M : Word R} (cohook : C.CohookExtension D) (hmono : IsMonomial R) (f : C.rightModule hmono ⟶ M.rightModule hmono) (g : M.rightModule hmono ⟶ D.rightModule hmono) (hfactor : CategoryTheory.CategoryStruct.comp f g = cohook.moduleMap hmono) (hlength : length R M = length R D) : CategoryTheory.IsIso g

If the intermediate string has the cohook result's length, the second factor of a right-cohook factorization is an isomorphism.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.HookExtension.result_length_lt_intermediate_of_not_split {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D M : Word R} (hook : C.HookExtension D) (hmono : IsMonomial R) (f : D.rightModule hmono ⟶ M.rightModule hmono) (g : M.rightModule hmono ⟶ C.rightModule hmono) (hfactor : CategoryTheory.CategoryStruct.comp f g = hook.moduleMap hmono) (hf : ¬CategoryTheory.IsSplitMono f) (hg : ¬CategoryTheory.IsSplitEpi g) : length R D < length R M

A literal-string factorization of a right hook with neither factor split must pass through a word strictly longer than the complete hook word.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.CohookExtension.result_length_lt_intermediate_of_not_split {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D M : Word R} (cohook : C.CohookExtension D) (hmono : IsMonomial R) (f : C.rightModule hmono ⟶ M.rightModule hmono) (g : M.rightModule hmono ⟶ D.rightModule hmono) (hfactor : CategoryTheory.CategoryStruct.comp f g = cohook.moduleMap hmono) (hf : ¬CategoryTheory.IsSplitMono f) (hg : ¬CategoryTheory.IsSplitEpi g) : length R D < length R M

A literal-string factorization of a right cohook with neither factor split must pass through a word strictly longer than the complete cohook word.