A density version of the Halpern-Läuchli theorem

We prove a density version of the Halpern-Lä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⩾2 such that every t∈T has exactly b immediate successors. We show that for every d⩾1 and every tuple (T1,…,Td) of homogeneous trees, if D is a subset of the level product of (T1,…,Td) satisfying lim supn→∞|D∩(T1(n)×⋯×Td(n))||T1(n)×⋯×Td(n)|>0 then there exist strong subtrees (S1,…,Sd) of (T1,…,Td) having a common level set such that the level product of (S1,…,Sd) is a subset of D.