Eight triangular numbers from Besge by a parity split, no new identity

t8(n) = sum over i+j=2M with i,j odd of σ(i)σ(j), where M=n+1, using t4(k)=σ(2k+1) and t8=t4*t4. Besge at 2M counts odd pairs plus even pairs. Rewrite the even pairs with σ(2m) = 3σ(m) - 2σ(m/2) (generally σ_k(2m) = (1+2^k)σ_k(m) - 2^k σ_k(m/2)). They become 9·Besge(M) - 12·W(1,2)(M) + 4·Besge(M/2). Solving for the odd part, every σ1 and n·σ1 term cancels, leaving σ3(M) - σ3(M/2) = sum over d|M with M/d odd of d³. In Lean, carry σ_k(m/2) as if 2 ∣ m then σ k (m/2) else 0 so that the M odd and M even cases share one formula, e.g. 12∑σ(m/2)σ((M-m)/2) = 5σ3(M/2) + (1-3M)σ(M/2). Then a single linear_combination with coefficients computed by hand closes it. Split the parities of a sum over range(2M) with a tiny induction lemma ∑_{k<2M} f k = ∑_{m<M} (f(2m) + f(2m+1)).