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.

✓ 3 results · all verified · 1 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 2 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.

Generalized Niceness and Reduction Outcomes -- Examples

1 · Prerequisites

2 · Summary

These examples check the batch-15 mechanisms on explicit finite data. The first shows how a weakly sparse four-block configuration can be thinned to equal subblocks with directional sparsity. The second shows the maximal-blockade extension step behind the pure-pair extraction lemma. The third records the numerical exponent choice used in the final iterative restricted-sparsification argument.

3 · Logical flowchart

4 · Definitions, theorems and proofs

None yet.

5 · Examples, counterexamples and false statements

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

Thinning a four-block weakly sparse blockade to directional sparse subblocks

Example

Let $G$ have four pairwise disjoint blocks $A_{1} = {a_{1}, \dots, a_{8}}, A_{2} = {b_{1}, \dots, b_{8}}, A_{3} = {c_{1}, \dots, c_{8}}, A_{4} = {d_{1}, \dots, d_{8}} .$

and suppose the only cross-edges between noncomplete pairs are

$a_{1} b_{1}, a_{2} c_{1}, a_{3} d_{1}, b_{2} c_{2}, b_{3} d_{2}, c_{3} d_{3} .$

Then $(A_{1}, A_{2}, A_{3}, A_{4})$ is a blockade of width $8$ , every noncomplete pair is weakly $1 / 16$ -sparse, and the subblocks

$D_{1} = {a_{7}, a_{8}}, D_{2} = {b_{7}, b_{8}}, D_{3} = {c_{7}, c_{8}}, D_{4} = {d_{7}, d_{8}}$

are pairwise complete or pairwise anticomplete. In particular every formerly weakly sparse pair becomes directionally $0$ -sparse after thinning.

Facts & Assumptions

Given: The graph $G$ and the four blocks $A_{1}, A_{2}, A_{3}, A_{4}$ described in the example.

[L1]

A blockade is an ordered sequence of pairwise disjoint nonempty vertex sets, and its width is the minimum block size (Blockades, their length, their width, and their support).

[L2]

A weakly $c$ -sparse pair $(X, Y)$ satisfies $e_{G} (X, Y) \leq c ∣ X ∣ ∣ Y ∣$ , while directional sparsity bounds the neighbours of each single vertex into the opposite set (Sparsity of one vertex set to another, and weak sparsity of a pair).

Verification

technique · direct adjacency count

1.1

The four blocks are pairwise disjoint and nonempty, each has size $8$ , so $(A_{1}, A_{2}, A_{3}, A_{4})$ is a blockade of width $8$ by [L1]. Every noncomplete pair listed in the example has exactly one cross-edge, hence at most $1 = (1 / 16) \cdot 8 \cdot 8$ cross-edges. Therefore each such pair is weakly $1 / 16$ -sparse by [L2].

L1L2givenalgebra

1.2

None of the vertices $a_{7}, a_{8}, b_{7}, b_{8}, c_{7}, c_{8}, d_{7}, d_{8}$ appears in any of the six displayed cross-edges. Hence every noncomplete pair among $D_{1}, D_{2}, D_{3}, D_{4}$ has no cross-edge at all, so each vertex in one chosen subblock has $0$ neighbours in the other. By [L2], those pairs are directionally $0$ -sparse.

givenL2

2.1

Therefore the thinning $(A_{1}, A_{2}, A_{3}, A_{4}) ⇝ (D_{1}, D_{2}, D_{3}, D_{4})$ exhibits exactly the weak-to-directional sparsity conversion claimed in the example.

step 1.1step 1.2∎

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

A large almost-pure pair extends an anticomplete blockade

Example

Let

$B_{0} = {u_{1}, u_{2}}, B_{1} = {v_{1}, v_{2}}, B_{2} = {w_{1}, w_{2}, w_{3}, w_{4}, w_{5}, w_{6}},$

and assume:

$B_{0}$ is anticomplete to $B_{1}$ ;
$B_{0} \cup B_{1}$ is anticomplete to $B_{2}$ ;
inside $B_{2}$ there are disjoint subsets $X = {w_{1}, w_{2}}, Y = {w_{3}, w_{4}, w_{5}, w_{6}},$ with $Y$ anticomplete to $X$ .

Then $(B_{0}, B_{1}, B_{2})$ is an anticomplete blockade, and replacing the last block $B_{2}$ by the pair $(X, Y)$ produces the longer anticomplete blockade $(B_{0}, B_{1}, X, Y)$ .

Facts & Assumptions

Given: The blocks $B_{0}, B_{1}, B_{2}$ and the subsets $X, Y \subseteq B_{2}$ with the adjacency relations stated in the example.

[L1]

A blockade is an ordered sequence of pairwise disjoint nonempty vertex sets (Blockades, their length, their width, and their support).

[L2]

A pair of disjoint vertex sets is anticomplete exactly when there are no edges between them (Edges between disjoint vertex sets; complete, anticomplete, pure and mixed pairs).

Verification

technique · direct

1.1

The sets $B_{0}, B_{1}, B_{2}$ are pairwise disjoint and nonempty, so $(B_{0}, B_{1}, B_{2})$ is a blockade by [L1]. Hypotheses 1 and 2 say that each earlier block is anticomplete to every later block, so [L2] makes it an anticomplete blockade.

L1L2given

1.2

The sets $X$ and $Y$ are disjoint nonempty subsets of $B_{2}$ , and hypothesis 3 says that $Y$ is anticomplete to $X$ . Hypothesis 2 also implies that both $X$ and $Y$ are anticomplete to $B_{0} \cup B_{1}$ . Therefore every earlier block in $(B_{0}, B_{1}, X, Y)$ is anticomplete to every later block.

givenL2

2.1

By steps 1.1 and 1.2, replacing the last block $B_{2}$ by the anticomplete pair $(X, Y)$ extends the original anticomplete blockade by one step.

step 1.1step 1.2∎

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

A numeric run of the Lemma 3.3 exponent choice

Example

Suppose the three-outcome constants for a generalized nice, leaf-reducible, wonderful family satisfy

$c_{3} = c_{4} = 4, c = \frac{1}{4}, x = 2^{- 10} .$

Then the exponent choices in the final restricted-sparsification step become

$b_{1} = \frac{c_{4}}{2} = 2, b_{2} = \frac{4 c_{3}}{c_{4}} = 4, b_{3} = c_{3} = 4,$

$b_{1} b_{2} = 8 = b_{2} + b_{3} .$

Let $G$ be a $c^{2}$ -restricted $\overline{F}$ -free graph satisfying the two global failure hypotheses of the helper lemma. If $c y \in [x, c^{2}]$ , then the helper asks for a $c y$ -restricted induced subgraph $F$ of size at least $(c y)^{4} ∣ G ∣$ and returns a $(c y)^{2}$ -restricted induced subgraph of size at least $(c y)^{4} ∣ F ∣$ . The iterative lemma then yields an $x$ -restricted induced subgraph of size at least $x^{8} ∣ G ∣$ .

Facts & Assumptions

Given: The numerical choices $c_{3} = c_{4} = 4$ , $c = \frac{1}{4}$ , and $x = 2^{- 10}$ , and a graph $G$ satisfying the conditional hypotheses in the Example.

[L1]

The helper claim uses the substitutions $b_{1} = c_{4} / 2$ , $b_{2} = 4 c_{3} / c_{4}$ , and $b_{3} = c_{3}$ (A large cy-restricted subgraph in the three-outcome theorem forces a smaller-scale restricted subgraph).

[L2]

The iterative restricted-sparsification lemma concludes with an $x$ -restricted induced subgraph of size at least $x^{b_{1} b_{2}} ∣ G ∣$ (Iterated restricted sparsification reaches the target scale).

[L3]

The final generalized-niceness lemma is obtained by exactly this choice of $b_{1}, b_{2}, b_{3}$ (Constant-scale restricted generalized niceness yields an x-scale restricted subgraph, a polynomial clique or stable set, or a blockade).

Verification

technique · direct arithmetic

1.1

Substituting the given values into [L1] gives $b_{1} = 2$ , $b_{2} = 4$ , and $b_{3} = 4$ . Therefore $b_{1} b_{2} = 8 = b_{2} + b_{3}$ , so the numerical inequality required by the iterative lemma holds exactly.

L1givenalgebra

2.1

The graph $G$ itself supplies the starting $c^{2}$ -restricted subgraph required by [L2], because $∣ G ∣ \geq (c^{2})^{b_{2}} ∣ G ∣$ . For every $λ \in [x, c^{2}]$ , write $λ = c y$ . The helper [L1], under the two global failure hypotheses in the Given data, sends each $λ$ -restricted $F$ with $∣ F ∣ \geq λ^{b_{2}} ∣ G ∣ = λ^{4} ∣ G ∣$ to a $λ^{b_{1}}$ -restricted subgraph of size at least $λ^{b_{3}} ∣ F ∣ = λ^{4} ∣ F ∣$ . Thus both hypotheses of [L2] hold with starting constant $c^{2}$ , and it gives an $x$ -restricted induced subgraph of size at least $x^{b_{1} b_{2}} ∣ G ∣ = x^{8} ∣ G ∣$ .

step 1.1L1L2givenalgebra

3.1

This is exactly the numerical exponent pattern used again in [L3].

step 2.1L3∎

Generalized Niceness and Reduction Outcomes -- Examples

1 · Prerequisites

2 · Summary

3 · Logical flowchart

4 · Definitions, theorems and proofs

5 · Examples, counterexamples and false statements

Thinning a four-block weakly sparse blockade to directional sparse subblocks

Example

Facts & Assumptions

Verification

A large almost-pure pair extends an anticomplete blockade

Example

Facts & Assumptions

Verification

A numeric run of the Lemma 3.3 exponent choice

Example

Facts & Assumptions

Verification

Sources