Tracing detector coordinates through a literal string

A basis coordinate which survives the difference between two transported coordinate subspaces cannot arise from a kernel contribution at an inverse letter: such a contribution belongs to both transports. It therefore has a unique predecessor at every signed letter. Iterating this observation turns a surviving detector coordinate into a literal occurrence of the detector word in the evaluated string.

def MagnitudeConjecture.BoundQuiver.StringWord.Word.SignedArrowPositionStep {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (D : Word R) {x y : Q} (e : SignedArrow x y) (i : D.PositionAt x) (j : D.PositionAt y) : Prop

A signed arrow of one word is realized by adjacent positions of another word, respecting the signed direction.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.signedArrowPositionStep_iff {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (D : Word R) {x y : Q} (e : SignedArrow x y) (i : D.PositionAt x) (j : D.PositionAt y) : D.SignedArrowPositionStep e i j ↔ ↑j = Quiver.Path.comp (↑i) (Quiver.Hom.toPath e) ∨ ↑i = Quiver.Path.comp (↑j) (Quiver.reverse e).toPath

The signed formulation says directly that the target position is one letter forward or the source position is one reversed letter forward.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.SignedArrowPositionStep.index {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (D : Word R) {x y : Q} {e : SignedArrow x y} {i : D.PositionAt x} {j : D.PositionAt y} (hstep : D.SignedArrowPositionStep e i j) : j.index = i.index + 1 ∨ i.index = j.index + 1

A realized signed arrow changes the word-position index by one.

@[irreducible]

def MagnitudeConjecture.BoundQuiver.StringWord.Word.SignedPathPositionReach {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (D : Word R) {x y : Q} : SignedPath x y → D.PositionAt x → D.PositionAt y → Prop

A complete signed path is realized by a consecutive position walk in a literal string word.

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.signedPathPositionReach_nil {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (D : Word R) {x : Q} (i j : D.PositionAt x) : D.SignedPathPositionReach Quiver.Path.nil i j ↔ i = j

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.signedPathPositionReach_cons {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (D : Word R) {x y z : Q} (p : SignedPath x y) (e : SignedArrow y z) (i : D.PositionAt x) (l : D.PositionAt z) : D.SignedPathPositionReach (Quiver.Path.cons p e) i l ↔ ∃ (j : D.PositionAt y), D.SignedPathPositionReach p i j ∧ D.SignedArrowPositionStep e j l

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.exists_positionStep_of_single_mem_signedArrowSubspace_not_mem {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (D : Word R) (hmono : IsMonomial R) {x y : Q} (e : SignedArrow x y) {U V : Submodule k (D.Space x)} (hV : D.IsCoordinateSubspace V) (j : D.PositionAt y) (hjV : Finsupp.single j 1 ∈ signedArrowSubspace (D.rightModule hmono) e V) (hjU : Finsupp.single j 1 ∉ signedArrowSubspace (D.rightModule hmono) e U) : ∃ (i : D.PositionAt x), D.SignedArrowPositionStep e i j ∧ Finsupp.single i 1 ∈ V ∧ Finsupp.single i 1 ∉ U

A basis coordinate surviving the difference of two one-arrow transports has a predecessor which survives the original difference.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.exists_positionReach_of_single_mem_signedPathSubspace_not_mem {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (D : Word R) (hmono : IsMonomial R) {x y : Q} (p : SignedPath x y) {U V : Submodule k (D.Space x)} : D.IsCoordinateSubspace V → ∀ (j : D.PositionAt y), Finsupp.single j 1 ∈ signedPathSubspace (D.rightModule hmono) p V → Finsupp.single j 1 ∉ signedPathSubspace (D.rightModule hmono) p U → ∃ (i : D.PositionAt x), D.SignedPathPositionReach p i j ∧ Finsupp.single i 1 ∈ V ∧ Finsupp.single i 1 ∉ U

A basis coordinate surviving the difference of two signed-path transports traces back to a source basis coordinate surviving the original difference.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.morphismCoefficientPosition_eqvGen_of_positionReach {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C D : Word R) {i : D.PositionAt C.source} {j : D.PositionAt C.target} (hreach : D.SignedPathPositionReach C.path i j) : Relation.EqvGen (C.MorphismCoefficientStep D) ⟨C.source, (C.sourcePosition, i)⟩ ⟨C.target, (C.targetPosition, j)⟩

A realized complete word path places its two endpoint pairs in one matched-coefficient component.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.positionReach_endpointSlope {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C D : Word R) {i : D.PositionAt C.source} {j : D.PositionAt C.target} (hreach : D.SignedPathPositionReach C.path i j) : j.index = i.index + length R C ∨ i.index = j.index + length R C

A realized complete word has constant position slope in the evaluated literal string.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.positionReach_prefix_eq_of_forward {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (D : Word R) {x y : Quiver.Symmetrify Q} (p : Quiver.Path x y) : IsString R p → ∀ (i : D.PositionAt (have this := x; this)) (j : D.PositionAt (have this := y; this)), D.SignedPathPositionReach p i j → j.index = i.index + p.length → ↑j = Quiver.Path.comp (↑i) p

In the increasing slope, a realized signed path is literally the segment between the two position prefixes.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.positionReach_prefix_eq_of_reverse {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (D : Word R) {x y : Quiver.Symmetrify Q} (p : Quiver.Path x y) : IsString R p → ∀ (i : D.PositionAt (have this := x; this)) (j : D.PositionAt (have this := y; this)), D.SignedPathPositionReach p i j → i.index = j.index + p.length → ↑i = Quiver.Path.comp (↑j) p.reverse

In the decreasing slope, the source prefix is the target prefix followed by the reverse of the realized signed path.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.positionReach_self_eq_targetPosition {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) {i : C.PositionAt C.source} {j : C.PositionAt C.target} (hreach : C.SignedPathPositionReach C.path i j) : j = C.targetPosition

A complete occurrence of a reduced word inside itself can only end at the canonical target position. The decreasing slope would make the whole word a reverse palindrome, which reducedness excludes unless its length is zero.