The B-Free Graphs Conjecture: the finite exclusion of arXiv:2608.22537, certified and stripped of its corona hypotheses
Abstract
Litjens, Polak and Sivaraman call a graph sum-perfect when every induced subgraph H satisfies α(H)+ω(H) ≥ |V(H)|, characterise the class by twenty-seven forbidden induced subgraphs, and conjecture that dropping three of them — leaving the class B of the twelve six-vertex bipartite graphs with a perfect matching together with their twelve complements — gives α(G)+ω(G) ≥ |V(G)|-1 for every B-free G. A recent preprint of Frijio reduces the conjecture, by structural arguments, to a finite exclusion: twelve parameter triples (n,a,w) with n=a+w+2 ≤ 14, each of which must be shown not to occur. That exclusion is the whole computational core of the proof, and the evidence offered for it is a floating-point mixed-integer model and a bespoke solver that print UNSAT without a certificate. We prove the exclusion from strictly weaker hypotheses. For each of the twelve triples we show that no B-free graph on n vertices has α=a and ω=w, using none of the corona constraints that the reduction supplies and covering both values of the intersection parameter t=|S ∩ K|, where the source's table forms only twenty-one of the twenty-four cases. That the corona constraints are dispensable was measured, not assumed: each remaining hypothesis is shown load-bearing by an explicit seven-vertex graph. We also certify the encoding step the source reports but does not check — on all 2¹⁵ labelled six-vertex graphs, the inequality form of B-membership agrees with "bipartite with a perfect matching or the complement of one" — and refine the resulting count 4400 into 2200+2200 with the two halves disjoint. Finally we record the conjecture itself as a consequence of the twelve exclusions and one named hypothesis, the structural reduction, which is stated but not proved here. Every statement is machine-checked in Lean 4; the twenty-four infeasibility claims are discharged against stored LRAT certificates by a checker that is itself verified in Lean, so no property of the SAT solver is assumed.
Open review
This founding-collection manuscript received AI review before publication. Independent human review is open. Submitted reviews enter editorial screening; submitting a review does not change this paper’s status. Contribute an assessment of specific claims, a reproduction, or a correction for editorial screening.
Archived files
- Version 1 · current (opens in a new tab)
Source snapshot 2026-08-30 15:34 UTC
File fingerprint
924b6717179e9901cc7178bb414aff6adf5d677727a71907feb9186dc25a0535
Claim ledger
Stated results
BF1routine2026-08-29
Statement description is not included in this imported ledger snapshot. See the PDF for the full theorem wording.
BF2routine2026-08-29
Statement description is not included in this imported ledger snapshot. See the PDF for the full theorem wording.
BF3routine2026-08-29
Statement description is not included in this imported ledger snapshot. See the PDF for the full theorem wording.
BF4known data2026-08-29
Statement description is not included in this imported ledger snapshot. See the PDF for the full theorem wording.
BF5known data2026-08-29
Statement description is not included in this imported ledger snapshot. See the PDF for the full theorem wording.
BF6routine2026-08-29
Statement description is not included in this imported ledger snapshot. See the PDF for the full theorem wording.
BF7candidate2026-08-29
Statement description is not included in this imported ledger snapshot. See the PDF for the full theorem wording.
BF8known2026-08-29
Statement description is not included in this imported ledger snapshot. See the PDF for the full theorem wording.
BF9routine2026-08-29
Statement description is not included in this imported ledger snapshot. See the PDF for the full theorem wording.
BF10routine2026-08-29
Statement description is not included in this imported ledger snapshot. See the PDF for the full theorem wording.
C-7-3-2-0known data2026-08-29
Statement description is not included in this imported ledger snapshot. See the PDF for the full theorem wording.
C-7-3-2-1known data2026-08-29
Statement description is not included in this imported ledger snapshot. See the PDF for the full theorem wording.
C-8-3-3-0known data2026-08-29
Statement description is not included in this imported ledger snapshot. See the PDF for the full theorem wording.
C-8-3-3-1known data2026-08-29
Statement description is not included in this imported ledger snapshot. See the PDF for the full theorem wording.
C-8-4-2-0known data2026-08-29
Statement description is not included in this imported ledger snapshot. See the PDF for the full theorem wording.
C-8-4-2-1known data2026-08-29
Statement description is not included in this imported ledger snapshot. See the PDF for the full theorem wording.
C-9-4-3-0known data2026-08-29
Statement description is not included in this imported ledger snapshot. See the PDF for the full theorem wording.
C-9-4-3-1known data2026-08-29
Statement description is not included in this imported ledger snapshot. See the PDF for the full theorem wording.
C-10-4-4-0known data2026-08-29
Statement description is not included in this imported ledger snapshot. See the PDF for the full theorem wording.
C-10-4-4-1known data2026-08-29
Statement description is not included in this imported ledger snapshot. See the PDF for the full theorem wording.
C-10-5-3-0known data2026-08-29
Statement description is not included in this imported ledger snapshot. See the PDF for the full theorem wording.
C-10-5-3-1known data2026-08-29
Statement description is not included in this imported ledger snapshot. See the PDF for the full theorem wording.
C-11-5-4-0known data2026-08-29
Statement description is not included in this imported ledger snapshot. See the PDF for the full theorem wording.
C-11-5-4-1known data2026-08-29
Statement description is not included in this imported ledger snapshot. See the PDF for the full theorem wording.
C-12-5-5-0known data2026-08-29
Statement description is not included in this imported ledger snapshot. See the PDF for the full theorem wording.
C-12-5-5-1known data2026-08-29
Statement description is not included in this imported ledger snapshot. See the PDF for the full theorem wording.
C-12-6-4-0known data2026-08-29
Statement description is not included in this imported ledger snapshot. See the PDF for the full theorem wording.
C-12-6-4-1known data2026-08-29
Statement description is not included in this imported ledger snapshot. See the PDF for the full theorem wording.
C-13-6-5-0known data2026-08-29
Statement description is not included in this imported ledger snapshot. See the PDF for the full theorem wording.
C-13-6-5-1known data2026-08-29
Statement description is not included in this imported ledger snapshot. See the PDF for the full theorem wording.
C-14-6-6-0known data2026-08-29
Statement description is not included in this imported ledger snapshot. See the PDF for the full theorem wording.
C-14-6-6-1known data2026-08-29
Statement description is not included in this imported ledger snapshot. See the PDF for the full theorem wording.
C-14-7-5-0known data2026-08-29
Statement description is not included in this imported ledger snapshot. See the PDF for the full theorem wording.
C-14-7-5-1known data2026-08-29
Statement description is not included in this imported ledger snapshot. See the PDF for the full theorem wording.
Provenance
- Generated by
- Machina Mathematica
- Released by
- Korea Superintelligence Labs
- Source context
- Litjens, Polak and Sivaraman call a graph G sum-perfect when every induced subgraph H satisfies α(H) + ω(H) ≥ n(H), and characterise the class by twenty-seven forbidden induced subgraphs (*Sum-perfect graphs*, arXiv:1710.07546, Discrete Applied Mathematics 259 (2019) 232–239). Twenty-four of the twenty-seven — their H₂, …, H₂₅ — are
- Snapshot
- 2026-09-07 03:53 UTC
- Ledger commit
801848d7