LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-06

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.

Integral geometric layers exist, cover the partition, and retain the required cutoff bounds

Statement

For the integral geometric layers of a decreasing partition with $t \geq ℓ \geq 4$ , the integer $q$ exists, the layers are nonempty and partition $(A_{1}, \dots, A_{t})$ , and for every $1 \leq r \leq q$ , $ℓ^{r / 4} \leq m_{r} \leq ℓ^{r / 2} .$

Facts & Assumptions

Given: $t \geq ℓ \geq 4$ and the integral cutoffs $m_{r}$ and layers $C_{r}$ .

[F1]

Each $m_{r}$ is the largest integer at most both $t$ and $ℓ^{r / 2}$ , and $q$ is the least index with $m_{q} = t$ (Integral geometric layers of a decreasing block partition).

[F2]

Positive real powers satisfy $(a^{r})^{s} = a^{r s}$ (The exponent, product, quotient, and iterated-power laws for positive real bases and real exponents).

[F3]

Every nonempty subset of $N$ has a least element (The well-ordering principle).

Proof

technique · direct

1.1

Choose an integer $N > t$ ; then $ℓ^{N / 2} \geq 2^{N / 2} > t$ , so $m_{N} = t$ by [F1]. Thus the set of indices attaining $t$ is nonempty, and [F3] supplies the least one $q$ .

F1F3algebra

1.2

The upper bound $m_{r} \leq ℓ^{r / 2}$ is part of [F1]. First let $r < q$ and write $x : = ℓ^{r / 2} \geq 2$ . Then $m_{r} < t$ , so maximality in [F1] gives $x < m_{r} + 1$ . If $m_{r} < \sqrt{x}$ , then $m_{r}^{2} < x < m_{r} + 1$ ; but $m_{r} \geq 2$ and $m_{r}^{2} \geq m_{r} + 1$ , a contradiction. Thus $m_{r} \geq \sqrt{x} = ℓ^{r / 4}$ by [F2]. For the terminal cutoff, $m_{1} \leq \sqrt{ℓ} < ℓ \leq t$ , so $q \geq 2$ . Put $y : = ℓ^{(q - 1) / 2}$ . Since $m_{q - 1} < t$ and $m_{q - 1}$ is the largest integer at most $y$ , integrality gives $t \geq m_{q - 1} + 1 > y \geq ℓ^{q / 4}$ . Hence $m_{q} = t \geq ℓ^{q / 4}$ as well.

F1F2assume-contradischarge-contradictionalgebra

2.1

Fix $2 \leq r \leq q$ . Minimality of $q$ gives $m_{r - 1} < t$ . Put $x = ℓ^{(r - 1) / 2} \geq 1$ . Since $m_{r - 1} \leq x$ and $ℓ^{r / 2} = \sqrt{ℓ} x \geq 2 x \geq x + 1$ , the integer $m_{r - 1} + 1$ is at most both $t$ and $ℓ^{r / 2}$ . It is therefore admissible in the maximum defining $m_{r}$ , so $m_{r} \geq m_{r - 1} + 1$ . Also $m_{1} \geq 1$ ; hence every layer is nonempty and the successive index intervals cover exactly $[t]$ .

F1step 1.1algebra

3.1

Steps 1.1--2.1 prove existence, coverage, nonemptiness, and both cutoff bounds.

step 1.1step 2.1step 1.2∎

Depends on

Used by

Dependency tree · two levels

34 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

Huang, Ju, and Zhou, Erdős–Hajnal beyond the five-vertex path, proof of Lemma 5.1 (standard reference, not scraped)