The finite order on endpoint-polarized detector words

Route signs read a word from its fixed target toward its source. The order places a positive child below its parent, its parent below an inverse child, and compares two branches at their first differing sign. Ringel's word subspace inclusions then show that distinct detector intervals avoid one another.

def MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.routeOrderDigit (b : Bool) : Fin 3

The three-valued digit used to realize the in-order route comparison as an ordinary lexicographic order: positive is below the terminal marker and inverse is above it.

theorem MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.routeOrderDigit_injective : Function.Injective routeOrderDigit

def MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.routeOrderKey {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] {P : SpecialBiserialPresentation k A Q} {S : P.ArrowPolarization} {u : Q} {t : Bool} (C : EndpointWord S u t) : List (Fin 3)

A lexicographic key for the in-order source-extension comparison.

theorem MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.routeOrderKey_injective {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] {P : SpecialBiserialPresentation k A Q} {S : P.ArrowPolarization} {u : Q} {t : Bool} : Function.Injective routeOrderKey

@[instance_reducible]

noncomputable instance MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.endpointWordLinearOrder {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] {P : SpecialBiserialPresentation k A Q} {S : P.ArrowPolarization} {u : Q} {t : Bool} : LinearOrder (EndpointWord S u t)

The canonical finite-word order is the ordinary lexicographic order on the three-valued route key.

def MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.RouteLT (a b : List Bool) : Prop

In-order comparison of two routes in the source-extension tree. A positive descendant is below its ancestor, an inverse descendant is above its ancestor, and a positive branch is below an inverse branch at their first split.

theorem MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.RouteLT.cons {a b : List Bool} (head : Bool) (h : RouteLT a b) : RouteLT (head :: a) (head :: b)

Prefixing the same route sign preserves the in-order comparison.

theorem MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.routeOrderKey_lt_of_routeLT {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] {P : SpecialBiserialPresentation k A Q} {S : P.ArrowPolarization} {u : Q} {t : Bool} {C D : EndpointWord S u t} (h : RouteLT C.routeSigns D.routeSigns) : C.routeOrderKey < D.routeOrderKey

The recursive route comparison implies lexicographic comparison of the three-valued route keys.

theorem MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.route_eq_or_routeLT_or_routeLT (a b : List Bool) : a = b ∨ RouteLT a b ∨ RouteLT b a

Any two Boolean routes are equal or comparable in exactly one of the two in-order directions.

def MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.WordLT {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] {P : SpecialBiserialPresentation k A Q} {S : P.ArrowPolarization} {u : Q} {t : Bool} (C D : EndpointWord S u t) : Prop

The strict order on endpoint words induced by their route signs.

theorem MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.eq_or_wordLT_or_wordLT {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] {P : SpecialBiserialPresentation k A Q} {S : P.ArrowPolarization} {u : Q} {t : Bool} (C D : EndpointWord S u t) : C = D ∨ C.WordLT D ∨ D.WordLT C

Fixed-endpoint words are equal or comparable in the two word-order directions.

theorem MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.wordLT_iff_lt {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] {P : SpecialBiserialPresentation k A Q} {S : P.ArrowPolarization} {u : Q} {t : Bool} (C D : EndpointWord S u t) : C.WordLT D ↔ C < D

The explicit recursive word comparison is the strict canonical order.

theorem MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.upperSubspace_le_lowerSubspace_of_wordLT {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] {P : SpecialBiserialPresentation k A Q} {S : P.ArrowPolarization} {u : Q} {t : Bool} (N : CategoryTheory.Functor (Category P.relations)ᵒᵖ (ModuleCat k)) [N.Additive] (C D : EndpointWord S u t) (h : C.WordLT D) : upperSubspace N C ≤ lowerSubspace N D

Ringel's word-order implication: if C < D, then the upper endpoint of the interval of C lies below the lower endpoint of the interval of D.

theorem MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.eq_or_intervals_avoid {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] {P : SpecialBiserialPresentation k A Q} {S : P.ArrowPolarization} {u : Q} {t : Bool} (N : CategoryTheory.Functor (Category P.relations)ᵒᵖ (ModuleCat k)) [N.Additive] (C D : EndpointWord S u t) : C = D ∨ upperSubspace N C ≤ lowerSubspace N D ∨ upperSubspace N D ≤ lowerSubspace N C

Distinct fixed-endpoint word intervals avoid one another.