The gauge on odd quotients of even A (Lemma A.1(2))

lem:periodic-scalar-gauges (2), periodic-mesh-calculations.tex: "For the odd even-A quotient, first keep the scales of the arrows ε_j equal to one and choose the root mesh scales to normalize the coefficients of ε_{j-2} ε_{j-1}. The recurrence on each arm edge advances j by two. … Its product equation determines the next vertex's mesh-scaling product, and the same recursion finishes the normalization."

Vertices of A_{2h} are indexed by their depth d ∈ [0, 2h) from one end; the middle edge is {h - 1, h}, and the deck generator is (d, s) ↦ (2h - 1 - d, s + c₀) with c₀ odd. The coefficients are recorded by C a b s (the coefficient at (a, s + 2) of the arrow from (b, s + 1)). We solve the equations on the half d ≥ h and fold the other half onto it.

def MultiplicativeBasisDeformations.OddGauge.lineS {k : Type u} [Field k] (C : ℕ → ℕ → ℤ → kˣ) (e : ℕ) (Np : ℤ → kˣ) (s : ℤ) : kˣ

The products prescribed on the edge {e, e + 1} of the right half (e ≥ h), given the parent's relation scales Np.

noncomputable def MultiplicativeBasisDeformations.OddGauge.step {k : Type u} [Field k] (C : ℕ → ℕ → ℤ → kˣ) (c0 e : ℕ) (Np : ℤ → kˣ) : (ℤ → kˣ) × (ℤ → kˣ)

One step down the right half.

def MultiplicativeBasisDeformations.OddGauge.Nmid {k : Type u} [Field k] (h : ℕ) (C : ℕ → ℕ → ℤ → kˣ) (s : ℤ) : kˣ

The relation scales of the middle vertex h.

def MultiplicativeBasisDeformations.OddGauge.right {k : Type u} [Field k] (h : ℕ) (C : ℕ → ℕ → ℤ → kˣ) (c0 : ℕ) : ℕ → (ℤ → kˣ) × (ℤ → kˣ)

The relation scales (.1, of the child h + 1 + j) and arrow scales (.2, of the edge {h + j, h + j + 1}) on the right half.

noncomputable def MultiplicativeBasisDeformations.OddGauge.parN {k : Type u} [Field k] (h : ℕ) (C : ℕ → ℕ → ℤ → kˣ) (c0 j : ℕ) : ℤ → kˣ

The parent relation scales of the edge {h + j, h + j + 1}.

theorem MultiplicativeBasisDeformations.OddGauge.right_eq {k : Type u} [Field k] (h : ℕ) (C : ℕ → ℕ → ℤ → kˣ) (c0 j : ℕ) : right h C c0 j = step C c0 (h + j) (parN h C c0 j)

theorem MultiplicativeBasisDeformations.OddGauge.lineS_periodic {k : Type u} [Field k] (C : ℕ → ℕ → ℤ → kˣ) (c0 : ℕ) (hper : ∀ (a b : ℕ) (s : ℤ), C a b (s + ↑(2 * c0)) = C a b s) (e : ℕ) (Np : ℤ → kˣ) (hNp : ∀ (s : ℤ), Np (s + ↑(2 * c0)) = Np s) (s : ℤ) : lineS C e Np (s + ↑(2 * c0)) = lineS C e Np s

theorem MultiplicativeBasisDeformations.OddGauge.step_spec {k : Type u} [Field k] (C : ℕ → ℕ → ℤ → kˣ) (c0 : ℕ) (hc0 : 0 < c0) (hper : ∀ (a b : ℕ) (s : ℤ), C a b (s + ↑(2 * c0)) = C a b s) (e : ℕ) (Np : ℤ → kˣ) (hNp : ∀ (s : ℤ), Np (s + ↑(2 * c0)) = Np s) : (∀ (s : ℤ), (step C c0 e Np).1 (s + ↑(2 * c0)) = (step C c0 e Np).1 s) ∧ (∀ (s : ℤ), (step C c0 e Np).2 (s + ↑(2 * c0)) = (step C c0 e Np).2 s) ∧ ∀ (s : ℤ), ((step C c0 e Np).2 s * (step C c0 e Np).2 (s + 1) * if ↑s = ↑(e + 1) then (step C c0 e Np).1 (s + 2) else 1) = lineS C e Np s

theorem MultiplicativeBasisDeformations.OddGauge.right_spec {k : Type u} [Field k] (h : ℕ) (C : ℕ → ℕ → ℤ → kˣ) (c0 : ℕ) (hc0 : 0 < c0) (hper : ∀ (a b : ℕ) (s : ℤ), C a b (s + ↑(2 * c0)) = C a b s) (j : ℕ) : (∀ (s : ℤ), (right h C c0 j).1 (s + ↑(2 * c0)) = (right h C c0 j).1 s) ∧ (∀ (s : ℤ), (right h C c0 j).2 (s + ↑(2 * c0)) = (right h C c0 j).2 s) ∧ ∀ (s : ℤ), ((right h C c0 j).2 s * (right h C c0 j).2 (s + 1) * if ↑s = ↑(h + j + 1) then (right h C c0 j).1 (s + 2) else 1) = lineS C (h + j) (parN h C c0 j) s

noncomputable def MultiplicativeBasisDeformations.OddGauge.NR {k : Type u} [Field k] (h : ℕ) (C : ℕ → ℕ → ℤ → kˣ) (c0 d : ℕ) (s : ℤ) : kˣ

The relation scales on the right half d ≥ h.

noncomputable def MultiplicativeBasisDeformations.OddGauge.MR {k : Type u} [Field k] (h : ℕ) (C : ℕ → ℕ → ℤ → kˣ) (c0 e : ℕ) (s : ℤ) : kˣ

The arrow scales on the edges {e, e + 1} with e ≥ h - 1.

noncomputable def MultiplicativeBasisDeformations.OddGauge.Nd {k : Type u} [Field k] (h : ℕ) (C : ℕ → ℕ → ℤ → kˣ) (c0 d : ℕ) (s : ℤ) : kˣ

The relation scales, folding the left half onto the right half.

noncomputable def MultiplicativeBasisDeformations.OddGauge.Md {k : Type u} [Field k] (h : ℕ) (C : ℕ → ℕ → ℤ → kˣ) (c0 e : ℕ) (s : ℤ) : kˣ

The arrow scales of the edges {e, e + 1}.

theorem MultiplicativeBasisDeformations.OddGauge.NR_periodic {k : Type u} [Field k] (h : ℕ) (C : ℕ → ℕ → ℤ → kˣ) (c0 : ℕ) (hc0 : 0 < c0) (hper : ∀ (a b : ℕ) (s : ℤ), C a b (s + ↑(2 * c0)) = C a b s) (d : ℕ) (s : ℤ) : NR h C c0 d (s + ↑(2 * c0)) = NR h C c0 d s

theorem MultiplicativeBasisDeformations.OddGauge.MR_periodic {k : Type u} [Field k] (h : ℕ) (C : ℕ → ℕ → ℤ → kˣ) (c0 : ℕ) (hc0 : 0 < c0) (hper : ∀ (a b : ℕ) (s : ℤ), C a b (s + ↑(2 * c0)) = C a b s) (e : ℕ) (s : ℤ) : MR h C c0 e (s + ↑(2 * c0)) = MR h C c0 e s

theorem MultiplicativeBasisDeformations.OddGauge.Nd_inv {k : Type u} [Field k] (h : ℕ) (C : ℕ → ℕ → ℤ → kˣ) (c0 : ℕ) (hc0 : 0 < c0) (hper : ∀ (a b : ℕ) (s : ℤ), C a b (s + ↑(2 * c0)) = C a b s) (d : ℕ) (hd : d < 2 * h) (s : ℤ) : Nd h C c0 (2 * h - 1 - d) (s + ↑c0) = Nd h C c0 d s

The relation scales are invariant under (d, s) ↦ (2h - 1 - d, s + c₀).

theorem MultiplicativeBasisDeformations.OddGauge.Md_inv {k : Type u} [Field k] (h : ℕ) (C : ℕ → ℕ → ℤ → kˣ) (c0 : ℕ) (hc0 : 0 < c0) (hper : ∀ (a b : ℕ) (s : ℤ), C a b (s + ↑(2 * c0)) = C a b s) (e : ℕ) (he : e + 1 < 2 * h) (s : ℤ) : Md h C c0 (2 * h - 2 - e) (s + ↑c0) = Md h C c0 e s

theorem MultiplicativeBasisDeformations.OddGauge.right_eqn {k : Type u} [Field k] (h : ℕ) (C : ℕ → ℕ → ℤ → kˣ) (c0 : ℕ) (hc0 : 0 < c0) (hper : ∀ (a b : ℕ) (s : ℤ), C a b (s + ↑(2 * c0)) = C a b s) (e : ℕ) (he : h ≤ e) (s : ℤ) : (↑s = ↑(e + 1) → Nd h C c0 (e + 1) (s + 2) * C (e + 1) e s * Md h C c0 e s * Md h C c0 e (s + 1) = 1) ∧ (↑s = ↑e → Nd h C c0 e (s + 2) * C e (e + 1) s * Md h C c0 e s * Md h C c0 e (s + 1) = 1)

The equations on the right half.

theorem MultiplicativeBasisDeformations.OddGauge.mid_eqn {k : Type u} [Field k] (h : ℕ) (C : ℕ → ℕ → ℤ → kˣ) (c0 : ℕ) (hh : 1 ≤ h) (hC : ∀ (a b : ℕ) (s : ℤ), a < 2 * h → b < 2 * h → C (2 * h - 1 - a) (2 * h - 1 - b) (s + ↑c0) = C a b s) (s : ℤ) : (↑s = ↑h → Nd h C c0 h (s + 2) * C h (h - 1) s * Md h C c0 (h - 1) s * Md h C c0 (h - 1) (s + 1) = 1) ∧ (↑s = ↑(h - 1) → Nd h C c0 (h - 1) (s + 2) * C (h - 1) h s * Md h C c0 (h - 1) s * Md h C c0 (h - 1) (s + 1) = 1)

The equations on the middle edge (all arrow scales one).

theorem MultiplicativeBasisDeformations.OddGauge.par_fold (h c0 : ℕ) (hodd : Odd c0) {a : ℕ} (ha : a < 2 * h) (s : ℤ) (hs : ↑s = ↑a) : ↑(s + ↑c0) = ↑(2 * h - 1 - a)

theorem MultiplicativeBasisDeformations.OddGauge.eqn {k : Type u} [Field k] (h : ℕ) (C : ℕ → ℕ → ℤ → kˣ) (c0 : ℕ) (hc0 : 0 < c0) (hper : ∀ (a b : ℕ) (s : ℤ), C a b (s + ↑(2 * c0)) = C a b s) (hh : 1 ≤ h) (hC : ∀ (a b : ℕ) (s : ℤ), a < 2 * h → b < 2 * h → C (2 * h - 1 - a) (2 * h - 1 - b) (s + ↑c0) = C a b s) (hodd : Odd c0) (a b : ℕ) (ha : a < 2 * h) (hb : b < 2 * h) (hab : b = a + 1 ∨ a = b + 1) (s : ℤ) (hs : ↑s = ↑a) : Nd h C c0 a (s + 2) * C a b s * Md h C c0 (min a b) s * Md h C c0 (min a b) (s + 1) = 1

The gauge equations on all edges.