Step 1 of Remark 21
ProvedBlockCycleRotation.gTerm_eqanalytic-number-theoryblock-cycle-rotationzeta-values
Step 1 of Remark 21. (2a+a')/(2a²(a+a')²) = (1/(2a'))(1/a² - 1/(a+a')²).
In Blomer–Bux this is Remark 21, “Summand rewriting”.
Preamble
import Definitions.Def_BlockCycleRotation_Remark21 import Mathlib open BlockCycleRotation open Real Finset Filter Topology
Formal statement
theorem BlockCycleRotation.gTerm_eq (p : ℕ × ℕ) : gTerm p = (zTerm p - eTerm p) / 2 := by sorry
Source
Valentin Blomer and Kai-Uwe Bux, "The cost of cyclic permutations and remainder sums in the Euclidean algorithm", AofA 2026, LIPIcs vol. 381, pp. 14:1-14:17, doi:10.4230/LIPIcs.AofA.2026.14. Numbering follows the full version, arXiv:2601.00979v1 -- Remark 21. Lean source: https://github.com/dbenbenn/block-cycle-rotation/blob/f69003fd8b00c9b5d6d1a4f6807b4943bce0a92c/BlockCycleRotation/Remark21.lean#L62-L76