TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedaudited 2026-09-14

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Halpern–Läuchli dense-matrix dichotomy

Statement

In ZF, let $d > 0$ , let $T_{1}, \dots, T_{d}$ be finitistic trees, and let $Q \subseteq \prod_{i = 1}^{d} T_{i}$ . The alternatives need not be exclusive, but at least one of the following holds:

for every $k < ω$ , $Q$ contains a $k$ -matrix;
for some $h < ω$ and every $k < ω$ , $\prod_{i} T_{i} ∖ Q$ contains an $(h, k)$ -matrix.

Facts & Assumptions

Given: The positive finite family of trees and the subset $Q$ in the statement.

[F1]

The preceding definition distinguishes the full product and matrices and proves the common-maximum-height cone restriction. Finitistic trees, level products, density, and matrices

[F2]

The all- $a$ /all- $x$ endpoint word derives the all- $A$ /all-universal- $x$ endpoint word. Finite word-calculus rearrangement

[F3]

Soundness of the three word rules and density-preserving finite thinning defines $W (n, B)$ by reading $W$ from left to right: $\exists A_{i}$ selects an $n_{i}$ -dense subset of $B_{i}$ , $\forall x_{i}$ ranges over it, $\forall a_{i}$ ranges over the height- $n_{i}$ cone traces in $B_{i}$ , and $\exists x_{i}$ ranges over that trace, with the empty word asserting membership in $Q$ . It defines $Φ (W, n, p)$ to mean that $W (n, B)$ holds whenever every $B_{i}$ is $p$ -dense, and proves that derivations preserve the scheme $\forall n \exists p Φ (W, n, p)$ .

Proof

1.1

Let $W_{0} = \forall a_{1} \dots \forall a_{d} \exists x_{1} \dots \exists x_{d}$ and $W_{1} = \exists A_{1} \dots \exists A_{d} \forall x_{1} \dots \forall x_{d}$ . By classical logic, the scheme $S (W_{0}) : = \forall n \exists p Φ (W_{0}, n, p)$ either holds or fails.

givenconstructcases

2.1

Assume first that $S (W_{0})$ holds. By F2 and F3, $S (W_{1})$ holds. Fix $k$ , take $n = (k, \dots, k)$ , and obtain a corresponding $p$ .

F2F3step 1.1assume-case first

2.2

Assume instead that $S (W_{0})$ fails. Then some vector $n$ satisfies: for every $p$ there are $p$ -dense $B_{i}$ for which $W_{0} (n, B)$ is false. Unwinding the negated endpoint word gives roots $t_{i} \in T_{i} (n_{i})$ whose cones $a_{i} = B_{i} \cap {u : t_{i} \leq_{T_{i}} u}$ satisfy $\prod_{i} a_{i} \subseteq \prod_{i} T_{i} ∖ Q$ .

F3step 1.1assume-case second

3.1

Apply $Φ (W_{1}, n, p)$ from step 2.1 with $B_{i} = T_{i}$ , which is $p$ -dense because it contains every node. The interpretation supplies $k$ -dense $A_{i} \subseteq T_{i}$ such that every tuple in $\prod_{i} A_{i}$ lies in $Q$ . Hence $Q$ contains a $k$ -matrix; since $k$ was arbitrary, alternative 1 holds.

F1F3step 2.1

3.2

Put $h = \max_{i} n_{i}$ for the vector from step 2.2 and fix $k < ω$ . Take $p = h + k$ , extend each of the finitely many $t_{i}$ to a node $s_{i} \in T_{i} (h)$ , and put $C_{i} = a_{i} \cap {u : s_{i} \leq_{T_{i}} u}$ . Every height- $(h + k)$ extension of $s_{i}$ is dominated by $B_{i}$ , and its dominating member belongs to $C_{i}$ ; hence $C_{i}$ is $(h, k)$ -dense. Also $\prod_{i} C_{i} \subseteq \prod_{i} a_{i}$ lies in the complement of $Q$ . Thus alternative 2 holds for this single $h$ and every $k$ , including $k = 0$ .

F1step 2.2choose

4.1

The two cases in step 1.1 are exhaustive, and steps 3.1 and 3.2 prove the respective alternatives. No infinite choice was used: only finitely many cone roots were extended in step 3.2.

step 1.1step 3.1step 3.2cases-exhaustive∎

Depends on

Used by

Dependency tree · two levels

6 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Halpern–Läuchli, A partition theorem (1966), Theorem 1 and proof, pp. 361–367 (standard reference, not scraped)
Monk, Set theory following Jech (2024), Theorem 29.28, pp. 661–670 (standard reference, not scraped)