The periodic gauge on a star model (Lemma A.1(1))

lem:periodic-scalar-gauges (1), periodic-mesh-calculations.tex, for Q = ℤΔ / ⟨g⟩ with Δ a star rooted at its centre, g (v, t) = (σ v, t + c₀) and σ fixing the centre and permuting the arms by θ.

The coefficients are recorded by Cf w w' h, the coefficient at (w, h + 2) of the arrow from (w', h + 1), invariant under g. The unknowns are the arrow scales M e h (the arrow over the edge with child endpoint e at source height h) and the relation scales N v h. On the representative arm of each θ-orbit the edges are treated down the arm (reps): the parent's relation scales are known, and exists_periodic_line_vertex gives the arrow scales and the child's relation scales, with period per · c₀. The other arms of the orbit are obtained by applying g.

def MultiplicativeBasisDeformations.StarGauge.pa {t : ℕ} {L : Fin t → ℕ} (i : Fin t) (j : ℕ) (h : j ≤ L i) : StarV L

The parent of the vertex j of arm i.

def MultiplicativeBasisDeformations.StarGauge.ch {t : ℕ} {L : Fin t → ℕ} (i : Fin t) (j : ℕ) (h : j ≤ L i) : StarV L

The vertex j of arm i.

def MultiplicativeBasisDeformations.StarGauge.lineS {k : Type u} [CommRing k] {t : ℕ} {L : Fin t → ℕ} (Cf : StarV L → StarV L → ℤ → kˣ) (sg : StarV L → StarV L → kˣ) (i : Fin t) (j : ℕ) (h : j ≤ L i) (Np : ℤ → kˣ) (s : ℤ) : kˣ

The prescribed products on the edge line with child ch i j, given the relation scales Np of the parent.

noncomputable def MultiplicativeBasisDeformations.StarGauge.step {k : Type u} [CommRing k] {t : ℕ} {L : Fin t → ℕ} (Cf : StarV L → StarV L → ℤ → kˣ) (sg : StarV L → StarV L → kˣ) (P : ℕ) (i : Fin t) (j : ℕ) (h : j ≤ L i) (Np : ℤ → kˣ) : (ℤ → kˣ) × (ℤ → kˣ)

One step down an arm: the child's relation scales and the edge's arrow scales.

theorem MultiplicativeBasisDeformations.StarGauge.step_spec {k : Type u} [CommRing k] {t : ℕ} {L : Fin t → ℕ} (Cf : StarV L → StarV L → ℤ → kˣ) (sg : StarV L → StarV L → kˣ) (P : ℕ) (i : Fin t) (j : ℕ) (h : j ≤ L i) (Np : ℤ → kˣ) (hP : 0 < P) (hPe : Even P) (hS : ∀ (s : ℤ), lineS Cf sg i j h Np (s + ↑P) = lineS Cf sg i j h Np s) : (∀ (s : ℤ), (step Cf sg P i j h Np).1 (s + ↑P) = (step Cf sg P i j h Np).1 s) ∧ (∀ (s : ℤ), (step Cf sg P i j h Np).2 (s + ↑P) = (step Cf sg P i j h Np).2 s) ∧ ∀ (s : ℤ), ((step Cf sg P i j h Np).2 s * (step Cf sg P i j h Np).2 (s + 1) * if ↑s = ↑(j + 1) then (step Cf sg P i j h Np).1 (s + 2) else 1) = lineS Cf sg i j h Np s

def MultiplicativeBasisDeformations.StarGauge.reps {k : Type u} [CommRing k] {t : ℕ} {L : Fin t → ℕ} (Cf : StarV L → StarV L → ℤ → kˣ) (sg : StarV L → StarV L → kˣ) (P : ℕ) (i : Fin t) : ℕ → (ℤ → kˣ) × (ℤ → kˣ)

The scales down a representative arm i₀.

theorem MultiplicativeBasisDeformations.StarGauge.reps_succ {k : Type u} [CommRing k] {t : ℕ} {L : Fin t → ℕ} (Cf : StarV L → StarV L → ℤ → kˣ) (sg : StarV L → StarV L → kˣ) (P : ℕ) (i : Fin t) (j : ℕ) (h : j + 1 ≤ L i) : reps Cf sg P i (j + 1) = step Cf sg P i (j + 1) h (reps Cf sg P i j).1

noncomputable def MultiplicativeBasisDeformations.StarGauge.parN {k : Type u} [CommRing k] {t : ℕ} {L : Fin t → ℕ} (Cf : StarV L → StarV L → ℤ → kˣ) (sg : StarV L → StarV L → kˣ) (P : ℕ) (i : Fin t) (j : ℕ) : ℤ → kˣ

The relation scales of the parent of the vertex j of the arm.

theorem MultiplicativeBasisDeformations.StarGauge.reps_eq_step {k : Type u} [CommRing k] {t : ℕ} {L : Fin t → ℕ} (Cf : StarV L → StarV L → ℤ → kˣ) (sg : StarV L → StarV L → kˣ) (P : ℕ) (i : Fin t) (j : ℕ) (h : j ≤ L i) : reps Cf sg P i j = step Cf sg P i j h (parN Cf sg P i j)

theorem MultiplicativeBasisDeformations.StarGauge.lineS_periodic {k : Type u} [CommRing k] {t : ℕ} {L : Fin t → ℕ} (Cf : StarV L → StarV L → ℤ → kˣ) (sg : StarV L → StarV L → kˣ) (P : ℕ) (hPe : Even P) (i : Fin t) (hper : ∀ (j : ℕ) (h : j ≤ L i) (s : ℤ), Cf (ch i j h) (pa i j h) (s + ↑P) = Cf (ch i j h) (pa i j h) s ∧ Cf (pa i j h) (ch i j h) (s + ↑P) = Cf (pa i j h) (ch i j h) s) (j : ℕ) (h : j ≤ L i) (Np : ℤ → kˣ) (hNp : ∀ (s : ℤ), Np (s + ↑P) = Np s) (s : ℤ) : lineS Cf sg i j h Np (s + ↑P) = lineS Cf sg i j h Np s

theorem MultiplicativeBasisDeformations.StarGauge.reps_spec {k : Type u} [CommRing k] {t : ℕ} {L : Fin t → ℕ} (Cf : StarV L → StarV L → ℤ → kˣ) (sg : StarV L → StarV L → kˣ) (P : ℕ) (hP : 0 < P) (hPe : Even P) (i : Fin t) (hper : ∀ (j : ℕ) (h : j ≤ L i) (s : ℤ), Cf (ch i j h) (pa i j h) (s + ↑P) = Cf (ch i j h) (pa i j h) s ∧ Cf (pa i j h) (ch i j h) (s + ↑P) = Cf (pa i j h) (ch i j h) s) (j : ℕ) (h : j ≤ L i) : (∀ (s : ℤ), (reps Cf sg P i j).1 (s + ↑P) = (reps Cf sg P i j).1 s) ∧ (∀ (s : ℤ), (reps Cf sg P i j).2 (s + ↑P) = (reps Cf sg P i j).2 s) ∧ ∀ (s : ℤ), ((reps Cf sg P i j).2 s * (reps Cf sg P i j).2 (s + 1) * if ↑s = ↑(j + 1) then (reps Cf sg P i j).1 (s + 2) else 1) = lineS Cf sg i j h (parN Cf sg P i j) s

The scales down a representative arm are P-periodic and solve the edge equations.

Transport along the orbit

theorem MultiplicativeBasisDeformations.StarGauge.ch_congr {t : ℕ} {L : Fin t → ℕ} {i i' : Fin t} (e : i = i') (j : ℕ) (h : j ≤ L i) (h' : j ≤ L i') : ch i j h = ch i' j h'

theorem MultiplicativeBasisDeformations.StarGauge.pa_congr {t : ℕ} {L : Fin t → ℕ} {i i' : Fin t} (e : i = i') (j : ℕ) (h : j ≤ L i) (h' : j ≤ L i') : pa i j h = pa i' j h'

theorem MultiplicativeBasisDeformations.StarGauge.L_pow {t : ℕ} {L : Fin t → ℕ} (θ : Equiv.Perm (Fin t)) (hL : ∀ (i : Fin t), L (θ i) = L i) (n : ℕ) (i : Fin t) : L ((θ ^ n) i) = L i

theorem MultiplicativeBasisDeformations.StarGauge.pow_ch {t : ℕ} {L : Fin t → ℕ} (θ : Equiv.Perm (Fin t)) (hL : ∀ (i : Fin t), L (θ i) = L i) (σ : StarV L ≃ StarV L) (hθ : ∀ (i : Fin t) (j : ℕ) (h : j ≤ L i), σ (ch i j h) = ch (θ i) j ⋯) (n : ℕ) (i : Fin t) (j : ℕ) (h : j ≤ L i) : (σ ^ n) (ch i j h) = ch ((θ ^ n) i) j ⋯

theorem MultiplicativeBasisDeformations.StarGauge.pow_pa {t : ℕ} {L : Fin t → ℕ} (θ : Equiv.Perm (Fin t)) (hL : ∀ (i : Fin t), L (θ i) = L i) (σ : StarV L ≃ StarV L) (hσo : σ none = none) (hθ : ∀ (i : Fin t) (j : ℕ) (h : j ≤ L i), σ (ch i j h) = ch (θ i) j ⋯) (n : ℕ) (i : Fin t) (j : ℕ) (h : j ≤ L i) : (σ ^ n) (pa i j h) = pa ((θ ^ n) i) j ⋯

theorem MultiplicativeBasisDeformations.StarGauge.Cf_pow {k : Type u} [CommRing k] {t : ℕ} {L : Fin t → ℕ} (Cf : StarV L → StarV L → ℤ → kˣ) (σ : StarV L ≃ StarV L) (c0 : ℕ) (hCinv : ∀ (w w' : StarV L) (s : ℤ), Cf (σ w) (σ w') (s + ↑c0) = Cf w w' s) (n : ℕ) (w w' : StarV L) (s : ℤ) : Cf ((σ ^ n) w) ((σ ^ n) w') (s + ↑n * ↑c0) = Cf w w' s

theorem MultiplicativeBasisDeformations.StarGauge.sg_pow {k : Type u} [CommRing k] {t : ℕ} {L : Fin t → ℕ} (sg : StarV L → StarV L → kˣ) (σ : StarV L ≃ StarV L) (hsg : ∀ (w w' : StarV L), sg (σ w) (σ w') = sg w w') (n : ℕ) (w w' : StarV L) : sg ((σ ^ n) w) ((σ ^ n) w') = sg w w'

noncomputable def MultiplicativeBasisDeformations.StarGauge.Pof {t : ℕ} (θ : Equiv.Perm (Fin t)) (c0 : ℕ) (i : Fin t) : ℕ

The period of the edge lines on the orbit of the arm i.

noncomputable def MultiplicativeBasisDeformations.StarGauge.Nf {k : Type u} [CommRing k] {t : ℕ} {L : Fin t → ℕ} (Cf : StarV L → StarV L → ℤ → kˣ) (sg : StarV L → StarV L → kˣ) (θ : Equiv.Perm (Fin t)) (c0 : ℕ) : StarV L → ℤ → kˣ

The relation scales.

noncomputable def MultiplicativeBasisDeformations.StarGauge.Mf {k : Type u} [CommRing k] {t : ℕ} {L : Fin t → ℕ} (Cf : StarV L → StarV L → ℤ → kˣ) (sg : StarV L → StarV L → kˣ) (θ : Equiv.Perm (Fin t)) (c0 : ℕ) : StarV L → ℤ → kˣ

The arrow scales, indexed by the child endpoint of the edge.

theorem MultiplicativeBasisDeformations.StarGauge.L_rep {t : ℕ} {L : Fin t → ℕ} (θ : Equiv.Perm (Fin t)) (hL : ∀ (i : Fin t), L (θ i) = L i) (i : Fin t) : L (OrbitReps.rep θ i) = L i

theorem MultiplicativeBasisDeformations.StarGauge.edge_eq {k : Type u} [CommRing k] {t : ℕ} {L : Fin t → ℕ} (Cf : StarV L → StarV L → ℤ → kˣ) (sg : StarV L → StarV L → kˣ) (θ : Equiv.Perm (Fin t)) (hL : ∀ (i : Fin t), L (θ i) = L i) (σ : StarV L ≃ StarV L) (hσo : σ none = none) (hθ : ∀ (i : Fin t) (j : ℕ) (h : j ≤ L i), σ (ch i j h) = ch (θ i) j ⋯) (c0 : ℕ) (hCinv : ∀ (w w' : StarV L) (s : ℤ), Cf (σ w) (σ w') (s + ↑c0) = Cf w w' s) (hsg : ∀ (w w' : StarV L), sg (σ w) (σ w') = sg w w') (hc0 : 0 < c0) (hc0e : Even c0) (i : Fin t) (j : ℕ) (h : j ≤ L i) (s : ℤ) : (Mf Cf sg θ c0 (ch i j h) s * Mf Cf sg θ c0 (ch i j h) (s + 1) * if ↑s = ↑(j + 1) then Nf Cf sg θ c0 (ch i j h) (s + 2) else 1) = lineS Cf sg i j h (Nf Cf sg θ c0 (pa i j h)) s

The edge equations hold on every arm.

theorem MultiplicativeBasisDeformations.StarGauge.reps_periodic {k : Type u} [CommRing k] {t : ℕ} {L : Fin t → ℕ} (Cf : StarV L → StarV L → ℤ → kˣ) (sg : StarV L → StarV L → kˣ) (θ : Equiv.Perm (Fin t)) (hL : ∀ (i : Fin t), L (θ i) = L i) (σ : StarV L ≃ StarV L) (hσo : σ none = none) (hθ : ∀ (i : Fin t) (j : ℕ) (h : j ≤ L i), σ (ch i j h) = ch (θ i) j ⋯) (c0 : ℕ) (hCinv : ∀ (w w' : StarV L) (s : ℤ), Cf (σ w) (σ w') (s + ↑c0) = Cf w w' s) (hc0 : 0 < c0) (hc0e : Even c0) (i : Fin t) (j : ℕ) (h : j ≤ L i) : Function.Periodic (reps Cf sg (Pof θ c0 i) (OrbitReps.rep θ i) j).1 ↑(Pof θ c0 i) ∧ Function.Periodic (reps Cf sg (Pof θ c0 i) (OrbitReps.rep θ i) j).2 ↑(Pof θ c0 i)

theorem MultiplicativeBasisDeformations.StarGauge.Pof_apply {t : ℕ} (θ : Equiv.Perm (Fin t)) (c0 : ℕ) (i : Fin t) : Pof θ c0 (θ i) = Pof θ c0 i

theorem MultiplicativeBasisDeformations.StarGauge.shift_eq {t : ℕ} (θ : Equiv.Perm (Fin t)) (c0 : ℕ) (i : Fin t) (s : ℤ) : ∃ (q : ℤ), s + ↑c0 - ↑(OrbitReps.ord θ (θ i)) * ↑c0 = s - ↑(OrbitReps.ord θ i) * ↑c0 + q * ↑(Pof θ c0 i)

theorem MultiplicativeBasisDeformations.StarGauge.Nf_inv {k : Type u} [CommRing k] {t : ℕ} {L : Fin t → ℕ} (Cf : StarV L → StarV L → ℤ → kˣ) (sg : StarV L → StarV L → kˣ) (θ : Equiv.Perm (Fin t)) (hL : ∀ (i : Fin t), L (θ i) = L i) (σ : StarV L ≃ StarV L) (hσo : σ none = none) (hθ : ∀ (i : Fin t) (j : ℕ) (h : j ≤ L i), σ (ch i j h) = ch (θ i) j ⋯) (c0 : ℕ) (hCinv : ∀ (w w' : StarV L) (s : ℤ), Cf (σ w) (σ w') (s + ↑c0) = Cf w w' s) (hc0 : 0 < c0) (hc0e : Even c0) (v : StarV L) (s : ℤ) : Nf Cf sg θ c0 (σ v) (s + ↑c0) = Nf Cf sg θ c0 v s

The relation scales are g-invariant.

theorem MultiplicativeBasisDeformations.StarGauge.Mf_inv {k : Type u} [CommRing k] {t : ℕ} {L : Fin t → ℕ} (Cf : StarV L → StarV L → ℤ → kˣ) (sg : StarV L → StarV L → kˣ) (θ : Equiv.Perm (Fin t)) (hL : ∀ (i : Fin t), L (θ i) = L i) (σ : StarV L ≃ StarV L) (hσo : σ none = none) (hθ : ∀ (i : Fin t) (j : ℕ) (h : j ≤ L i), σ (ch i j h) = ch (θ i) j ⋯) (c0 : ℕ) (hCinv : ∀ (w w' : StarV L) (s : ℤ), Cf (σ w) (σ w') (s + ↑c0) = Cf w w' s) (hc0 : 0 < c0) (hc0e : Even c0) (v : StarV L) (s : ℤ) : Mf Cf sg θ c0 (σ v) (s + ↑c0) = Mf Cf sg θ c0 v s

The arrow scales are g-invariant.