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.
Comb Structure in co-E-Free Graphs — Examples
1 · Prerequisites
- Absolute and Conditional Convergence; Rearrangement; Products
- Binary Operations, Monoids, Groups and Subgroups
- Blockades, Combs and Pattern Graphs
- Cographs, Perfect Patterns and Pure Pairs
- Comb Structure in co-E-Free Graphs
- Compactness in Metric Spaces
- Completeness, Completion, and Uniform Continuity
- Construction of the Natural Numbers
- Construction of the Real Numbers via Cauchy Sequences
- Construction of the Real Numbers via Dedekind Cuts
- Continuity, IVT, EVT, and Uniform Continuity
- Countability and Uncountability
- Finite Counting, Factorials and Binomial Coefficients
- Finite Probability Spaces and Random Variables
- Foundations of the Real Numbers for Analysis
- Graph Colouring
- Graphs, Walks and Connectivity
- Inclusion–Exclusion, the Pigeonhole Principle and Double Counting
- Induced Subgraphs and Hereditary Graph Classes
- Iterative Sparsification and the Five-Vertex Path
- Limits of Real Functions
- limsup, liminf, and Subsequential Limits
- Metric Spaces
- Modules, Substitution and Prime Graphs
- Monotone Functions, Discontinuities, and Continuity Sets
- Monotone Sequences, Bolzano-Weierstrass, and Cauchy Completeness
- Order, Zorn's Lemma, and the Axiom of Choice
- Polynomial Rödl, Virality and Erdős–Hajnal Equivalence
- Power Series and Real-Analytic Functions
- Properties of the Integral and the Working FTC
- Quotient Blockades and Mixing Relations
- Ramsey Theory
- Regular Pairs and Induced Counting
- Relations, Functions, and Quotients
- Rings, Subrings, Integral Domains and Fields
- Roots, Rational Powers, and Classical Inequalities
- Sequences and Limits
- Sequences and Series of Functions; Uniform Convergence
- Series: Convergence and the Nonnegative Tests
- Small-Graph Erdős-Hajnal Consequences
- Sparse Restricted Subgraphs and the Rödl–Nikiforov Theorems
- Suprema and Infima
- The Derivative and the Mean Value Theorems
- The Erdős–Hajnal Property and Homogeneous Sets
- The Exponential Function
- The Five-Cycle and the Erdős-Hajnal Property
- The Logarithm and General Powers
- The Riemann Integral: Definition and Integrability
- The ZFC Axioms and the Basic Set Constructions
- Topology of ℝ
- Vector Spaces, Linear Subspaces, Span and Direct Sums
2 · Summary
Finite adjacency data for the two local obstructions, an overlap class, and a special-vertex comb.
3 · Logical flowchart
4 · Definitions, theorems and proofs
None yet.
5 · Examples, counterexamples and false statements
The two induced co- witnesses behind the forbidden path runs
Example
In the ambient configuration of the preceding lemma, an induced with adjacent only to gives the six-vertex witness on . An induced with adjacent to only gives the six-vertex witness on . The other vertex of the ambient complete nonedge pair does not belong to this second witness.
Facts & Assumptions
Given: The two configurations in the Example.
Co- is the complement of the stated graph (The -graph and co-).
Proof
In the first configuration the nonedges are exactly , the -edges in the order . In the second they are exactly , the -edges in the order . Hence both graphs are co-.
Their displayed paths are induced and the mixed vertex has respectively two consecutive nonneighbours and three consecutive neighbours.
This verifies both finite witnesses.
An -overlap class and its terminal quotient
Example
Fix a comb block whose induced graph consists of two labeled copies of sharing precisely their rim vertex , with no other cross edges.
Facts & Assumptions
Given: The comb block in the Example.
Two vertices in are related when a finite vertex sequence joins them with each consecutive pair contained in one induced inside (The -overlap-chain relation in one comb block).
Proof
Every vertex of belongs to one of the two induced copies, so . For any , the vertex sequence has each consecutive pair in one of those copies; omit repeated consecutive vertices if necessary. Thus [F1] gives , and is the unique overlap class.
The initial overlap blockade is therefore . There is no pair of distinct blocks, so it is pure vacuously. Its mixed-block reachability relation has just the singleton class ; replacing that class by its union returns . Every iterate is consequently , already terminal at the first stage.
This gives the claimed overlap class and terminal quotient.
A bipartite four-tooth comb has the co- structural partition
Example
Let be disjoint independent four-vertex sets. Add teeth , each complete exactly to , and add complete to every and anticomplete to all teeth; add no other edges.
Facts & Assumptions
Given: The displayed bipartite graph.
Co- contains a triangle, on the images of (The -graph and co-).
Proof
The graph is bipartite, with sides and . By [F1] it is co--free.
Choose , set and . Each is independent and co--free.
Each singleton has a pure one-block blockade and one-vertex pattern, and every vertex in another block is anticomplete to it. Thus the structural clauses hold.