Convex source support of string coefficient components

The forward partial-bijection relation linearly orders each generated coefficient component. Every source-word index between two component vertices is therefore represented by a unique component vertex.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.reflTransGen_morphismCoefficientForwardStep_or_reverse_of_eqvGen {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C D : Word R) {p q : C.MorphismCoefficientPosition D} (hpq : Relation.EqvGen (C.MorphismCoefficientStep D) p q) : Relation.ReflTransGen (C.MorphismCoefficientForwardStep D) p q ∨ Relation.ReflTransGen (C.MorphismCoefficientForwardStep D) q p

Two vertices in one coefficient component are comparable by forward reachability.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.reflTransGen_morphismCoefficientForwardStep_of_eqvGen_of_inputIndex_le {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C D : Word R) {p q : C.MorphismCoefficientPosition D} (hpq : Relation.EqvGen (C.MorphismCoefficientStep D) p q) (hindex : p.inputIndex ≤ q.inputIndex) : Relation.ReflTransGen (C.MorphismCoefficientForwardStep D) p q

Component comparability is oriented by the order of source indices.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.exists_reflTransGen_morphismCoefficientForwardStep_inputIndex_eq {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C D : Word R) {p q : C.MorphismCoefficientPosition D} (hpq : Relation.ReflTransGen (C.MorphismCoefficientForwardStep D) p q) (n : ℕ) (hpn : p.inputIndex ≤ n) (hnq : n ≤ q.inputIndex) : ∃ (r : C.MorphismCoefficientPosition D), Relation.ReflTransGen (C.MorphismCoefficientForwardStep D) p r ∧ r.inputIndex = n

Every integer index between the endpoints of a forward coefficient walk occurs along that walk.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.morphismCoefficientForwardStep_of_reflTransGen_of_inputIndex_add_one {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C D : Word R) {p q : C.MorphismCoefficientPosition D} (hpq : Relation.ReflTransGen (C.MorphismCoefficientForwardStep D) p q) (hindex : q.inputIndex = p.inputIndex + 1) : C.MorphismCoefficientForwardStep D p q

A forward walk whose input indices differ by exactly one is a single forward edge.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.morphismCoefficientStep_eqvGen_of_reflTransGen_forward {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C D : Word R) {p q : C.MorphismCoefficientPosition D} (hpq : Relation.ReflTransGen (C.MorphismCoefficientForwardStep D) p q) : Relation.EqvGen (C.MorphismCoefficientStep D) p q

A forward coefficient walk is contained in the original matched-step component.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.exists_morphismCoefficientComponentSupport_inputIndex_eq_of_between {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C D : Word R) (root : C.MorphismCoefficientPosition D) (p q : C.MorphismCoefficientComponentSupport D root) (n : ℕ) (hpn : (↑p).inputIndex ≤ n) (hnq : n ≤ (↑q).inputIndex) : ∃ (r : C.MorphismCoefficientComponentSupport D root), (↑r).inputIndex = n

The source-index projection of a coefficient component is a convex interval: every index between two supported indices is supported.

def MagnitudeConjecture.BoundQuiver.StringWord.Word.morphismCoefficientComponentSupportTranspose {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C D : Word R) (root : C.MorphismCoefficientPosition D) : C.MorphismCoefficientComponentSupport D root ≃ D.MorphismCoefficientComponentSupport C ((C.morphismCoefficientPositionTranspose D) root)

Transposition identifies a component support with the corresponding component support for the reversed word pair.

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.morphismCoefficientComponentSupportTranspose_apply_val {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C D : Word R) (root : C.MorphismCoefficientPosition D) (p : C.MorphismCoefficientComponentSupport D root) : ↑((C.morphismCoefficientComponentSupportTranspose D root) p) = (C.morphismCoefficientPositionTranspose D) ↑p

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.morphismCoefficientComponentSupportTranspose_symm_apply_val {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C D : Word R) (root : C.MorphismCoefficientPosition D) (q : D.MorphismCoefficientComponentSupport C ((C.morphismCoefficientPositionTranspose D) root)) : ↑((C.morphismCoefficientComponentSupportTranspose D root).symm q) = (D.morphismCoefficientPositionTranspose C) ↑q

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.exists_morphismCoefficientComponentSupport_outputIndex_eq_of_between {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C D : Word R) (root : C.MorphismCoefficientPosition D) (p q : C.MorphismCoefficientComponentSupport D root) (n : ℕ) (hpn : (↑p).outputIndex ≤ n) (hnq : n ≤ (↑q).outputIndex) : ∃ (r : C.MorphismCoefficientComponentSupport D root), (↑r).outputIndex = n

The target-index projection of a coefficient component is also a convex interval.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.MorphismCoefficientForwardStep.outputIndex {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C D : Word R) {p q : C.MorphismCoefficientPosition D} (hpq : C.MorphismCoefficientForwardStep D p q) : q.outputIndex = p.outputIndex + 1 ∨ p.outputIndex = q.outputIndex + 1

A forward coefficient edge changes the target-word index by one in one of the two directions.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.morphismCoefficientForwardStep_outputIndex_no_turn {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C D : Word R) {p q r : C.MorphismCoefficientPosition D} (hpq : C.MorphismCoefficientForwardStep D p q) (hqr : C.MorphismCoefficientForwardStep D q r) : q.outputIndex = p.outputIndex + 1 ∧ r.outputIndex = q.outputIndex + 1 ∨ p.outputIndex = q.outputIndex + 1 ∧ q.outputIndex = r.outputIndex + 1

The target direction cannot turn across two consecutive forward edges. Such a turn would repeat a target position inside one component.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.transGen_morphismCoefficientForwardStep_outputSlope_and_last {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C D : Word R) {p q : C.MorphismCoefficientPosition D} (hpq : Relation.TransGen (C.MorphismCoefficientForwardStep D) p q) : (q.outputIndex = p.outputIndex + (q.inputIndex - p.inputIndex) ∧ ∃ (r : C.MorphismCoefficientPosition D), C.MorphismCoefficientForwardStep D r q ∧ q.outputIndex = r.outputIndex + 1) ∨ p.outputIndex = q.outputIndex + (q.inputIndex - p.inputIndex) ∧ ∃ (r : C.MorphismCoefficientPosition D), C.MorphismCoefficientForwardStep D r q ∧ r.outputIndex = q.outputIndex + 1

Along a nonempty forward chain, the target index has one constant slope; the final edge records the same slope as the endpoint formula.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.transGen_morphismCoefficientForwardStep_outputSlope {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C D : Word R) {p q : C.MorphismCoefficientPosition D} (hpq : Relation.TransGen (C.MorphismCoefficientForwardStep D) p q) : q.outputIndex = p.outputIndex + (q.inputIndex - p.inputIndex) ∨ p.outputIndex = q.outputIndex + (q.inputIndex - p.inputIndex)

Endpoints of a nonempty forward chain have target displacement equal in absolute value to their source displacement.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.reflTransGen_morphismCoefficientForwardStep_outputSlope {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C D : Word R) {p q : C.MorphismCoefficientPosition D} (hpq : Relation.ReflTransGen (C.MorphismCoefficientForwardStep D) p q) : q.outputIndex = p.outputIndex + (q.inputIndex - p.inputIndex) ∨ p.outputIndex = q.outputIndex + (q.inputIndex - p.inputIndex)

The same constant-slope formula, including the reflexive chain.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.morphismCoefficientStep_eqvGen_outputSlope_of_inputIndex_le {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C D : Word R) {p q : C.MorphismCoefficientPosition D} (hpq : Relation.EqvGen (C.MorphismCoefficientStep D) p q) (hindex : p.inputIndex ≤ q.inputIndex) : q.outputIndex = p.outputIndex + (q.inputIndex - p.inputIndex) ∨ p.outputIndex = q.outputIndex + (q.inputIndex - p.inputIndex)

Within one coefficient component, ordering by source index identifies the component correspondence with an interval map of constant slope one or minus one.