TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 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.

Finite level-product partition theorem by the compactness tree

Statement

Assume AC. Fix positive integers $d, q$ and finitistic trees $T_{1}, \dots, T_{d}$ . There is an $n > 0$ such that every $q$ -coloring of

$\prod_{i = 1}^{d} (T_{i} ↾ n), T_{i} ↾ n = ⋃_{j < n} T_{i} (j),$

has a color class containing an $(h, 1)$ -matrix for some $h < n$ . The same $n$ has the terminal common-level form: every $q$ -coloring of $\prod_{i} T_{i} (n)$ has a monochromatic $(h, 1)$ -matrix for some $h < n$ whose coordinate sets lie in the terminal levels $T_{i} (n)$ .

Facts & Assumptions

Given: Positive $d, q$ , the finitistic trees, and AC.

[F1]

Finite truncations, domination, and $(h, 1)$ -matrices have the conventions of the local definition. Finitistic trees, level products, density, and matrices

[F2]

Every subset of the full product satisfies the dense-matrix dichotomy in ZF. Halpern–Läuchli dense-matrix dichotomy

[F3]

In ZFC, every height- $ω$ tree with finite levels has an infinite branch. König’s lemma for finite levels

[A1]

AC is assumed, and is used to invoke F3 for the bad-coloring tree. The Axiom of Choice

Proof

1.1

Induct on $q$ . For $q = 1$ , take $n = 2$ : the sole color contains $\prod_{i} T_{i} (1)$ , a $(0, 1)$ -matrix inside the truncation.

F1base

1.2

Assume the assertion for $q$ , with witness $k > 0$ , and suppose for contradiction that the truncation assertion fails for $q + 1$ . For every $n > 0$ there is then a bad $(q + 1)$ -coloring of $\prod_{i} (T_{i} ↾ n)$ , meaning one with no monochromatic $(h, 1)$ -matrix for $h < n$ .

ihassume-contra

2.1

Order all bad finite colorings by restriction. A restriction is still bad, each level is finite because its coloring domain is finite, and step 1.2 gives a node at every positive level; adjoining the empty coloring as root makes a height- $ω$ finite-level tree.

F1step 1.2construct

3.1

Apply F3 using A1. Its branch is a coherent sequence of bad colorings, whose union is a $(q + 1)$ -coloring $c$ of the full product: every tuple belongs to a sufficiently high finite truncation, and coherence makes its color independent of that choice.

F3A1step 2.1choose

4.1

Let $Q$ be the union of the first $q$ color classes of $c$ . Apply F2. Either the last color contains an $(h, 1)$ -matrix, or $Q$ contains a $k$ -matrix for the induction witness $k$ .

F2step 3.1cases

5.1

In the first case, thin each coordinate of the $(h, 1)$ -matrix to finitely many nodes, one dominating witness for each member of the finite height- $(h + 1)$ cone frontier. The finite product is still monochromatic and is contained in some truncation, contradicting that branch node's badness.

F1step 3.1step 4.1assume-case firstchoose

5.2

In the second case write the $k$ -matrix as $\prod_{i} A_{i} \subseteq Q$ . Since $A_{i}$ dominates $T_{i} (k)$ and $T_{i} (k)$ dominates $T_{i} ↾ k$ , choose on the finite truncation a map $f_{i} (x) \in A_{i}$ with $x \leq f_{i} (x)$ . Pull the $q$ colors on $Q$ back along $\prod_{i} f_{i}$ . The induction hypothesis gives a monochromatic $(h, 1)$ -matrix in the truncated domain; its coordinatewise image is still $(h, 1)$ -dense and lies in one of the first $q$ colors. After finite thinning it lies in some branch truncation, again contradicting badness.

F1step 1.2step 3.1step 4.1assume-case secondchoose

6.1

Both dichotomy cases contradict step 1.2. Hence a truncation witness exists for $q + 1$ , and induction proves the first assertion for every positive $q$ . AC entered only at step 3.1; all selections in steps 5.1–5.2 are ZF and finite.

step 1.1step 1.2step 5.1step 5.2cases-exhaustivedischarge-contradictiondischarge-induction

7.1

For the terminal form, fix the truncation witness $n$ and a coloring of $\prod_{i} T_{i} (n)$ . On each finite $T_{i} ↾ n$ , select an extension map $g_{i} (x) \in T_{i} (n)$ with $x \leq g_{i} (x)$ and pull the coloring back along $\prod_{i} g_{i}$ . A monochromatic $(h, 1)$ -matrix from the first assertion maps coordinatewise to an $(h, 1)$ -matrix in $\prod_{i} T_{i} (n)$ of the original color.

F1step 6.1choose∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

13 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 2 and Corollary 2, pp. 362–363 (standard reference, not scraped)