Halpern–Läuchli matrix statement and proof destination

Let $d$ be positive finite and let $T_1,\dots ,T_d$ be rooted finitely branching trees of height $\omega$ without terminal nodes. For every $Q\subseteq {\prod }_{i=1}^d{T}_i$, at least one of the following holds:

• For every $k<\omega$ there is a $k$-matrix contained in $Q$.
• There is $h<\omega$ such that for every $k<\omega$ there is an $(h,k)$-matrix contained in $({\prod }_{i=1}^d{T}_i)\setminus Q$.

Matrices have the full-product density meaning of Finite products of pruned trees and dense matrices, not an assumed equal-level or strong-subtree formulation. This is the Halpern–Läuchli matrix theorem recorded without proof here.

The planned page halpern-lauchli-and-bpi-without-choice owns the finite word-calculus, density-thinning lemmas, and proof of this theorem. Its separate symmetric-model application must establish its own choice requirements. Monk states this matrix dichotomy as Theorem 29.28 after the no-terminal-node standing convention. Its proof occupies printed pp661–670. The final cone argument must put the finitely many root heights at a common height and preserve density after restriction; equality of those heights is not automatic. No strong-subtree equivalence or symmetric-model consequence is asserted here.

For the boundary instance $Q={\prod }_i{T}_i$, taking $A_i=T_i$ gives every required $k$-matrix, since each node dominates itself. For $Q=\mathrm{\varnothing }$, the same choice gives the second alternative with $h=0$. These two immediate instances do not prove the general dichotomy.