LemmaStatement: Literature-sourcedProof: AI-generatedSession-authored (Fable 5 assisted)precheck passjudge pass (gpt-5.6-terra)audited 2026-08-28

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.

A vertex mixed on a quotient block but pure on each member block yields two mixed member blocks with opposite adjacency

Statement

Let $D$ be a block of the quotient blockade $L / M$ , and let $u \notin D$ be a vertex. Suppose that $u$ is mixed on $D$ but is pure to every original block of $L$ contained in $D$ . Then there are two original blocks $A_{1}, A_{2}$ of $L$ , both contained in $D$ , such that

$A_{1}$ and $A_{2}$ are mixed; and
$u$ is complete to $A_{1}$ and anticomplete to $A_{2}$ .

Facts & Assumptions

Given: A blockade $L$ , a quotient block $D$ of $L / M$ , and a vertex $u \notin D$ that is mixed on $D$ but pure to every original block of $L$ contained in $D$ .

[L1]

Because $u$ is mixed on $D$ but pure to each member block, there are original blocks $B_{1}, B_{2} \subseteq D$ such that $u$ is complete to $B_{1}$ and anticomplete to $B_{2}$ (Edges between disjoint vertex sets; complete, anticomplete, pure and mixed pairs).

[L2]

Since $D$ is one quotient block, any two original blocks it contains are related by the mixed-block reachability relation, so there is a chain $B_{1} = A_{r_{1}}, A_{r_{2}}, \dots, A_{r_{m}} = B_{2}$ with each consecutive pair mixed (The quotient blockade obtained from mixed-block reachability, The mixed-block reachability relation on a blockade).

Proof

technique · direct

1.1

By [L1], choose original blocks $B_{1}, B_{2} \subseteq D$ such that $u$ is complete to $B_{1}$ and anticomplete to $B_{2}$ .

L1choose

2.1

By [L2], choose a mixed block chain $B_{1} = A_{r_{1}}, A_{r_{2}}, \dots, A_{r_{m}} = B_{2}$ inside $D$ . Since $u$ is complete to the first block and anticomplete to the last, there is a first index $j < m$ at which the relation changes. Then $u$ is complete to $A_{r_{j}}$ and anticomplete to $A_{r_{j + 1}}$ , and the two blocks are mixed because they are consecutive on the chain.

step 1.1L2choose

3.1

Taking $A_{1} : = A_{r_{j}}$ and $A_{2} : = A_{r_{j + 1}}$ gives the required pair of mixed original blocks in $D$ .

step 2.1∎

Depends on

Used by

Dependency tree · two levels

7 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

Shenwei Huang, Yiao Ju, and Yidong Zhou, Erdős-Hajnal beyond the five-vertex path, Lemma 6.1(3) (standard reference, not scraped)