Factorized B\u00e9zout bound for curves with no common infinite factor

Let $p$ and $q$ be nonzero plane polynomials ($h_{p0} : p \neq 0$, $h_{q0} : q \neq 0$) of total degrees at most $d_1$ and $d_2$, and assume they share no common irreducible factor with infinite real zero set ($h_{\mathrm{noinf}} : \neg\,\mathrm{HasCommonInfiniteIrreducibleFactor}\,p\,q$). Then their real zero sets meet in a finite set, with an explicit bound:

The proof covers $Z(p) \cap Z(q)$ by the intersections $Z(h) \cap Z(k)$ over pairs $(h, k)$ of normalized factors of $p$ and $q$, and bounds each pair by $(d_1 + d_2 + 1)^5$ in one of two branches. If $h$ and $k$ are associated (a shared irreducible factor, which the hypothesis allows when its real zero set is finite), then $Z(h) = Z(k)$ and the bound comes from finite_real_zero_set_of_irreducible_factor_bound, that is, from the singularity count of $h$. If $h$ and $k$ are not associated, irreducible_pair_intersection_bound gives $(d_1 + d_2 + 1)^4$. The number of pairs is at most $d_1 d_2 \le (d_1 + d_2 + 1)^2$, which gives the eighth power. This lemma feeds directly into the existential bezout statement.