The winding mesh weight of a periodic component (Proposition 7.5)

weights-and-parameters.tex (prop:primitive-parameter-characters): "Lift p_i to ℤΔ, starting at a vertex (x, j) over τv_i. Its endpoint lies over v_i […] The closed walk p_i t_{v_i}⁻¹ winds once around the component."

Deviation: instead of identifying χ_i with a deck class and using a lemma on the periodic core, we construct, on a periodic component covered by ℤΔ with deck transformations (v, t) ↦ (ρ v, t + c₀), an integer mesh weight measuring this winding: an arrow lifted to X → Y gets weight ⌊Y_t / c₀⌋ − ⌊X_t / c₀⌋, which does not depend on the lift (floorWt). For the candidate row of a word of length c₀/2 + 1 (Appendix B) the weight of the row minus ν is one (floorWt_candRow).

def MultiplicativeBasisDeformations.StarTrace.fl {t : ℕ} {L : Fin t → ℕ} (c0 : ℕ) (X : (starTree L).ZVert) : ℤ

The winding level of a vertex of ℤΔ.

theorem MultiplicativeBasisDeformations.StarTrace.fl_gZ {t : ℕ} {L : Fin t → ℕ} (ρ : StarV L ≃ StarV L) (hρ : ∀ (a b : StarV L), (starTree L).G.Adj (ρ a) (ρ b) ↔ (starTree L).G.Adj a b) (c0 : ℕ) (hρp : ∀ (v : StarV L), (starTree L).par (ρ v) = (starTree L).par v + ↑↑c0) (hc0 : 0 < c0) (n : ℕ) (X : (starTree L).ZVert) : fl c0 ((StarGauge.gZ ρ hρ c0 hρp)^[n] X) = fl c0 X + ↑n

theorem MultiplicativeBasisDeformations.StarTrace.gZ_ztau {t : ℕ} {L : Fin t → ℕ} (ρ : StarV L ≃ StarV L) (hρ : ∀ (a b : StarV L), (starTree L).G.Adj (ρ a) (ρ b) ↔ (starTree L).G.Adj a b) (c0 : ℕ) (hρp : ∀ (v : StarV L), (starTree L).par (ρ v) = (starTree L).par v + ↑↑c0) (n : ℕ) (X : (starTree L).ZVert) : (StarGauge.gZ ρ hρ c0 hρp)^[n] ((starTree L).ztau X) = (starTree L).ztau ((StarGauge.gZ ρ hρ c0 hρp)^[n] X)

theorem MultiplicativeBasisDeformations.StarTrace.star_eq {V : Type} [Quiver V] [∀ (x y : V), Subsingleton (x ⟶ y)] {u a b : V} (ha : a = b) (e : u ⟶ a) (e' : u ⟶ b) : ⟨a, e⟩ = ⟨b, e'⟩

theorem MultiplicativeBasisDeformations.StarTrace.lift_eq_of_src {t : ℕ} {L : Fin t → ℕ} {V : Type} [Quiver V] [∀ (x y : V), Subsingleton (x ⟶ y)] (π : (starTree L).ZVert ⥤q V) (hπ : π.IsCovering) {X Y Y' : (starTree L).ZVert} (e : X ⟶ Y) (e' : X ⟶ Y') (h : π.obj Y = π.obj Y') : Y = Y'

Two lifts of an arrow with lifted sources over the same vertex.

theorem MultiplicativeBasisDeformations.StarTrace.π_gZ {t : ℕ} {L : Fin t → ℕ} {V : Type} [Quiver V] [∀ (x y : V), Subsingleton (x ⟶ y)] (π : (starTree L).ZVert ⥤q V) (ρ : StarV L ≃ StarV L) (hρ : ∀ (a b : StarV L), (starTree L).G.Adj (ρ a) (ρ b) ↔ (starTree L).G.Adj a b) (c0 : ℕ) (hρp : ∀ (v : StarV L), (starTree L).par (ρ v) = (starTree L).par v + ↑↑c0) (hdeck : ∀ (Z : (starTree L).ZVert), π.obj (((starTree L).zAct ρ hρ (↑c0) hρp).obj Z) = π.obj Z) (n : ℕ) (Z : (starTree L).ZVert) : π.obj ((StarGauge.gZ ρ hρ c0 hρp)^[n] Z) = π.obj Z

theorem MultiplicativeBasisDeformations.StarTrace.fl_arrow_aux {t : ℕ} {L : Fin t → ℕ} {V : Type} [Quiver V] [∀ (x y : V), Subsingleton (x ⟶ y)] (π : (starTree L).ZVert ⥤q V) (hπ : π.IsCovering) (ρ : StarV L ≃ StarV L) (hρ : ∀ (a b : StarV L), (starTree L).G.Adj (ρ a) (ρ b) ↔ (starTree L).G.Adj a b) (c0 : ℕ) (hρp : ∀ (v : StarV L), (starTree L).par (ρ v) = (starTree L).par v + ↑↑c0) (hc0 : 0 < c0) (hdeck : ∀ (Z : (starTree L).ZVert), π.obj (((starTree L).zAct ρ hρ (↑c0) hρp).obj Z) = π.obj Z) (n : ℕ) {X Y Y' : (starTree L).ZVert} (e : X ⟶ Y) (e' : (StarGauge.gZ ρ hρ c0 hρp)^[n] X ⟶ Y') (hY : π.obj Y = π.obj Y') : fl c0 Y - fl c0 X = fl c0 Y' - fl c0 ((StarGauge.gZ ρ hρ c0 hρp)^[n] X)

theorem MultiplicativeBasisDeformations.StarTrace.fl_arrow {t : ℕ} {L : Fin t → ℕ} {V : Type} [Quiver V] [∀ (x y : V), Subsingleton (x ⟶ y)] (π : (starTree L).ZVert ⥤q V) (hπ : π.IsCovering) (ρ : StarV L ≃ StarV L) (hρ : ∀ (a b : StarV L), (starTree L).G.Adj (ρ a) (ρ b) ↔ (starTree L).G.Adj a b) (c0 : ℕ) (hρp : ∀ (v : StarV L), (starTree L).par (ρ v) = (starTree L).par v + ↑↑c0) (hc0 : 0 < c0) (hdeck : ∀ (Z : (starTree L).ZVert), π.obj (((starTree L).zAct ρ hρ (↑c0) hρp).obj Z) = π.obj Z) (hfib : ∀ (X Y : (starTree L).ZVert), π.obj X = π.obj Y → ∃ (n : ℕ), Y = (StarGauge.gZ ρ hρ c0 hρp)^[n] X ∨ X = (StarGauge.gZ ρ hρ c0 hρp)^[n] Y) {X Y X' Y' : (starTree L).ZVert} (e : X ⟶ Y) (e' : X' ⟶ Y') (hX : π.obj X = π.obj X') (hY : π.obj Y = π.obj Y') : fl c0 Y - fl c0 X = fl c0 Y' - fl c0 X'

The winding increment of an arrow does not depend on its lift.

theorem MultiplicativeBasisDeformations.StarTrace.fl_tau {t : ℕ} {L : Fin t → ℕ} {V : Type} [Quiver V] [∀ (x y : V), Subsingleton (x ⟶ y)] (π : (starTree L).ZVert ⥤q V) (ρ : StarV L ≃ StarV L) (hρ : ∀ (a b : StarV L), (starTree L).G.Adj (ρ a) (ρ b) ↔ (starTree L).G.Adj a b) (c0 : ℕ) (hρp : ∀ (v : StarV L), (starTree L).par (ρ v) = (starTree L).par v + ↑↑c0) (hc0 : 0 < c0) (hdeck : ∀ (Z : (starTree L).ZVert), π.obj (((starTree L).zAct ρ hρ (↑c0) hρp).obj Z) = π.obj Z) (hfib : ∀ (X Y : (starTree L).ZVert), π.obj X = π.obj Y → ∃ (n : ℕ), Y = (StarGauge.gZ ρ hρ c0 hρp)^[n] X ∨ X = (StarGauge.gZ ρ hρ c0 hρp)^[n] Y) {X X' : (starTree L).ZVert} (hX : π.obj X = π.obj X') : fl c0 X - fl c0 ((starTree L).ztau X) = fl c0 X' - fl c0 ((starTree L).ztau X')

theorem MultiplicativeBasisDeformations.StarTrace.exists_lift_to {t : ℕ} {L : Fin t → ℕ} {V : Type} [Quiver V] [∀ (x y : V), Subsingleton (x ⟶ y)] (π : (starTree L).ZVert ⥤q V) (hπ : π.IsCovering) {y x : V} (a : y ⟶ x) (X : (starTree L).ZVert) (hX : π.obj X = x) : ∃ (Y : (starTree L).ZVert) (x : Y ⟶ X), π.obj Y = y

theorem MultiplicativeBasisDeformations.StarTrace.exists_lift {t : ℕ} {L : Fin t → ℕ} {V : Type} [Quiver V] [∀ (x y : V), Subsingleton (x ⟶ y)] (π : (starTree L).ZVert ⥤q V) (hπ : π.IsCovering) (hsurj : ∀ (x : V), ∃ (X : (starTree L).ZVert), π.obj X = x) {y x : V} (a : y ⟶ x) : ∃ (X : (starTree L).ZVert) (Y : (starTree L).ZVert) (x_1 : X ⟶ Y), π.obj X = y ∧ π.obj Y = x

theorem MultiplicativeBasisDeformations.StarTrace.w_def_eq {t : ℕ} {L : Fin t → ℕ} {V : Type} [Quiver V] [∀ (x y : V), Subsingleton (x ⟶ y)] (π : (starTree L).ZVert ⥤q V) (hπ : π.IsCovering) (hsurj : ∀ (x : V), ∃ (X : (starTree L).ZVert), π.obj X = x) (ρ : StarV L ≃ StarV L) (hρ : ∀ (a b : StarV L), (starTree L).G.Adj (ρ a) (ρ b) ↔ (starTree L).G.Adj a b) (c0 : ℕ) (hρp : ∀ (v : StarV L), (starTree L).par (ρ v) = (starTree L).par v + ↑↑c0) (hc0 : 0 < c0) (hdeck : ∀ (Z : (starTree L).ZVert), π.obj (((starTree L).zAct ρ hρ (↑c0) hρp).obj Z) = π.obj Z) (hfib : ∀ (X Y : (starTree L).ZVert), π.obj X = π.obj Y → ∃ (n : ℕ), Y = (StarGauge.gZ ρ hρ c0 hρp)^[n] X ∨ X = (StarGauge.gZ ρ hρ c0 hρp)^[n] Y) {y x : V} (a : y ⟶ x) {X Y : (starTree L).ZVert} (e : X ⟶ Y) (hX : π.obj X = y) (hY : π.obj Y = x) : fl c0 (Classical.choose ⋯) - fl c0 (Classical.choose ⋯) = fl c0 Y - fl c0 X

theorem MultiplicativeBasisDeformations.StarTrace.ν_def_eq {t : ℕ} {L : Fin t → ℕ} {V : Type} [Quiver V] [∀ (x y : V), Subsingleton (x ⟶ y)] (π : (starTree L).ZVert ⥤q V) (hsurj : ∀ (x : V), ∃ (X : (starTree L).ZVert), π.obj X = x) (ρ : StarV L ≃ StarV L) (hρ : ∀ (a b : StarV L), (starTree L).G.Adj (ρ a) (ρ b) ↔ (starTree L).G.Adj a b) (c0 : ℕ) (hρp : ∀ (v : StarV L), (starTree L).par (ρ v) = (starTree L).par v + ↑↑c0) (hc0 : 0 < c0) (hdeck : ∀ (Z : (starTree L).ZVert), π.obj (((starTree L).zAct ρ hρ (↑c0) hρp).obj Z) = π.obj Z) (hfib : ∀ (X Y : (starTree L).ZVert), π.obj X = π.obj Y → ∃ (n : ℕ), Y = (StarGauge.gZ ρ hρ c0 hρp)^[n] X ∨ X = (StarGauge.gZ ρ hρ c0 hρp)^[n] Y) (x : V) {X : (starTree L).ZVert} (hX : π.obj X = x) : fl c0 (Classical.choose ⋯) - fl c0 ((starTree L).ztau (Classical.choose ⋯)) = fl c0 X - fl c0 ((starTree L).ztau X)

noncomputable def MultiplicativeBasisDeformations.StarTrace.floorWt {t : ℕ} {L : Fin t → ℕ} {V : Type} [Quiver V] [∀ (x y : V), Subsingleton (x ⟶ y)] {Q : TranslationQuiver V} (hQ : Q.IsStable) (π : (starTree L).ZVert ⥤q V) (hπ : π.IsCovering) (hτ : ∀ (Y : (starTree L).ZVert), π.obj ((starTree L).ztau Y) = hQ.tauE (π.obj Y)) (hsurj : ∀ (x : V), ∃ (X : (starTree L).ZVert), π.obj X = x) (ρ : StarV L ≃ StarV L) (hρ : ∀ (a b : StarV L), (starTree L).G.Adj (ρ a) (ρ b) ↔ (starTree L).G.Adj a b) (c0 : ℕ) (hρp : ∀ (v : StarV L), (starTree L).par (ρ v) = (starTree L).par v + ↑↑c0) (hc0 : 0 < c0) (hdeck : ∀ (Z : (starTree L).ZVert), π.obj (((starTree L).zAct ρ hρ (↑c0) hρp).obj Z) = π.obj Z) (hfib : ∀ (X Y : (starTree L).ZVert), π.obj X = π.obj Y → ∃ (n : ℕ), Y = (StarGauge.gZ ρ hρ c0 hρp)^[n] X ∨ X = (StarGauge.gZ ρ hρ c0 hρp)^[n] Y) : MeshWalk.MeshWt Q ℤ

The winding mesh weight.

theorem MultiplicativeBasisDeformations.StarTrace.floorWt_w {t : ℕ} {L : Fin t → ℕ} {V : Type} [Quiver V] [∀ (x y : V), Subsingleton (x ⟶ y)] {Q : TranslationQuiver V} (hQ : Q.IsStable) (π : (starTree L).ZVert ⥤q V) (hπ : π.IsCovering) (hτ : ∀ (Y : (starTree L).ZVert), π.obj ((starTree L).ztau Y) = hQ.tauE (π.obj Y)) (hsurj : ∀ (x : V), ∃ (X : (starTree L).ZVert), π.obj X = x) (ρ : StarV L ≃ StarV L) (hρ : ∀ (a b : StarV L), (starTree L).G.Adj (ρ a) (ρ b) ↔ (starTree L).G.Adj a b) (c0 : ℕ) (hρp : ∀ (v : StarV L), (starTree L).par (ρ v) = (starTree L).par v + ↑↑c0) (hc0 : 0 < c0) (hdeck : ∀ (Z : (starTree L).ZVert), π.obj (((starTree L).zAct ρ hρ (↑c0) hρp).obj Z) = π.obj Z) (hfib : ∀ (X Y : (starTree L).ZVert), π.obj X = π.obj Y → ∃ (n : ℕ), Y = (StarGauge.gZ ρ hρ c0 hρp)^[n] X ∨ X = (StarGauge.gZ ρ hρ c0 hρp)^[n] Y) {y x : V} (a : y ⟶ x) {X Y : (starTree L).ZVert} (e : X ⟶ Y) (hX : π.obj X = y) (hY : π.obj Y = x) : (floorWt hQ π hπ hτ hsurj ρ hρ c0 hρp hc0 hdeck hfib).w a = fl c0 Y - fl c0 X

theorem MultiplicativeBasisDeformations.StarTrace.floorWt_pw {t : ℕ} {L : Fin t → ℕ} {V : Type} [Quiver V] [∀ (x y : V), Subsingleton (x ⟶ y)] {Q : TranslationQuiver V} (hQ : Q.IsStable) (π : (starTree L).ZVert ⥤q V) (hπ : π.IsCovering) (hτ : ∀ (Y : (starTree L).ZVert), π.obj ((starTree L).ztau Y) = hQ.tauE (π.obj Y)) (hsurj : ∀ (x : V), ∃ (X : (starTree L).ZVert), π.obj X = x) (ρ : StarV L ≃ StarV L) (hρ : ∀ (a b : StarV L), (starTree L).G.Adj (ρ a) (ρ b) ↔ (starTree L).G.Adj a b) (c0 : ℕ) (hρp : ∀ (v : StarV L), (starTree L).par (ρ v) = (starTree L).par v + ↑↑c0) (hc0 : 0 < c0) (hdeck : ∀ (Z : (starTree L).ZVert), π.obj (((starTree L).zAct ρ hρ (↑c0) hρp).obj Z) = π.obj Z) (hfib : ∀ (X Y : (starTree L).ZVert), π.obj X = π.obj Y → ∃ (n : ℕ), Y = (StarGauge.gZ ρ hρ c0 hρp)^[n] X ∨ X = (StarGauge.gZ ρ hρ c0 hρp)^[n] Y) {X Z : (starTree L).ZVert} (P : Quiver.Path X Z) : (floorWt hQ π hπ hτ hsurj ρ hρ c0 hρp hc0 hdeck hfib).pw (π.mapPath P) = fl c0 Z - fl c0 X

theorem MultiplicativeBasisDeformations.StarTrace.floorWt_ν {t : ℕ} {L : Fin t → ℕ} {V : Type} [Quiver V] [∀ (x y : V), Subsingleton (x ⟶ y)] {Q : TranslationQuiver V} (hQ : Q.IsStable) (π : (starTree L).ZVert ⥤q V) (hπ : π.IsCovering) (hτ : ∀ (Y : (starTree L).ZVert), π.obj ((starTree L).ztau Y) = hQ.tauE (π.obj Y)) (hsurj : ∀ (x : V), ∃ (X : (starTree L).ZVert), π.obj X = x) (ρ : StarV L ≃ StarV L) (hρ : ∀ (a b : StarV L), (starTree L).G.Adj (ρ a) (ρ b) ↔ (starTree L).G.Adj a b) (c0 : ℕ) (hρp : ∀ (v : StarV L), (starTree L).par (ρ v) = (starTree L).par v + ↑↑c0) (hc0 : 0 < c0) (hdeck : ∀ (Z : (starTree L).ZVert), π.obj (((starTree L).zAct ρ hρ (↑c0) hρp).obj Z) = π.obj Z) (hfib : ∀ (X Y : (starTree L).ZVert), π.obj X = π.obj Y → ∃ (n : ℕ), Y = (StarGauge.gZ ρ hρ c0 hρp)^[n] X ∨ X = (StarGauge.gZ ρ hρ c0 hρp)^[n] Y) (x : ↑Q.nonprojective) {X : (starTree L).ZVert} (hX : π.obj X = ↑x) : (floorWt hQ π hπ hτ hsurj ρ hρ c0 hρp hc0 hdeck hfib).ν x = fl c0 X - fl c0 ((starTree L).ztau X)

theorem MultiplicativeBasisDeformations.StarTrace.MeshWt_pw_cast {V : Type} [Quiver V] [∀ (x y : V), Subsingleton (x ⟶ y)] {Q : TranslationQuiver V} {M : Type} [AddCommGroup M] (W : MeshWalk.MeshWt Q M) {y x y' x' : V} (p : Quiver.Path y x) (h1 : y = y') (h2 : x = x') : W.pw (Quiver.Path.cast h1 h2 p) = W.pw p

theorem MultiplicativeBasisDeformations.StarTrace.floorWt_candRow {t : ℕ} {L : Fin t → ℕ} {V : Type} [Quiver V] [∀ (x y : V), Subsingleton (x ⟶ y)] {Q : TranslationQuiver V} (hQ : Q.IsStable) (π : (starTree L).ZVert ⥤q V) (hπ : π.IsCovering) (hτ : ∀ (Y : (starTree L).ZVert), π.obj ((starTree L).ztau Y) = hQ.tauE (π.obj Y)) (hsurj : ∀ (x : V), ∃ (X : (starTree L).ZVert), π.obj X = x) (ρ : StarV L ≃ StarV L) (hρ : ∀ (a b : StarV L), (starTree L).G.Adj (ρ a) (ρ b) ↔ (starTree L).G.Adj a b) (c0 : ℕ) (hρp : ∀ (v : StarV L), (starTree L).par (ρ v) = (starTree L).par v + ↑↑c0) (hc0 : 0 < c0) (hdeck : ∀ (Z : (starTree L).ZVert), π.obj (((starTree L).zAct ρ hρ (↑c0) hρp).obj Z) = π.obj Z) (hfib : ∀ (X Y : (starTree L).ZVert), π.obj X = π.obj Y → ∃ (n : ℕ), Y = (StarGauge.gZ ρ hρ c0 hρp)^[n] X ∨ X = (StarGauge.gZ ρ hρ c0 hρp)^[n] Y) (hc0e : Even c0) (W₀ : List (Fin t)) (hW : W₀.length = c0 / 2 + 1) (R : (x : ↑Q.nonprojective) × Quiver.Path ↑(Q.tau x) ↑x) : R ∈ candRow hQ π W₀ → (floorWt hQ π hπ hτ hsurj ρ hρ c0 hρp hc0 hdeck hfib).pw R.snd - (floorWt hQ π hπ hτ hsurj ρ hρ c0 hρp hc0 hdeck hfib).ν R.fst = 1

The candidate row winds once.