2607.20376v1 / README.md
all files
# Reproduction of arXiv:2607.20376v1
Status: **reproduced**, from one explicitly named deep external hypothesis.
The formal development is in [`Tihany.lean`](./Tihany.lean). It proves the
paper's new Theorem 1.4 in full and derives its central even-hole-free result,
Theorem 1.5, from exactly the bisimplicial-vertex part of the
Chudnovsky--Seymour structural theorem.
## Verification
From this directory:
```sh
lake env lean Tihany.lean
```
This succeeds offline. The file contains no `sorry`, `admit`, or custom
`axiom` declaration. An audit with
```lean
#print axioms Tihany.theorem14
#print axioms Tihany.theorem15
```
reported only `[propext, Classical.choice, Quot.sound]`, the standard logical
principles used throughout mathlib. In particular,
`ChudnovskySeymourStatement` is a proposition passed explicitly to
`theorem15`, not an axiom.
## Final theorem and declared hypothesis
`Tihany.theorem15` proves, for a finite simple graph `G` and integers
`s,t ≥ 2`,
```lean
(G.cliqueNum : ℕ∞) < G.chromaticNumber
G.chromaticNumber = s + t - 1
EvenHoleFree G
-----------------------------------------
Splittable G s t
```
from this one named hypothesis:
```lean
def ChudnovskySeymourStatement : Prop :=
∀ (W : Type u) [Fintype W] (H : SimpleGraph W),
EvenHoleFree H → Nonempty W → ∃ v : W, Bisimplicial H v
```
This is the precise part of Chudnovsky and Seymour's deep structural theorem
used by the paper. Their additional bound `χ(H) ≤ 2ω(H)-1` is not assumed.
Formalizing the structural theorem itself would require reproducing the
separate long decomposition theorem on even-hole-free graphs, so it is the
single external result treated under the run's deep-theorem exception.
## Fidelity of the definitions
The development uses mathlib's `SimpleGraph`, induced graph, coloring,
chromatic number, clique number, cycle graph, and induced-containment APIs.
- `Bisimplicial G v` is literally the paper's definition: `neighborSet v` is
the union of two clique sets. `bisimplicial_iff_finset` proves equivalence
with the disjoint finite-clique form used in the proof. This also formally
verifies the paper's observation that the two cliques may be made
disjoint.
- `Splittable G s t` says that some vertex set and its complement induce
graphs of chromatic number at least `s` and `t`. The theorem
`splittable_iff_partition` proves equivalence with a naive formulation
quantifying two disjoint sets whose union is the whole vertex set.
- `EvenHoleFree G` excludes induced copies `cycleGraph n ⊴ G` for every even
`n ≥ 4`. Mathlib defines `⊴` as existence of a graph embedding, hence as an
induced copy. `evenHoleFree_iff_naive` proves equivalence with the naive
statement that no induced vertex set is isomorphic to such a cycle.
- `C4Free G` is the standard condition `¬ cycleGraph 4 ⊴ G`.
- The final hypotheses and conclusion use mathlib's actual `cliqueNum` and
`chromaticNumber`, not replacement invariants.
## Proof inventory
The file proves the following components.
1. `crossNeighborhoods_comparable` constructs an actual
`cycleGraph 4 ↪g G` from two incomparable cross-neighborhoods. Thus the
paper's four-vertex argument is checked against the standard induced-cycle
definition.
2. `exists_clique_with_clique_commonNeighbors` proves the structural part of
Lemma 2.2. Instead of enumerating all of `A`, it chooses a member with
minimum cross-neighborhood and extends it to an arbitrary `r`-subset.
Comparability proves that this minimum neighborhood is contained in every
other one, which is exactly what the enumeration supplies.
3. `colorable_of_missing_commonNeighbor` formalizes the coloring surgery in
Lemma 2.1: if a color class of `G-K` lacks a vertex complete to `K`, that
class is recolored using vertices of `K`, saving one color.
4. `clique_isTihanyAt` completes Lemma 2.1. If every color class has a common
neighbor, one representative per color together with `K` forms a forbidden
clique of order `χ(G)`.
5. `exists_tihany_clique` combines the two paper lemmas.
6. `exists_vertexCritical_induced` chooses a smallest non-`(k-1)`-colorable
induced subgraph. `colorable_of_delete_colorable_of_degree_lt` proves the
usual critical-graph minimum-degree bound by extending a deletion coloring
with a color absent from the neighborhood.
7. `theorem14_coloring` performs the corrected bisimplicial degree argument,
produces the Tihany clique, and transports the split from the critical
induced subgraph back to the original graph.
8. `theorem14` converts the exact mathlib hypotheses
`ω(G)<χ(G)=s+t-1` to the finite-coloring formulation and handles both
orders of `s,t`.
9. `theorem15` obtains hereditary bisimpliciality by applying the declared
Chudnovsky--Seymour statement to every induced subgraph of an
even-hole-free graph, then invokes `theorem14`.
## Correction to the paper
The last proof paragraph in v1 says, after naming the two neighborhood
cliques, “We may assume that `|A| ≤ |B|`” and then uses
```text
2|A| ≤ |A|+|B| = d(v) ≥ 2s-2
```
to conclude `|A| ≥ s-1`. That inference is invalid: the displayed
inequalities give no lower bound on the smaller summand.
The intended and sufficient choice is the larger clique:
`|B| ≤ |A|`. Then
```text
d(v) = |A|+|B| ≤ 2|A|
and
d(v) ≥ s+t-2 ≥ 2s-2,
```
so `|A| ≥ s-1`. `theorem14_coloring` makes exactly this corrected choice
(and swaps `A,B` when necessary). No other change to the argument is needed,
so this is a local direction typo rather than a counterexample to the
theorem.
## Files changed
- `Tihany.lean`: complete formal development.
- `README.md`: this reproduction and audit report.