Certified reductions, structural theorems, and clean-room verification for $R(J_4,J_8)$
Let $J_t=K_t-e$, with ordinary subgraph containment. We consolidate a seven-phase investigation of the unresolved Ramsey number $R(J_4,J_8)$. The published, fully checkable interval remains $30\le R(J_4,J_8)\le32$. A corrected two-pivot reduction sends every hypothetical graph of order $30$ or $31$ to one of $359$ strengthened arithmetic roots and a terminal graph in $\mathcal R(J_4,J_6;s)$ with $s\le16$. We give a directly verified $29$-vertex lower-bound graph, exact attachment-profile criteria, cross-level capacity and defect identities, and band-specific obstruction and lifting theorems. Clean-room generation reproduces the complete terminal censuses at orders $10$, $11$, $12$, $15$, and $16$; in particular the order-$15$ census has $20{,}266$ canonical members and zero failures under independent membership checks. The main new human theorem proves that no graph in $\mathcal R(J_4,J_8;31)$ has minimum degree $11$; together with a binary rigidity theorem at order $30$, this gives human terminals for all eighteen original degree-eleven roots. Earlier exhaustive research computations remove $32$ further roots, but their negative leaves do not yet carry publication-grade proof objects. The current research frontier is therefore $309$ roots, while $341=309+32$ roots remain unresolved under the strict clean-room standard. Two independent exact encodings report that the stored $29$-vertex witness has no one-vertex extension; without a checked refutation and a classification of all order-$29$ graphs, this is evidence rather than an order-$30$ theorem. Thus the present paper records a certified structural advance and a reproducible proof architecture, not an exact-value claim.
Authors
- Guo Chen (ORCID: https://orcid.org/0009-0002-2910-376X)
Publication Details
- Journal
- Zenodo (CERN European Organization for Nuclear Research)
- Published
- 2026-07-22
- DOI
- https://doi.org/10.5281/zenodo.21497005
- Primary Topic
- Complexity and Algorithms in Graphs
- Type
- preprint