Transporting the distinguished basis vector along its own string

The self-evaluation of a Butler--Ringel detector rests on one elementary calculation: starting with the source-position basis vector of a literal string module and transporting its span along any prefix of the same word reaches the basis vector at the end of that prefix. Positive letters use the displayed-arrow image; inverse letters use its preimage.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.not_exists_arrowStep_sourcePosition_of_prepend_negative_isString {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (D : Word R) {y : Q} (a : D.source ⟶ y) (hstring : IsString R ((Quiver.Hom.toPath (negativeArrow a)).comp D.path)) : ¬∃ (j : D.PositionAt y), D.ArrowStep a D.sourcePosition j

If the inverse of an outgoing arrow can be prefixed to a string, that arrow kills the string module's source-position basis vector.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.arrowLinearMap_sourceBasis_eq_zero_of_prepend_negative_isString {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (D : Word R) {y : Q} (a : D.source ⟶ y) (hstring : IsString R ((Quiver.Hom.toPath (negativeArrow a)).comp D.path)) : (D.arrowLinearMap a) (Finsupp.single D.sourcePosition 1) = 0

Concrete arrow-map form of the preceding no-step statement.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.not_exists_arrowStep_to_sourcePosition_of_prepend_positive_isString {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (D : Word R) {x : Q} (a : x ⟶ D.source) (hstring : IsString R ((Quiver.Hom.toPath (positiveArrow a)).comp D.path)) : ¬∃ (i : D.PositionAt x), D.ArrowStep a i D.sourcePosition

If an incoming arrow can be prefixed positively to a string, no position of the string maps to its source-position coordinate along that arrow.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.arrowLinearMap_apply_sourcePosition_eq_zero_of_prepend_positive_isString {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (D : Word R) {x : Q} (a : x ⟶ D.source) (v : D.Space x) (hstring : IsString R ((Quiver.Hom.toPath (positiveArrow a)).comp D.path)) : ((D.arrowLinearMap a) v) D.sourcePosition = 0

Every image along such an incoming arrow has zero source-position coefficient.

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.moduleArrowMap_rightModule {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (D : Word R) (hmono : IsMonomial R) {x y : Q} (a : x ⟶ y) : moduleArrowMap (D.rightModule hmono) a = ModuleCat.ofHom (D.arrowLinearMap a)

On a literal string module, the general displayed-arrow map is its position-basis arrow map.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.prefixBasis_mem_signedPathSubspace_span_source {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (D : Word R) (hmono : IsMonomial R) {x : Q} (p : SignedPath D.source x) (q : SignedPath x D.target) (hp : D.path = Quiver.Path.comp p q) : Finsupp.single ⟨p, ⋯⟩ 1 ∈ signedPathSubspace (D.rightModule hmono) p (k ∙ Finsupp.single D.sourcePosition 1)

The distinguished basis vector at the end of a prefix belongs to the transport, along that prefix, of the source-position line.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.targetBasis_mem_signedPathSubspace_span_source {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (D : Word R) (hmono : IsMonomial R) : Finsupp.single D.targetPosition 1 ∈ signedPathSubspace (D.rightModule hmono) D.path (k ∙ Finsupp.single D.sourcePosition 1)

In particular, transporting the source-position line along the complete word reaches the target-position basis vector.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.signedPathSubspace_apply_prefixPosition_eq_zero {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (D : Word R) (hmono : IsMonomial R) {x : Q} (p : SignedPath D.source x) (q : SignedPath x D.target) (hp : D.path = Quiver.Path.comp p q) (U : Submodule k (D.Space D.source)) (_hU : ∀ v ∈ U, v D.sourcePosition = 0) (v : D.Space x) : v ∈ signedPathSubspace (D.rightModule hmono) p U → v ⟨p, ⋯⟩ = 0

Vanishing of the distinguished coordinate propagates along every prefix of the literal string through the detector's direct-image/preimage transport.

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.signedPathTargetSign_comp_toPath {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} {x y z : Q} (p : SignedPath x y) (e : SignedArrow y z) : signedPathTargetSign S (Quiver.Path.comp p (Quiver.Hom.toPath e)) = some (signedArrowTargetSign S e)

theorem MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.sourceBasis_mem_upperBoundarySubspace_rightModule {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} {u₀ : Q} {t : Bool} (C : EndpointWord S u₀ t) : Finsupp.single C.word.sourcePosition 1 ∈ upperBoundarySubspace (C.word.rightModule ⋯) C

The source-position basis vector of an endpoint word lies in its own upper boundary filter.

theorem MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.targetBasis_mem_upperSubspace_rightModule {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} {u₀ : Q} {t : Bool} (C : EndpointWord S u₀ t) : Finsupp.single C.word.targetPosition 1 ∈ upperSubspace (C.word.rightModule ⋯) C

Transporting the upper boundary filter of an endpoint word through its own literal module contains the target-position basis vector.

theorem MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.lowerBoundarySubspace_apply_sourcePosition_eq_zero_rightModule {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} {u₀ : Q} {t : Bool} (C : EndpointWord S u₀ t) (v : C.word.Space C.word.source) (hv : v ∈ lowerBoundarySubspace (C.word.rightModule ⋯) C) : v C.word.sourcePosition = 0

Every vector in the lower boundary filter of a literal word has zero source-position coefficient.

theorem MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.lowerSubspace_apply_targetPosition_eq_zero_rightModule {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} {u₀ : Q} {t : Bool} (C : EndpointWord S u₀ t) (v : C.word.Space u₀) (hv : v ∈ lowerSubspace (C.word.rightModule ⋯) C) : v C.word.targetPosition = 0

Target-coordinate evaluation vanishes on the complete lower subspace C^- of a literal word evaluated on itself.

theorem MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.not_exists_arrowStep_to_targetPosition_of_targetSign_ne {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} {u₀ : Q} {t : Bool} (C : EndpointWord S u₀ t) {x : Q} (a : x ⟶ u₀) (hne : S.targetSign a ≠ t) : ¬∃ (i : C.word.PositionAt x), C.word.ArrowStep a i C.word.targetPosition

An incoming arrow whose target sign differs from an endpoint word's target sign cannot hit the word's target-position coordinate.

theorem MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.arrowLinearMap_apply_targetPosition_eq_zero_of_targetSign_ne {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} {u₀ : Q} {t : Bool} (C : EndpointWord S u₀ t) {x : Q} (a : x ⟶ u₀) (v : C.word.Space x) (hne : S.targetSign a ≠ t) : ((C.word.arrowLinearMap a) v) C.word.targetPosition = 0

Every image along such an incoming arrow has zero target-position coefficient.

theorem MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.not_exists_arrowStep_targetPosition_of_sourceSign_ne {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} {u₀ : Q} {t : Bool} (C : EndpointWord S u₀ t) {y : Q} (a : u₀ ⟶ y) (hne : S.sourceSign a ≠ t) : ¬∃ (j : C.word.PositionAt y), C.word.ArrowStep a C.word.targetPosition j

An outgoing arrow whose source sign differs from an endpoint word's target sign cannot leave the word's target-position basis vector.

theorem MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.arrowLinearMap_targetBasis_eq_zero_of_sourceSign_ne {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} {u₀ : Q} {t : Bool} (C : EndpointWord S u₀ t) {y : Q} (a : u₀ ⟶ y) (hne : S.sourceSign a ≠ t) : (C.word.arrowLinearMap a) (Finsupp.single C.word.targetPosition 1) = 0

Concrete arrow-map form of target-sign exclusion.

theorem MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.targetBasis_mem_upperBoundarySubspace_oppositeVertex_rightModule {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} {u₀ : Q} {t : Bool} (C : EndpointWord S u₀ t) : Finsupp.single C.word.targetPosition 1 ∈ upperBoundarySubspace (C.word.rightModule ⋯) C.oppositeVertex

The target-position basis vector lies in the upper boundary filter of the oppositely polarized trivial word used by the detector.

theorem MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.lowerBoundarySubspace_oppositeVertex_apply_targetPosition_eq_zero_rightModule {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} {u₀ : Q} {t : Bool} (C : EndpointWord S u₀ t) (v : C.word.Space u₀) (hv : v ∈ lowerBoundarySubspace (C.word.rightModule ⋯) C.oppositeVertex) : v C.word.targetPosition = 0

Target-coordinate evaluation vanishes on the lower boundary filter of the oppositely polarized trivial word.

theorem MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.lowerSubspace_oppositeVertex_apply_targetPosition_eq_zero_rightModule {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} {u₀ : Q} {t : Bool} (C : EndpointWord S u₀ t) (v : C.word.Space u₀) (hv : v ∈ lowerSubspace (C.word.rightModule ⋯) C.oppositeVertex) : v C.word.targetPosition = 0

Since the opposite trivial word has empty path, its complete lower subspace also has zero target coordinate.

theorem MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.targetBasis_mem_upperSubspace_oppositeVertex_rightModule {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} {u₀ : Q} {t : Bool} (C : EndpointWord S u₀ t) : Finsupp.single C.word.targetPosition 1 ∈ upperSubspace (C.word.rightModule ⋯) C.oppositeVertex

The same target vector lies in the complete upper subspace of the opposite trivial word; its signed path is empty.

theorem MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.targetBasis_mem_detectorNumerator_rightModule {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} {u₀ : Q} {t : Bool} (C : EndpointWord S u₀ t) : Finsupp.single C.word.targetPosition 1 ∈ detectorNumerator (C.word.rightModule ⋯) C

The target-position basis vector is a concrete element of the matching detector numerator 1^+ ∩ C^+.

theorem MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.detectorDenominator_apply_targetPosition_eq_zero_rightModule {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} {u₀ : Q} {t : Bool} (C : EndpointWord S u₀ t) (v : C.word.Space u₀) (hv : v ∈ detectorDenominator (C.word.rightModule ⋯) C) : v C.word.targetPosition = 0

Target-coordinate evaluation annihilates the complete matching detector denominator.

theorem MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.targetBasis_not_mem_detectorDenominator_rightModule {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} {u₀ : Q} {t : Bool} (C : EndpointWord S u₀ t) : Finsupp.single C.word.targetPosition 1 ∉ detectorDenominator (C.word.rightModule ⋯) C

The distinguished target basis vector is not in the matching detector denominator.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.targetNumeratorElement {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} {u₀ : Q} {t : Bool} (C : EndpointWord S u₀ t) : ↥(detectorNumerator (C.word.rightModule ⋯) C)

The distinguished numerator element represented by the target-position basis vector.

theorem MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.targetNumeratorElement_not_mem_denominatorInNumerator {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} {u₀ : Q} {t : Bool} (C : EndpointWord S u₀ t) : C.targetNumeratorElement ∉ detectorDenominatorInNumerator (C.word.rightModule ⋯) C

The distinguished numerator element does not lie in the denominator viewed as a submodule of the numerator.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.targetDetectorClass {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} {u₀ : Q} {t : Bool} (C : EndpointWord S u₀ t) : DetectorSpace (C.word.rightModule ⋯) C

The quotient class of the target-position basis vector in the matching detector.

theorem MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.targetDetectorClass_ne_zero {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} {u₀ : Q} {t : Bool} (C : EndpointWord S u₀ t) : C.targetDetectorClass ≠ 0

The matching detector takes a literal string module to a nonzero vector space: the target-position class survives its denominator.