Proper intervals of full-support string graph components

The position selected by a one-sided full-support component traverses the entire shorter word with constant slope. When the other word is strictly longer, the selected interval has an explicit unused position on at least one of its two sides.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.BoundaryFreeMorphismCoefficientComponent.HasFullOutputSupport.inputPosition_endpointSlope {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (component : C.BoundaryFreeMorphismCoefficientComponent D) (hfull : component.HasFullOutputSupport) : (component.inputPosition ⋯ D.targetPosition).index = (component.inputPosition ⋯ D.sourcePosition).index + length R D ∨ (component.inputPosition ⋯ D.sourcePosition).index = (component.inputPosition ⋯ D.targetPosition).index + length R D

The source positions selected over the two target endpoints differ by the target word's length.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.BoundaryFreeMorphismCoefficientComponent.HasFullOutputSupport.inputPosition_properInterval {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (component : C.BoundaryFreeMorphismCoefficientComponent D) (hfull : component.HasFullOutputSupport) (hlength : length R D < length R C) : (component.inputPosition ⋯ D.targetPosition).index = (component.inputPosition ⋯ D.sourcePosition).index + length R D ∧ (0 < (component.inputPosition ⋯ D.sourcePosition).index ∨ (component.inputPosition ⋯ D.targetPosition).index < length R C) ∨ (component.inputPosition ⋯ D.sourcePosition).index = (component.inputPosition ⋯ D.targetPosition).index + length R D ∧ (0 < (component.inputPosition ⋯ D.targetPosition).index ∨ (component.inputPosition ⋯ D.sourcePosition).index < length R C)

If the source word is strictly longer, a full-target-support component occupies a proper source interval, with the unused side recorded together with its orientation.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.BoundaryFreeMorphismCoefficientComponent.HasFullInputSupport.outputPosition_endpointSlope {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (component : C.BoundaryFreeMorphismCoefficientComponent D) (hfull : component.HasFullInputSupport) : (component.outputPosition ⋯ C.targetPosition).index = (component.outputPosition ⋯ C.sourcePosition).index + length R C ∨ (component.outputPosition ⋯ C.sourcePosition).index = (component.outputPosition ⋯ C.targetPosition).index + length R C

The target positions selected over the two source endpoints differ by the source word's length.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.BoundaryFreeMorphismCoefficientComponent.HasFullInputSupport.outputPosition_properInterval {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (component : C.BoundaryFreeMorphismCoefficientComponent D) (hfull : component.HasFullInputSupport) (hlength : length R C < length R D) : (component.outputPosition ⋯ C.targetPosition).index = (component.outputPosition ⋯ C.sourcePosition).index + length R C ∧ (0 < (component.outputPosition ⋯ C.sourcePosition).index ∨ (component.outputPosition ⋯ C.targetPosition).index < length R D) ∨ (component.outputPosition ⋯ C.sourcePosition).index = (component.outputPosition ⋯ C.targetPosition).index + length R C ∧ (0 < (component.outputPosition ⋯ C.targetPosition).index ∨ (component.outputPosition ⋯ C.sourcePosition).index < length R D)

If the target word is strictly longer, a full-source-support component occupies a proper target interval, with the unused side recorded together with its orientation.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.BoundaryFreeMorphismCoefficientComponent.HasFullOutputSupport.exists_outgoingAtTarget_of_forward_of_lt {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (component : C.BoundaryFreeMorphismCoefficientComponent D) (hfull : component.HasFullOutputSupport) (hforward : (component.inputPosition ⋯ D.targetPosition).index = (component.inputPosition ⋯ D.sourcePosition).index + length R D) (hlt : (component.inputPosition ⋯ D.targetPosition).index < length R C) : ∃ (y : Q) (j : C.PositionAt y) (a : D.target ⟶ y), j.index = (component.inputPosition ⋯ D.targetPosition).index + 1 ∧ C.ArrowStep a (component.inputPosition ⋯ D.targetPosition) j

At the right end of an increasing full-target-support interval, an extra source-word edge must point out of the interval.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.BoundaryFreeMorphismCoefficientComponent.HasFullOutputSupport.exists_outgoingAtSource_of_forward_of_pos {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (component : C.BoundaryFreeMorphismCoefficientComponent D) (hfull : component.HasFullOutputSupport) (hforward : (component.inputPosition ⋯ D.targetPosition).index = (component.inputPosition ⋯ D.sourcePosition).index + length R D) (hpos : 0 < (component.inputPosition ⋯ D.sourcePosition).index) : ∃ (x : Q) (j : C.PositionAt x) (a : D.source ⟶ x), j.index + 1 = (component.inputPosition ⋯ D.sourcePosition).index ∧ C.ArrowStep a (component.inputPosition ⋯ D.sourcePosition) j

At the left end of an increasing full-target-support interval, an extra source-word edge must point out of the interval.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.BoundaryFreeMorphismCoefficientComponent.HasFullOutputSupport.exists_outgoingAtTarget_of_reverse_of_pos {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (component : C.BoundaryFreeMorphismCoefficientComponent D) (hfull : component.HasFullOutputSupport) (hreverse : (component.inputPosition ⋯ D.sourcePosition).index = (component.inputPosition ⋯ D.targetPosition).index + length R D) (hpos : 0 < (component.inputPosition ⋯ D.targetPosition).index) : ∃ (x : Q) (j : C.PositionAt x) (a : D.target ⟶ x), j.index + 1 = (component.inputPosition ⋯ D.targetPosition).index ∧ C.ArrowStep a (component.inputPosition ⋯ D.targetPosition) j

At the left end of a decreasing full-target-support interval, an extra source-word edge must point out of the interval.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.BoundaryFreeMorphismCoefficientComponent.HasFullOutputSupport.exists_outgoingAtSource_of_reverse_of_lt {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (component : C.BoundaryFreeMorphismCoefficientComponent D) (hfull : component.HasFullOutputSupport) (hreverse : (component.inputPosition ⋯ D.sourcePosition).index = (component.inputPosition ⋯ D.targetPosition).index + length R D) (hlt : (component.inputPosition ⋯ D.sourcePosition).index < length R C) : ∃ (y : Q) (j : C.PositionAt y) (a : D.source ⟶ y), j.index = (component.inputPosition ⋯ D.sourcePosition).index + 1 ∧ C.ArrowStep a (component.inputPosition ⋯ D.sourcePosition) j

At the right end of a decreasing full-target-support interval, an extra source-word edge must point out of the interval.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.BoundaryFreeMorphismCoefficientComponent.HasFullOutputSupport.exists_outgoingBoundary_of_length_lt {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (component : C.BoundaryFreeMorphismCoefficientComponent D) (hfull : component.HasFullOutputSupport) (hlength : length R D < length R C) : (component.inputPosition ⋯ D.targetPosition).index = (component.inputPosition ⋯ D.sourcePosition).index + length R D ∧ ((∃ (x : Q) (j : C.PositionAt x) (a : D.source ⟶ x), j.index + 1 = (component.inputPosition ⋯ D.sourcePosition).index ∧ C.ArrowStep a (component.inputPosition ⋯ D.sourcePosition) j) ∨ ∃ (y : Q) (j : C.PositionAt y) (a : D.target ⟶ y), j.index = (component.inputPosition ⋯ D.targetPosition).index + 1 ∧ C.ArrowStep a (component.inputPosition ⋯ D.targetPosition) j) ∨ (component.inputPosition ⋯ D.sourcePosition).index = (component.inputPosition ⋯ D.targetPosition).index + length R D ∧ ((∃ (x : Q) (j : C.PositionAt x) (a : D.target ⟶ x), j.index + 1 = (component.inputPosition ⋯ D.targetPosition).index ∧ C.ArrowStep a (component.inputPosition ⋯ D.targetPosition) j) ∨ ∃ (y : Q) (j : C.PositionAt y) (a : D.source ⟶ y), j.index = (component.inputPosition ⋯ D.sourcePosition).index + 1 ∧ C.ArrowStep a (component.inputPosition ⋯ D.sourcePosition) j)

A proper full-target-support interval has an outward source-word arrow at one of its four oriented boundaries.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.BoundaryFreeMorphismCoefficientComponent.HasFullInputSupport.exists_incomingAtTarget_of_forward_of_lt {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (component : C.BoundaryFreeMorphismCoefficientComponent D) (hfull : component.HasFullInputSupport) (hforward : (component.outputPosition ⋯ C.targetPosition).index = (component.outputPosition ⋯ C.sourcePosition).index + length R C) (hlt : (component.outputPosition ⋯ C.targetPosition).index < length R D) : ∃ (y : Q) (j : D.PositionAt y) (a : y ⟶ C.target), j.index = (component.outputPosition ⋯ C.targetPosition).index + 1 ∧ D.ArrowStep a j (component.outputPosition ⋯ C.targetPosition)

At the right end of an increasing full-source-support interval, an extra target-word edge must point into the interval.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.BoundaryFreeMorphismCoefficientComponent.HasFullInputSupport.exists_incomingAtSource_of_forward_of_pos {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (component : C.BoundaryFreeMorphismCoefficientComponent D) (hfull : component.HasFullInputSupport) (hforward : (component.outputPosition ⋯ C.targetPosition).index = (component.outputPosition ⋯ C.sourcePosition).index + length R C) (hpos : 0 < (component.outputPosition ⋯ C.sourcePosition).index) : ∃ (x : Q) (j : D.PositionAt x) (a : x ⟶ C.source), j.index + 1 = (component.outputPosition ⋯ C.sourcePosition).index ∧ D.ArrowStep a j (component.outputPosition ⋯ C.sourcePosition)

At the left end of an increasing full-source-support interval, an extra target-word edge must point into the interval.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.BoundaryFreeMorphismCoefficientComponent.HasFullInputSupport.exists_incomingAtTarget_of_reverse_of_pos {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (component : C.BoundaryFreeMorphismCoefficientComponent D) (hfull : component.HasFullInputSupport) (hreverse : (component.outputPosition ⋯ C.sourcePosition).index = (component.outputPosition ⋯ C.targetPosition).index + length R C) (hpos : 0 < (component.outputPosition ⋯ C.targetPosition).index) : ∃ (x : Q) (j : D.PositionAt x) (a : x ⟶ C.target), j.index + 1 = (component.outputPosition ⋯ C.targetPosition).index ∧ D.ArrowStep a j (component.outputPosition ⋯ C.targetPosition)

At the left end of a decreasing full-source-support interval, an extra target-word edge must point into the interval.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.BoundaryFreeMorphismCoefficientComponent.HasFullInputSupport.exists_incomingAtSource_of_reverse_of_lt {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (component : C.BoundaryFreeMorphismCoefficientComponent D) (hfull : component.HasFullInputSupport) (hreverse : (component.outputPosition ⋯ C.sourcePosition).index = (component.outputPosition ⋯ C.targetPosition).index + length R C) (hlt : (component.outputPosition ⋯ C.sourcePosition).index < length R D) : ∃ (y : Q) (j : D.PositionAt y) (a : y ⟶ C.source), j.index = (component.outputPosition ⋯ C.sourcePosition).index + 1 ∧ D.ArrowStep a j (component.outputPosition ⋯ C.sourcePosition)

At the right end of a decreasing full-source-support interval, an extra target-word edge must point into the interval.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.BoundaryFreeMorphismCoefficientComponent.HasFullInputSupport.exists_incomingBoundary_of_length_lt {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (component : C.BoundaryFreeMorphismCoefficientComponent D) (hfull : component.HasFullInputSupport) (hlength : length R C < length R D) : (component.outputPosition ⋯ C.targetPosition).index = (component.outputPosition ⋯ C.sourcePosition).index + length R C ∧ ((∃ (x : Q) (j : D.PositionAt x) (a : x ⟶ C.source), j.index + 1 = (component.outputPosition ⋯ C.sourcePosition).index ∧ D.ArrowStep a j (component.outputPosition ⋯ C.sourcePosition)) ∨ ∃ (y : Q) (j : D.PositionAt y) (a : y ⟶ C.target), j.index = (component.outputPosition ⋯ C.targetPosition).index + 1 ∧ D.ArrowStep a j (component.outputPosition ⋯ C.targetPosition)) ∨ (component.outputPosition ⋯ C.sourcePosition).index = (component.outputPosition ⋯ C.targetPosition).index + length R C ∧ ((∃ (x : Q) (j : D.PositionAt x) (a : x ⟶ C.target), j.index + 1 = (component.outputPosition ⋯ C.targetPosition).index ∧ D.ArrowStep a j (component.outputPosition ⋯ C.targetPosition)) ∨ ∃ (y : Q) (j : D.PositionAt y) (a : y ⟶ C.source), j.index = (component.outputPosition ⋯ C.sourcePosition).index + 1 ∧ D.ArrowStep a j (component.outputPosition ⋯ C.sourcePosition))

A proper full-source-support interval has an inward target-word arrow at one of its four oriented boundaries.