Repeated middle words for the positive hook square

The finite detector classification reduces an isomorphism between the two middle string modules to literal equality or reversal. In the reversal branch, cancellation of equally long hook prefixes shows that the original word has length zero.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.length_eq_zero_of_leftHook_result_eq_reverse_rightHook_result {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C rightResult : Word R} (right : C.HookExtension rightResult) (left : C.LeftHookExtension) (hmiddle : left.result = reverse R rightResult) : length R C = 0

If the left-hook result is the reverse of the right-hook result, then the base string has length zero.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.leftHook_result_ne_reverse_rightHook_result_of_twoHookPath_isString {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C rightResult : Word R} (right : C.HookExtension rightResult) (left : C.LeftHookExtension) (hpath : IsString R (twoHookPath right left)) : left.result ≠ reverse R rightResult

A valid two-hook corner rules out the reversal branch altogether: in the only possible length-zero case, equality of the reversed middle words forces the two central boundary letters to cancel.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.leftHook_result_eq_or_base_length_eq_zero_of_finiteRightModule_iso {k Q : Type u} [Field k] [Quiver Q] {A : Type u} [Ring A] [Algebra k A] [Fintype Q] [(x y : Q) → Fintype (x ⟶ y)] {P : StringPresentation k A Q} (S : P.ArrowPolarization) {C rightResult : Word P.relations} (right : C.HookExtension rightResult) (left : C.LeftHookExtension) (e : left.result.finiteRightModule ⋯ ≅ rightResult.finiteRightModule ⋯) : left.result = rightResult ∨ length P.relations C = 0

Isomorphic positive-hook middle modules have either literally equal middle words or a length-zero base word. Thus reversal is confined to the single convention-sensitive edge case.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.leftHook_result_eq_of_finiteRightModule_iso_of_twoHookPath_isString {k Q : Type u} [Field k] [Quiver Q] {A : Type u} [Ring A] [Algebra k A] [Fintype Q] [(x y : Q) → Fintype (x ⟶ y)] {P : StringPresentation k A Q} (S : P.ArrowPolarization) {C rightResult : Word P.relations} (right : C.HookExtension rightResult) (left : C.LeftHookExtension) (hpath : IsString P.relations (twoHookPath right left)) (e : left.result.finiteRightModule ⋯ ≅ rightResult.finiteRightModule ⋯) : left.result = rightResult

For a valid positive two-hook square, isomorphism of the two middle modules forces literal equality of their words. The detector classification gives equality or reversal, and reducedness excludes reversal.