Sign-preserving replay of hook and cohook arms

The boundary-square constructions replay endpoint suffixes after replacing the prefix word. The generic right-extension replay forgets that a hook tail is entirely negative or that a cohook tail is entirely positive. This file retains those signs; the resulting data can therefore be repackaged as literal maximal hooks and cohooks.

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

Replay a negative arm after a different certified prefix while retaining the fact that every replayed letter is negative.

• result : Word R
• rebased : (ofStringPath basePath hbase).NegativeExtension 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 arm.toRightExtension.suffixPath

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

Construct the sign-preserving replay of a negative arm.

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

Replay a positive arm after a different certified prefix while retaining the fact that every replayed letter is positive.

• result : Word R
• rebased : (ofStringPath basePath hbase).PositiveExtension 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 arm.toRightExtension.suffixPath

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

Construct the sign-preserving replay of a positive arm.

@[simp]

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

@[simp]

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

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.HookExtension.rebasedPath_startsInDeep {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (hook : C.HookExtension D) {source : Q} (basePath : SignedPath source C.target) (hfull : IsString R (Quiver.Path.comp basePath hook.toPositiveBoundaryExtension.toRightExtension.suffixPath)) : (ofStringPath (Quiver.Path.comp basePath hook.toPositiveBoundaryExtension.toRightExtension.suffixPath) hfull).StartsInDeep

Replacing the prefix before a complete hook suffix does not destroy the deep at the hook endpoint. The initial positive hook arrow is a negative barrier after reversal, so a newly appended negative arrow would also extend the original hook result.

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

The result of replaying a complete hook after another certified prefix.

• result : Word R
• rebased : (ofStringPath basePath hbase).HookExtension 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 hook.toPositiveBoundaryExtension.toRightExtension.suffixPath

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

Replay a complete hook, retaining both the negative tail and endpoint maximality.

@[simp]

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

Replaying a hook preserves its total number of letters.

@[simp]

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

@[simp]

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

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.CohookExtension.rebasedPath_startsOnPeak {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (cohook : C.CohookExtension D) {source : Q} (basePath : SignedPath source C.target) (hfull : IsString R (Quiver.Path.comp basePath cohook.toNegativeBoundaryExtension.toRightExtension.suffixPath)) : (ofStringPath (Quiver.Path.comp basePath cohook.toNegativeBoundaryExtension.toRightExtension.suffixPath) hfull).StartsOnPeak

Replacing the prefix before a complete cohook suffix does not destroy the peak at the cohook endpoint. The initial negative cohook arrow blocks forward relations, while a newly appended positive arrow becomes a negative outer boundary after reversal.

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

The result of replaying a complete cohook after another certified prefix.

• result : Word R
• rebased : (ofStringPath basePath hbase).CohookExtension 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 cohook.toNegativeBoundaryExtension.toRightExtension.suffixPath

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

Replay a complete cohook, retaining both the positive tail and endpoint maximality.

@[simp]

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

Replaying a cohook preserves its total number of letters.