Research notes on every problem, and a library of the papers behind them. Built from the open erdos repository.
Updated
A proof of the seven-cycle threshold
c7_homomorphic_cleaning: Regularity cleaning separates repeated colors on closed seven-walks and transfers the threshold question to weighted templates.
c7_joint_clique_mass: A constrained maximization and weighted Hajnal argument for the clique-mass bound used in the seven-cycle threshold proof.
c7_near_bipartite: The rainbow-color lower bound at o(n squared) edit distance from bipartite, with no minimum-degree assumption.
c7_near_regular: The rainbow-color lower bound when minimum degree is n/2 up to a lower-order error.
c7_palette_savings: The finite weighted-template inequality, using a functional palette lemma and the joint-clique mass bound.
c7_solution: The argument combines a joint-walk clique bound, palette savings, cleaning, and the near-Turán boundary cases.
The solution note combines the finite and graph arguments. Its dependencies are, in reading order, joint clique mass, palette savings, near-bipartite graphs, near-regular graphs, and seven-walk cleaning. The Lean account identifies the corresponding Lean modules and the successful targeted build in this repository. The argument is the branch of native claim L17, accepted at tier 2 on 2026-09-25 for the Lean sources and the statement as they stood on 2026-09-25T03:40:15Z (first carried by the default branch on 2026-09-28); the solution note states the standing of the prose proof, which remains author-recorded. Earlier research notes give context for routes considered before the proof.