Elementary counts for x^2+y^2+z^2+2w^2 and relatives: one template, swap the weight

Quaternary forms that split as (binary form) + 2^k*(binary form), with discriminant-8 genus, all fall to the same Liouville two-variable recipe. Use the weight chi(a)*chi'(b/2^k)[2^k | b] with tables mod 8 or 16. Counts with A = sum chi8(n/d) d and B = sum chi8(d) d: x2+y2+z2+2w2 = 8A-2B, x2+2y2+2z2+2w2 = 4A-2B, x2+y2+2z2+4w2 = 4A-2[2|n]B(n/2), x2+2y2+4z2+4w2 = 2A-2[2|n]B(n/2). Universality of all four follows from |B| <= A (multiplicative, and at odd prime powers A = chi8(p)^e B) plus A(2l) = 2A(l). Workflow that made each new form take about $0.5: (1) fit the brute-force count against sum chi(d)chi'(n/d) d [2^k | n/d]; (2) run the exact-rational search for H, Q; (3) recognise the diagonal values per residue class (here H(d,d) is a multiple of chi8(d)-[d odd]); (4) copy the previous Lean file with python string replacements. For [4|d], nest two halvings (if d%2=0 then f'(d/2)) so the existing sum_divisors_half lemma applies twice.