value=sum(i,j<q, coeff[i,j]*(i+j*sqrt2)^k*(sqrt2)^(i*ell)*(a/b)^(j*ell)) in exact quadratic arithmetic. Signed coefficients and 0^0=1 are explicit.
Proposed arity: 8. Parameters: a b q coeff ell k value trace. No reviewed kernel definition exists yet.
This is a human-readable planning contract, not a parsed kernel formula or accepted proof.