Boundary continuation for string graph components

A boundary-free coefficient component cannot stop against a displayed arrow which continues on the other word in the forbidden direction. These lemmas turn that condition into explicit matched-arrow and continued-support witnesses.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.BoundaryFreeMorphismCoefficientComponent.exists_inputArrowStep_of_outputArrowStep {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (component : C.BoundaryFreeMorphismCoefficientComponent D) {x y : Q} (a : x ⟶ y) (i : C.PositionAt x) (i' : D.PositionAt x) (j' : D.PositionAt y) (hsupport : Relation.EqvGen (C.MorphismCoefficientStep D) (↑component).representative ⟨x, (i, i')⟩) (hstep : D.ArrowStep a i' j') : ∃ (j : C.PositionAt y), C.ArrowStep a i j

An outgoing target-word arrow at a supported pair has a matching outgoing source-word arrow.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.BoundaryFreeMorphismCoefficientComponent.exists_outputArrowStep_of_inputArrowStep {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (component : C.BoundaryFreeMorphismCoefficientComponent D) {x y : Q} (a : x ⟶ y) (i : C.PositionAt x) (j : C.PositionAt y) (j' : D.PositionAt y) (hsupport : Relation.EqvGen (C.MorphismCoefficientStep D) (↑component).representative ⟨y, (j, j')⟩) (hstep : C.ArrowStep a i j) : ∃ (i' : D.PositionAt x), D.ArrowStep a i' j'

An incoming source-word arrow at a supported pair has a matching incoming target-word arrow.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.BoundaryFreeMorphismCoefficientComponent.exists_support_of_outputArrowStep {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (component : C.BoundaryFreeMorphismCoefficientComponent D) {x y : Q} (a : x ⟶ y) (i : C.PositionAt x) (i' : D.PositionAt x) (j' : D.PositionAt y) (hsupport : Relation.EqvGen (C.MorphismCoefficientStep D) (↑component).representative ⟨x, (i, i')⟩) (hstep : D.ArrowStep a i' j') : ∃ (j : C.PositionAt y), C.ArrowStep a i j ∧ Relation.EqvGen (C.MorphismCoefficientStep D) (↑component).representative ⟨y, (j, j')⟩

A supported pair continues across any outgoing target-word arrow.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.BoundaryFreeMorphismCoefficientComponent.exists_support_of_inputArrowStep {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (component : C.BoundaryFreeMorphismCoefficientComponent D) {x y : Q} (a : x ⟶ y) (i : C.PositionAt x) (j : C.PositionAt y) (j' : D.PositionAt y) (hsupport : Relation.EqvGen (C.MorphismCoefficientStep D) (↑component).representative ⟨y, (j, j')⟩) (hstep : C.ArrowStep a i j) : ∃ (i' : D.PositionAt x), D.ArrowStep a i' j' ∧ Relation.EqvGen (C.MorphismCoefficientStep D) (↑component).representative ⟨x, (i, i')⟩

A supported pair continues backwards across any incoming source-word arrow.