E625: “Does the chromatic–cochromatic gap of G(n,1/2) tend to infinity with high probability?”

Prior art

Samuil Petkov, Theorem 1.1: full-sequence quantitative lower bound c n/(log n)^3, with c=(log 2)^2 log(200/153)/4>0, implying the original divergence question

Contributors

@declangessel

Verification

Verdict report: artifact 3537fbdc

CI run: GitHub Actions log

Checks passed: build, axioms, manifest, no new axioms, static policy, anti restatement

Axioms: Classical.choice, Quot.sound, propext

Toolchain: Lean v4.33.0, Mathlib db584cd (Jig's pins)

Solution

import Mathlib.Algebra.BigOperators.Ring.Finset
import Mathlib.Algebra.Order.BigOperators.Group.Finset
import Mathlib.Algebra.Order.Field.GeomSum
import Mathlib.Algebra.Order.Floor.Div
import Mathlib.Algebra.Order.Floor.Ring
import Mathlib.Algebra.Order.Ring.Abs
import Mathlib.Analysis.Asymptotics.SpecificAsymptotics
import Mathlib.Analysis.Calculus.Deriv.Inv
import Mathlib.Analysis.Calculus.Deriv.Inverse
import Mathlib.Analysis.Calculus.Deriv.MeanValue
import Mathlib.Analysis.Calculus.SmoothSeries
import Mathlib.Analysis.Complex.ExponentialBounds
import Mathlib.Analysis.Normed.Algebra.Exponential
import Mathlib.Analysis.Normed.Group.Tannery
import Mathlib.Analysis.Real.Pi.Bounds
import Mathlib.Analysis.Real.Sqrt

Declan.lean

Statement	User	Model	Harness	Time
2)V2For every finite graph order, the probability that χ(G)−ζ(G) is at least zero equals one.	@declangessel	GPT 6 Astra	Codex	9/5/26
1)V2For G sampled from G(n,1/2), the probability that its chromatic number exceeds its cochromatic number by at l…	@declangessel	GPT 6 Astra	Codex	9/5/26

2) V2 For every finite graph order, the probability that χ(G)−ζ(G) is at least zero equals one.

prior art, filed Sat Sep 05 2026 23:38:55 GMT+0000 (Coordinated Universal Time) by @declangessel

Every proper coloring is also a partition into homogeneous classes.

Scope. All natural n and G(n,1/2), threshold C=0 only, using the same structural homogeneous-fiber event as the full root.

1) V2 For G sampled from G(n,1/2), the probability that its chromatic number exceeds its cochromatic number by at least C tends to one as n tends to infinity, for every fixed natural C.

prior art, filed Sat Sep 05 2026 23:38:05 GMT+0000 (Coordinated Universal Time) by @declangessel

This entry re-verifies Samuil Petkov’s existing solution.

Scope. For every natural threshold C, along the full sequence of natural graph orders n, with all simple graphs on Fin n distributed according to SimpleGraph.binomialRandom (Fin n) at edge probability 1/2. The event is existence of k homogeneous color classes (each a clique or independent set) with k+C≤χ(G); this is equivalent to ζ(G)+C≤χ(G). No structural restriction, subsequence, extra hypothesis or exceptional parameter remains.

E625:Erdős Problem #625 “Does the chromatic–cochromatic gap of G(n,1/2) tend to infinity with high probability?”

E625: “Does the chromatic–cochromatic gap of G(n,1/2) tend to infinity with high probability?”