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.

✓ 4 results · all verified · 3 also independently AI-judged

Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs. The 1 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.

The Structural Criterion for Property (*) — Examples

1 · Prerequisites

2 · Summary

3 · Logical flowchart

4 · Definitions, theorems and proofs

None yet.

5 · Examples, counterexamples and false statements

ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passaudited 2026-09-06Open item page →

A large Y-part in a structural comb partition

Example

Assume $(F_{1}, F_{2}; H)$ satisfies the structural comb-partition hypothesis and $c = 1 / 2$ is an Erdős–Hajnal constant for both $F_{1}$ -free and $F_{2}$ -free graphs. Let $G$ be a finite $\overline{H}$ -free graph containing an $(ℓ, 16)$ -comb with $ℓ \geq 4$ , equipped with a structural partition. If one part has $∣ Y_{i} ∣ = 8$ , the large- $Y$ lemma supplies a clique or stable set in $G$ of size at least $16^{1 / 4} = 2$ .

Facts & Assumptions

Given: The families satisfying the structural comb-partition hypothesis, their common Erdős–Hajnal constant $c = 1 / 2$ , the finite $\overline{H}$ -free graph $G$ and its structurally partitioned $(ℓ, w)$ -comb with $ℓ \geq 4$ , $w = 16$ , and an index $i$ with $∣ Y_{i} ∣ = 8$ .

[F1]

Under the structural comb-partition hypothesis, with a common Erdős–Hajnal constant $c \in (0, 1]$ for the two forbidden families and a structurally partitioned $(ℓ, w)$ -comb with $ℓ, w \geq 4$ , a part with $∣ Y_{i} ∣ \geq w / 2$ yields a clique or stable set in $G$ of size at least $w^{c / 2}$ (A large Y-part in a structural comb partition yields the clique-or-stable-set outcome).

Verification

technique · direct calculation

1.1

The structural and common-constant hypotheses of [F1] are given. Also $c = 1 / 2 \in (0, 1]$ , $ℓ \geq 4$ , $w = 16 \geq 4$ , and $∣ Y_{i} ∣ = 8 = 16 / 2 = w / 2$ . Thus [F1] gives a clique or stable set in $G$ with at least $16^{(1 / 2) / 2}$ vertices.

givenF1

1.2

The displayed lower bound is $16^{(1 / 2) / 2} = 16^{1 / 4} = 2$ .

algebra

2.1

Hence, under the stated structural hypotheses, $G$ has a clique or stable set with at least two vertices, as asserted.

step 1.1step 1.2∎

ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-06Open item page →

A wide transversal in four structural comb partitions

Example

In a structural partition of a $(4, 8)$ -comb, select singleton partition blocks $A_{i} = {x_{i}}$ , one from each comb block. Suppose the pairs $A_{1} A_{2}, A_{1} A_{4}, A_{3} A_{4}$ complete and the other three pairs anticomplete. This is a pure transversal of width $1$ , hence also of width $1 / 2 = w / ℓ^{2}$ .

Facts & Assumptions

Given: A structural partition of a $(4, 8)$ -comb and four selected singleton blocks, one from each of its comb-block partitions, each of size $1 = w / (2 ℓ)$ , with the listed pairwise adjacencies.

[F1]

Such one-per-partition selected blocks form a pure $(ℓ, w / ℓ^{2})$ -blockade (A transversal of wide structural blocks yields the pure blockade outcome).

Verification

technique · direct calculation

1.1

The three listed complete pairs and three listed anticomplete pairs exhaust the six unordered pairs of four blocks. Thus every pair is pure.

given

1.2

Each selected block has size $1 = 8 / (2 \cdot 4)$ , so the hypotheses of [F1] are met and it yields a pure $(4, 8 / 4^{2})$ -blockade.

F1algebra

2.1

Since $8 / 4^{2} = 1 / 2$ , this is the asserted pure $(4, 1 / 2)$ -blockade.

step 1.2algebra∎

ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-06Open item page →

Integral geometric layers for fourteen ordered blocks

Example

For $ℓ = 4$ and $t = 14$ , the integral cutoffs are $m_{1} = 2, m_{2} = 4, m_{3} = 8, m_{4} = 14.$ Thus the four layers have respectively $2, 2, 4, 6$ blocks. The final layer is truncated at the integral endpoint $14$ , rather than referring to a nonintegral block index.

Facts & Assumptions

Given: A decreasing ordered partition of $14$ blocks and $ℓ = 4$ .

[F1]

The cutoff $m_{r}$ is the largest integer at most both $t$ and $ℓ^{r / 2}$ , and layers are successive cutoff differences (Integral geometric layers of a decreasing block partition).

[F2]

These cutoffs produce nonempty layers covering all blocks (Integral geometric layers exist, cover the partition, and retain the required cutoff bounds).

Verification

technique · direct calculation

1.1

The bounds $4^{1 / 2}, 4^{2 / 2}, 4^{3 / 2}, 4^{4 / 2}$ are $2, 4, 8, 16$ ; intersecting their allowed integer indices with $[14]$ gives the stated cutoffs $2, 4, 8, 14$ by [F1].

F1algebra

2.1

Successive differences are $2$ , $4 - 2 = 2$ , $8 - 4 = 4$ , and $14 - 8 = 6$ . Their sum is $14$ , agreeing with the coverage conclusion in [F2].

F2step 1.1algebra

3.1

In particular, the last cutoff is the integer $14$ , so no expression such as a fifteenth or nonintegrally numbered block has been used.

F1step 1.1∎

CounterexampleConstruction: AI-generatedVerification: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-06Open item page →

Omitting cross-block purity breaks the transversal conclusion

Statement refuted

It is false that one wide pure-partition block selected from each comb block must form a pure transversal if cross-block purity is omitted.

Facts & Assumptions

Given: Four comb blocks $B_{i} = {b_{i}^{0}, \dots, b_{i}^{7}}$ and teeth $a_{i}$ . Each $a_{i}$ is complete to $B_{i}$ and anticomplete to the other $B_{j}$ . Take the one-block partitions $A_{1}^{i} = B_{i}$ . Put precisely one edge, $b_{1}^{0} b_{2}^{0}$ , between $B_{1}$ and $B_{2}$ , and put no edges between any other distinct pair of blocks.

[F1]

The specified tooth/block incidences make these four pairs an $(4, 8)$ -comb (Combs in a graph).

[F2]

A pair is mixed when it is neither complete nor anticomplete (Edges between disjoint vertex sets; complete, anticomplete, pure and mixed pairs).

Counterexample

technique · direct finite adjacency check

1.1

Each one-block partition $(A_{1}^{i})$ is vacuously a pure blockade, and $∣ A_{1}^{i} ∣ = 8 \geq 8 / (2 \cdot 4) = 1$ ; [F1] confirms that the ambient blocks are a comb.

F1givenalgebra

1.2

The pair $(A_{1}^{1}, A_{1}^{2})$ has the edge $b_{1}^{0} b_{2}^{0}$ but, for example, does not have $b_{1}^{0} b_{2}^{1}$ . It is neither anticomplete nor complete, hence is mixed by [F2].

F2given

2.1

Therefore the four wide selected blocks are not a pure transversal. The missing cross-block-purity condition is exactly what fails here.

step 1.2F2∎

The Structural Criterion for Property (*) — Examples

1 · Prerequisites

2 · Summary

3 · Logical flowchart

4 · Definitions, theorems and proofs

5 · Examples, counterexamples and false statements

A large Y-part in a structural comb partition

Example

Facts & Assumptions

Verification

A wide transversal in four structural comb partitions

Example

Facts & Assumptions

Verification

Integral geometric layers for fourteen ordered blocks

Example

Facts & Assumptions

Verification

Omitting cross-block purity breaks the transversal conclusion

Statement refuted

Facts & Assumptions

Counterexample

Sources