Periodic scalar gauges (Lemma A.1)

lem:periodic-scalar-gauges (periodic-mesh-calculations.tex): "The required coefficient ratios prescribe … equations μ_{a,j} μ_{b,j-1} = t_{v,j} η_{v,j}, μ_{a,j-1} μ_{b,j-1} = t_{u,j} η_{u,j}. Dividing the two equations gives a recurrence for μ_a. It closes around the cycle exactly when [a product of the η] equals a prescribed number. Choose the root product freely and assign the child products down the tree. Realize each product by one factor, setting the other factors to one."

In height coordinates an edge line is indexed by ℤ and the equations read μ h μ (h+1) η' (h+2) = S h, where η' is the relation scale at the child endpoint when it sits at height h + 2, and the parent's scales are already absorbed into S. A solution periodic of even period P exists after choosing one factor of η' per period (exists_periodic_line).

def MultiplicativeBasisDeformations.lineRec {k : Type u} [CommRing k] (R : ℤ → kˣ) : ℕ → kˣ

The recurrence from μ 0 = 1.

theorem MultiplicativeBasisDeformations.lineRec_eq {k : Type u} [CommRing k] (R : ℤ → kˣ) (n : ℕ) : lineRec R n = ∏ i ∈ Finset.range n, R ↑i ^ (-1) ^ (n - 1 - i)

The closing product of the recurrence over [0, n).

theorem MultiplicativeBasisDeformations.exists_periodic_line {k : Type u} [CommRing k] (P : ℕ) (hP : 0 < P) (hPe : Even P) (R : ℤ → kˣ) (hR : ∀ (h : ℤ), R (h + ↑P) = R h) (hprod : ∏ i ∈ Finset.range P, R ↑i ^ (-1) ^ i = 1) : ∃ (μ : ℤ → kˣ), (∀ (h : ℤ), μ (h + ↑P) = μ h) ∧ ∀ (h : ℤ), μ h * μ (h + 1) = R h

A periodic solution of μ h μ (h + 1) = R h for R of even period P, when the alternating product over a period is one.

theorem MultiplicativeBasisDeformations.exists_periodic_line_vertex {k : Type u} [CommRing k] (P : ℕ) (hP : 0 < P) (hPe : Even P) (S : ℤ → kˣ) (hS : ∀ (h : ℤ), S (h + ↑P) = S h) (b : ZMod 2) : ∃ (N : ℤ → kˣ) (M : ℤ → kˣ), (∀ (h : ℤ), N (h + ↑P) = N h) ∧ (∀ (h : ℤ), M (h + ↑P) = M h) ∧ ∀ (h : ℤ), (M h * M (h + 1) * if ↑h = b then N (h + 2) else 1) = S h

One relation scale per period closes the line: for S of even period P and a parity class b (the heights h at which the child endpoint sits at h + 2), there are P-periodic N (relation scales of the child) and M (arrow scales) with M h M (h+1) N' h = S h, where N' h = N (h + 2) in the class b and 1 otherwise.