Intersection bound for a pair of nonassociated irreducible curves

Let $h$ and $k$ be irreducible bivariate real polynomials ($h_h$, $h_k$) of total degrees at most $d_1$ and $d_2$, not associated to each other ($h_{\mathrm{not}} : \neg\,\mathrm{Associated}\,h\,k$). Then their real zero sets meet in a finite set, with an explicit bound:

The proof is a three-way case split on whether the curried polynomials $\mathrm{Curry0}\,h$ and $\mathrm{Curry0}\,k$ have degree zero in the eliminated variable. Both zero: the intersection is empty (zeroCurry_zeroCurry_pair_intersection_bound). Exactly one zero: zeroCurry_nonvertical_pair_intersection_bound, applied with the roles of $h$ and $k$ chosen so that the degree-zero one comes first, gives $d_1 d_2$. Both positive: the curries are primitive and relatively prime, and primitive_nonvertical_pair_intersection_bound gives $((d_1 + d_2)^2 + 1) \cdot \max(d_1, d_2)$. Each of these is at most $(d_1 + d_2 + 1)^4$. The associated case, a shared irreducible factor, is excluded here by hypothesis; in factorized_bezout_bound that case is handled separately through finite_real_zero_set_of_irreducible_factor_bound and the singularity count, since the hypothesis there only forbids a shared factor with infinite real zero set.