A density version of the Halpern-L\"{a}uchli theorem

We prove a density version of the Halpern-L"{a}uchli Theorem. This settles in the affirmative a conjecture of R. Laver. Specifically, let us say that a tree $T$ is homogeneous if $T$ has a unique root and there exists an integer $b\text{meg}2$ such that every $t\in T$ has exactly $b$ immediate successors. We show that for every $d\text{meg}1$ and every tuple $(T_1,\mathrm{.}\mathrm{.}\mathrm{.},T_d)$ of homogeneous trees, if $D$ is a subset of the level product of $(T_1,\mathrm{.}\mathrm{.}\mathrm{.},T_d)$ satisfying $$\underset{n\to \mathrm{\infty }}{\mathrm{lim\hspace{0.17em}sup}}\frac{\mathrm{\mid }D\cap (T_1(n)\times \mathrm{.}\mathrm{.}\mathrm{.}\times T_d(n))\mathrm{\mid }}{\mathrm{\mid }{T}_1(n)\times \mathrm{.}\mathrm{.}\mathrm{.}\times T_d(n)\mathrm{\mid }}>0$$ then there exist strong subtrees $(S_1,\mathrm{.}\mathrm{.}\mathrm{.},S_d)$ of $(T_1,\mathrm{.}\mathrm{.}\mathrm{.},T_d)$ having common level set such that the level product of $(S_1,\mathrm{.}\mathrm{.}\mathrm{.},S_d)$ is a subset of $D$.