The global side of S2b-1: the X-free part of U_r(A / D_{5n}) is the functional locValue r (same formulas, global constants) on t A / D_{5n}.

theorem Zeta32.PrimeEdge.locPoly_X_mul (r : ℚ) (q : Polynomial ℚ) : locPoly r (Polynomial.X * q) = polynomialMoment r q

theorem Zeta32.PrimeEdge.locPoly_C (s c : ℚ) : locPoly s (Polynomial.C c) = 2 * s * c

theorem Zeta32.PrimeEdge.X_mul_prod_erase (M : Finset ℕ) {j : ℕ} (hj : j ∈ M) : Polynomial.X * ∏ m' ∈ M.erase j, (Polynomial.X + Polynomial.C ↑m') = mprod M - Polynomial.C ↑j * ∏ m' ∈ M.erase j, (Polynomial.X + Polynomial.C ↑m')

theorem Zeta32.PrimeEdge.XA_pf (A : Polynomial ℚ) (M : Finset ℕ) : Polynomial.X * A = (Polynomial.X * (A /ₘ mprod M) + Polynomial.C (∑ j ∈ M, resN A M j)) * mprod M + ∑ j ∈ M, Polynomial.C (-↑j * resN A M j) * ∏ m' ∈ M.erase j, (Polynomial.X + Polynomial.C ↑m')

X · A in partial-fraction form over D_{5n}.

theorem Zeta32.PrimeEdge.Lfun_coeff_zero (r : ℚ) (n : ℕ) (A : Polynomial ℚ) : (Arith.Local.Lfun r n A).coeff 0 = locValue r (Polynomial.X * A) (Finset.Icc 1 (5 * n))

The X-free part of Lfun is locValue r (X A) [1, 5n].