Prefix extensions of string words

A right prefix extension records an arbitrary finite sequence of letters appended to a string word. It retains the canonical embedding of old word positions and the split coordinate inclusion/projection on every displayed vertex space. The first appended letter is recorded separately when its sign controls whether the old coordinates form a subrepresentation or a quotient representation.

def MagnitudeConjecture.BoundQuiver.StringWord.Word.ofStringPath {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {source target : Q} (path : SignedPath source target) (h : IsString R path) : Word R

Bundle an already certified string path as a word.

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.ofStringPath_word_path {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) : ofStringPath C.path ⋯ = C

inductive MagnitudeConjecture.BoundQuiver.StringWord.Word.RightExtension {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) : Word R → Type u

An arbitrary finite sequence of letters appended at the right endpoint of C.

• base {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C : Word R} : C.RightExtension C
• step {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (extension : C.RightExtension D) {z : Q} (e : SignedArrow D.target z) (h : IsString R (Quiver.Path.comp D.path (Quiver.Hom.toPath e))) : C.RightExtension (append R D e h)

def MagnitudeConjecture.BoundQuiver.StringWord.Word.RightExtension.steps {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} : C.RightExtension D → ℕ

Number of appended letters.

def MagnitudeConjecture.BoundQuiver.StringWord.Word.RightExtension.suffixPath {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} : C.RightExtension D → SignedPath C.target D.target

The signed suffix appended by a right extension.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.RightExtension.source_eq {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (extension : C.RightExtension D) : D.source = C.source

A right extension does not change the source vertex.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.RightExtension.path_cast_comp_suffixPath {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (extension : C.RightExtension D) : Quiver.Path.cast ⋯ ⋯ D.path = Quiver.Path.comp C.path extension.suffixPath

The final path is the original path followed by the recorded suffix. The source cast is necessary because source preservation is propositional for an indexed extension record.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.RightExtension.comp_suffixPath_isString {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (extension : C.RightExtension D) : IsString R (Quiver.Path.comp C.path extension.suffixPath)

The explicit original-path-plus-suffix factorization is itself a string.

structure MagnitudeConjecture.BoundQuiver.StringWord.Word.RightExtension.RebaseResult {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (extension : C.RightExtension D) {source : Q} (basePath : SignedPath source C.target) (hbase : IsString R basePath) : Type u

Replaying an extension suffix after a different path with the same final vertex.

• result : Word R
• rebased : (ofStringPath basePath hbase).RightExtension self.result
• source_eq : self.result.source = source
• target_eq : self.result.target = D.target
• path_cast_eq : Quiver.Path.cast ⋯ ⋯ self.result.path = Quiver.Path.comp basePath extension.suffixPath

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.RightExtension.rebase {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (extension : C.RightExtension D) {source : Q} (basePath : SignedPath source C.target) (hbase : IsString R basePath) (hfull : IsString R (Quiver.Path.comp basePath extension.suffixPath)) : extension.RebaseResult basePath hbase

Replay a right extension after a different certified prefix. It is enough to know that the path with the complete replayed suffix is a string; all intermediate validity proofs follow by contiguous-subpath heredity.

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.RightExtension.rebase_steps {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (extension : C.RightExtension D) {source : Q} (basePath : SignedPath source C.target) (hbase : IsString R basePath) (hfull : IsString R (Quiver.Path.comp basePath extension.suffixPath)) : (extension.rebase basePath hbase hfull).rebased.steps = extension.steps

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.RightExtension.suffixPath_length {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (extension : C.RightExtension D) : Quiver.Path.length extension.suffixPath = extension.steps

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.RightExtension.result_length {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (extension : C.RightExtension D) : length R D = length R C + extension.steps

The final word is longer by exactly the number of appended letters.

def MagnitudeConjecture.BoundQuiver.StringWord.Word.RightExtension.trans {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D E : Word R} (first : C.RightExtension D) (second : D.RightExtension E) : C.RightExtension E

Concatenate two right extensions.

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.RightExtension.base_trans {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (extension : C.RightExtension D) : base.trans extension = extension

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.RightExtension.trans_base {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (extension : C.RightExtension D) : extension.trans base = extension

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.RightExtension.steps_trans {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D E : Word R} (first : C.RightExtension D) (second : D.RightExtension E) : (first.trans second).steps = first.steps + second.steps

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.RightExtension.suffixPath_trans {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D E : Word R} (first : C.RightExtension D) (second : D.RightExtension E) : (first.trans second).suffixPath = Quiver.Path.comp first.suffixPath second.suffixPath

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.RightExtension.trans_assoc {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {B C D E : Word R} (first : B.RightExtension C) (second : C.RightExtension D) (third : D.RightExtension E) : (first.trans second).trans third = first.trans (second.trans third)

Concatenation of right extensions is associative as dependent extension data.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.RightExtension.position {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (extension : C.RightExtension D) {x : Q} (i : C.PositionAt x) : D.PositionAt x

Embed every old prefix position into the extended word.

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.RightExtension.position_index {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (extension : C.RightExtension D) {x : Q} (i : C.PositionAt x) : (extension.position i).index = i.index

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.RightExtension.position_trans {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D E : Word R} (first : C.RightExtension D) (second : D.RightExtension E) {x : Q} (i : C.PositionAt x) : (first.trans second).position i = second.position (first.position i)

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.RightExtension.position_injective {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (extension : C.RightExtension D) {x : Q} : Function.Injective extension.position

The old-position embedding is injective.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.RightExtension.steps_transport_source {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C C' D : Word R} (h : C = C') (extension : C.RightExtension D) : (⋯.mp extension).steps = extension.steps

Transporting the source word of an extension does not change its number of appended letters.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.RightExtension.arrowStep_position {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (extension : C.RightExtension D) {x y : Q} (a : x ⟶ y) (i : C.PositionAt x) (j : C.PositionAt y) (hij : C.ArrowStep a i j) : D.ArrowStep a (extension.position i) (extension.position j)

Every arrow step between old positions remains an arrow step after an arbitrary right extension.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.RightExtension.arrowStep_position_iff {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (extension : C.RightExtension D) {x y : Q} (a : x ⟶ y) (i : C.PositionAt x) (j : C.PositionAt y) : D.ArrowStep a (extension.position i) (extension.position j) ↔ C.ArrowStep a i j

Appending further letters neither creates nor removes an arrow step between two inherited positions.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.RightExtension.exists_eq_position_of_index_le {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (extension : C.RightExtension D) {x : Q} (j : D.PositionAt x) (hj : j.index ≤ length R C) : ∃ (i : C.PositionAt x), extension.position i = j

Every position in the extended word at or before the old final index is the image of a unique old position.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.RightExtension.spaceInclusion {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (extension : C.RightExtension D) (x : Q) : C.Space x →ₗ[k] D.Space x

Coordinate inclusion of the old position basis into an arbitrary right extension.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.RightExtension.spaceProjection {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (extension : C.RightExtension D) (x : Q) : D.Space x →ₗ[k] C.Space x

Coordinate projection from an arbitrary extension onto its old position basis.

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.RightExtension.spaceInclusion_single {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (extension : C.RightExtension D) {x : Q} (i : C.PositionAt x) (c : k) : (extension.spaceInclusion x) (Finsupp.single i c) = Finsupp.single (extension.position i) c

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.RightExtension.spaceProjection_single_position {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (extension : C.RightExtension D) {x : Q} (i : C.PositionAt x) (c : k) : (extension.spaceProjection x) (Finsupp.single (extension.position i) c) = Finsupp.single i c

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.RightExtension.spaceProjection_single_of_not_exists {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (extension : C.RightExtension D) {x : Q} (j : D.PositionAt x) (c : k) (hj : ¬∃ (i : C.PositionAt x), extension.position i = j) : (extension.spaceProjection x) (Finsupp.single j c) = 0

Coordinate projection kills a basis position not inherited from the old word.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.RightExtension.spaceProjection_inclusion {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (extension : C.RightExtension D) (x : Q) (v : C.Space x) : (extension.spaceProjection x) ((extension.spaceInclusion x) v) = v

Projection is a left inverse to inclusion on every vertex space.

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.RightExtension.spaceProjection_apply_position {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (extension : C.RightExtension D) {x : Q} (v : D.Space x) (i : C.PositionAt x) : ((extension.spaceProjection x) v) i = v (extension.position i)

Projection reads the coefficient at the corresponding inherited position.

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.RightExtension.spaceInclusion_apply_position {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (extension : C.RightExtension D) {x : Q} (v : C.Space x) (i : C.PositionAt x) : ((extension.spaceInclusion x) v) (extension.position i) = v i

Inclusion preserves the coefficient at every inherited position.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.RightExtension.spaceInclusion_apply_of_not_exists {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (extension : C.RightExtension D) {x : Q} (v : C.Space x) (j : D.PositionAt x) (hj : ¬∃ (i : C.PositionAt x), extension.position i = j) : ((extension.spaceInclusion x) v) j = 0

Inclusion has zero coefficient at every non-inherited position.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.RightExtension.spaceInclusion_injective {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (extension : C.RightExtension D) (x : Q) : Function.Injective ⇑(extension.spaceInclusion x)

Coordinate inclusion along a right extension is injective.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.RightExtension.spaceProjection_surjective {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (extension : C.RightExtension D) (x : Q) : Function.Surjective ⇑(extension.spaceProjection x)

Coordinate projection along a right extension is surjective.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.RightExtension.spaceInclusion_trans_apply {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D E : Word R} (first : C.RightExtension D) (second : D.RightExtension E) (x : Q) (v : C.Space x) : ((first.trans second).spaceInclusion x) v = (second.spaceInclusion x) ((first.spaceInclusion x) v)

Coordinate inclusions compose when right extensions are concatenated.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.RightExtension.spaceProjection_trans_apply {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D E : Word R} (first : C.RightExtension D) (second : D.RightExtension E) (x : Q) (v : E.Space x) : ((first.trans second).spaceProjection x) v = (first.spaceProjection x) ((second.spaceProjection x) v)

Coordinate projections compose in the reverse order when right extensions are concatenated.

def MagnitudeConjecture.BoundQuiver.StringWord.Word.NegativeExtension.toRightExtension {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (arm : C.NegativeExtension D) : C.RightExtension D

Forget that every letter of a negative arm has the same sign.

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.NegativeExtension.toRightExtension_steps {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (arm : C.NegativeExtension D) : arm.toRightExtension.steps = arm.steps

def MagnitudeConjecture.BoundQuiver.StringWord.Word.PositiveExtension.toRightExtension {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (arm : C.PositiveExtension D) : C.RightExtension D

Forget that every letter of a positive arm has the same sign.

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.PositiveExtension.toRightExtension_steps {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (arm : C.PositiveExtension D) : arm.toRightExtension.steps = arm.steps

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.PositiveExtension.toRightExtension_suffixPath_eq_positivePath {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (arm : C.PositiveExtension D) : arm.toRightExtension.suffixPath = positivePath arm.ordinaryPath

Forgetting positivity retains exactly the positive signed path associated to the ordinary displayed-quiver arm.

structure MagnitudeConjecture.BoundQuiver.StringWord.Word.NegativeBoundaryExtension {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C D : Word R) : Type u

A nonempty right extension whose first appended letter is negative. Its remaining tail may contain arbitrary signs.

• vertex : Q
• arrow : self.vertex ⟶ C.target
• valid : IsString R (Quiver.Path.comp C.path (Quiver.Hom.toPath (negativeArrow self.arrow)))
• tail : (append R C (negativeArrow self.arrow) ⋯).RightExtension D

def MagnitudeConjecture.BoundQuiver.StringWord.Word.NegativeBoundaryExtension.toRightExtension {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (extension : C.NegativeBoundaryExtension D) : C.RightExtension D

Forget the marked first negative letter.

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.NegativeBoundaryExtension.toRightExtension_position {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (extension : C.NegativeBoundaryExtension D) {x : Q} (i : C.PositionAt x) : extension.toRightExtension.position i = extension.tail.position (C.appendPosition (negativeArrow extension.arrow) ⋯ i)

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.NegativeBoundaryExtension.firstNewPosition {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (extension : C.NegativeBoundaryExtension D) : D.PositionAt extension.vertex

The first position created by a negative-boundary extension, retained through its arbitrary tail.

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.NegativeBoundaryExtension.firstNewPosition_index {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (extension : C.NegativeBoundaryExtension D) : extension.firstNewPosition.index = length R C + 1

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.NegativeBoundaryExtension.arrowStep_firstNewPosition {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (extension : C.NegativeBoundaryExtension D) : D.ArrowStep extension.arrow extension.firstNewPosition (extension.toRightExtension.position C.targetPosition)

The first negative boundary letter is an ordinary arrow from the new position into the inherited old endpoint.

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.NegativeBoundaryExtension.toRightExtension_steps {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (extension : C.NegativeBoundaryExtension D) : extension.toRightExtension.steps = extension.tail.steps + 1

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.NegativeBoundaryExtension.toRightExtension_steps_transport_source {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C C' D : Word R} (h : C = C') (extension : C.NegativeBoundaryExtension D) : (⋯.mp extension).toRightExtension.steps = extension.toRightExtension.steps

Transporting the source word of a negative-boundary extension preserves its total step count.

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.NegativeBoundaryExtension.toRightExtension_suffixPath {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (extension : C.NegativeBoundaryExtension D) : extension.toRightExtension.suffixPath = (Quiver.Hom.toPath (negativeArrow extension.arrow)).comp extension.tail.suffixPath

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.NegativeBoundaryExtension.result_length {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (extension : C.NegativeBoundaryExtension D) : length R D = length R C + extension.tail.steps + 1

def MagnitudeConjecture.BoundQuiver.StringWord.Word.NegativeBoundaryExtension.transRightExtension {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D E : Word R} (extension : C.NegativeBoundaryExtension D) (further : D.RightExtension E) : C.NegativeBoundaryExtension E

Appending any further right extension preserves the marked negative boundary letter.

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.NegativeBoundaryExtension.toRightExtension_transRightExtension {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D E : Word R} (extension : C.NegativeBoundaryExtension D) (further : D.RightExtension E) : (extension.transRightExtension further).toRightExtension = extension.toRightExtension.trans further

structure MagnitudeConjecture.BoundQuiver.StringWord.Word.NegativeBoundaryExtension.RebaseResult {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (extension : C.NegativeBoundaryExtension D) {source : Q} (basePath : SignedPath source C.target) (hbase : IsString R basePath) : Type u

Replaying a negative-boundary extension after another certified base path, while retaining its distinguished first negative arrow.

• result : Word R
• rebased : (ofStringPath basePath hbase).NegativeBoundaryExtension self.result
• source_eq : self.result.source = source
• target_eq : self.result.target = D.target
• path_cast_eq : Quiver.Path.cast ⋯ ⋯ self.result.path = Quiver.Path.comp basePath extension.toRightExtension.suffixPath

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.NegativeBoundaryExtension.rebase {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (extension : C.NegativeBoundaryExtension D) {source : Q} (basePath : SignedPath source C.target) (hbase : IsString R basePath) (hfull : IsString R (Quiver.Path.comp basePath extension.toRightExtension.suffixPath)) : extension.RebaseResult basePath hbase

Construct the negative-boundary replay.

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.NegativeBoundaryExtension.rebase_steps {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (extension : C.NegativeBoundaryExtension D) {source : Q} (basePath : SignedPath source C.target) (hbase : IsString R basePath) (hfull : IsString R (Quiver.Path.comp basePath extension.toRightExtension.suffixPath)) : (extension.rebase basePath hbase hfull).rebased.toRightExtension.steps = extension.toRightExtension.steps

Replaying a negative-boundary extension preserves its total number of letters.

structure MagnitudeConjecture.BoundQuiver.StringWord.Word.PositiveBoundaryExtension {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C D : Word R) : Type u

A nonempty right extension whose first appended letter is positive. Its remaining tail may contain arbitrary signs.

• vertex : Q
• arrow : C.target ⟶ self.vertex
• valid : IsString R (Quiver.Path.comp C.path (Quiver.Hom.toPath (positiveArrow self.arrow)))
• tail : (append R C (positiveArrow self.arrow) ⋯).RightExtension D

def MagnitudeConjecture.BoundQuiver.StringWord.Word.PositiveBoundaryExtension.toRightExtension {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (extension : C.PositiveBoundaryExtension D) : C.RightExtension D

Forget the marked first positive letter.

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.PositiveBoundaryExtension.toRightExtension_position {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (extension : C.PositiveBoundaryExtension D) {x : Q} (i : C.PositionAt x) : extension.toRightExtension.position i = extension.tail.position (C.appendPosition (positiveArrow extension.arrow) ⋯ i)

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.PositiveBoundaryExtension.firstNewPosition {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (extension : C.PositiveBoundaryExtension D) : D.PositionAt extension.vertex

The first position created by a positive-boundary extension, retained through its arbitrary tail.

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.PositiveBoundaryExtension.firstNewPosition_index {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (extension : C.PositiveBoundaryExtension D) : extension.firstNewPosition.index = length R C + 1

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.PositiveBoundaryExtension.arrowStep_firstNewPosition {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (extension : C.PositiveBoundaryExtension D) : D.ArrowStep extension.arrow (extension.toRightExtension.position C.targetPosition) extension.firstNewPosition

The first positive boundary letter is an ordinary arrow from the inherited old endpoint to the new position.

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.PositiveBoundaryExtension.toRightExtension_steps {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (extension : C.PositiveBoundaryExtension D) : extension.toRightExtension.steps = extension.tail.steps + 1

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.PositiveBoundaryExtension.toRightExtension_steps_transport_source {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C C' D : Word R} (h : C = C') (extension : C.PositiveBoundaryExtension D) : (⋯.mp extension).toRightExtension.steps = extension.toRightExtension.steps

Transporting the source word of a positive-boundary extension preserves its total step count.

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.PositiveBoundaryExtension.toRightExtension_suffixPath {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (extension : C.PositiveBoundaryExtension D) : extension.toRightExtension.suffixPath = (Quiver.Hom.toPath (positiveArrow extension.arrow)).comp extension.tail.suffixPath

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.PositiveBoundaryExtension.result_length {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (extension : C.PositiveBoundaryExtension D) : length R D = length R C + extension.tail.steps + 1

def MagnitudeConjecture.BoundQuiver.StringWord.Word.PositiveBoundaryExtension.transRightExtension {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D E : Word R} (extension : C.PositiveBoundaryExtension D) (further : D.RightExtension E) : C.PositiveBoundaryExtension E

Appending any further right extension preserves the marked positive boundary letter.

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.PositiveBoundaryExtension.toRightExtension_transRightExtension {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D E : Word R} (extension : C.PositiveBoundaryExtension D) (further : D.RightExtension E) : (extension.transRightExtension further).toRightExtension = extension.toRightExtension.trans further

structure MagnitudeConjecture.BoundQuiver.StringWord.Word.PositiveBoundaryExtension.RebaseResult {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (extension : C.PositiveBoundaryExtension D) {source : Q} (basePath : SignedPath source C.target) (hbase : IsString R basePath) : Type u

Replaying a positive-boundary extension after another certified base path, while retaining its distinguished first positive arrow.

• result : Word R
• rebased : (ofStringPath basePath hbase).PositiveBoundaryExtension self.result
• source_eq : self.result.source = source
• target_eq : self.result.target = D.target
• path_cast_eq : Quiver.Path.cast ⋯ ⋯ self.result.path = Quiver.Path.comp basePath extension.toRightExtension.suffixPath

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.PositiveBoundaryExtension.rebase {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (extension : C.PositiveBoundaryExtension D) {source : Q} (basePath : SignedPath source C.target) (hbase : IsString R basePath) (hfull : IsString R (Quiver.Path.comp basePath extension.toRightExtension.suffixPath)) : extension.RebaseResult basePath hbase

Construct the positive-boundary replay. Validity of the complete replayed path supplies validity of the first arrow and every later tail prefix by contiguous-subpath heredity.

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.PositiveBoundaryExtension.rebase_steps {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (extension : C.PositiveBoundaryExtension D) {source : Q} (basePath : SignedPath source C.target) (hbase : IsString R basePath) (hfull : IsString R (Quiver.Path.comp basePath extension.toRightExtension.suffixPath)) : (extension.rebase basePath hbase hfull).rebased.toRightExtension.steps = extension.toRightExtension.steps

Replaying a positive-boundary extension preserves its total number of letters.