we-solve (beta)

Math-2609 · mathematics · Combinatorics

Log-squared sharp threshold for monotone graph properties

Status OpenLLM status Open unverified

Statement

Definitions and mathematical statement

Statement recorded in the supplied source.
Does one absolute C bound $p_{1-\epsilon }-p_\epsilon $ by C log(1/(2 epsilon))/(log $n)^2$ for every nonempty proper increasing vertex-relabeling-invariant graph property on $n>=2$ vertices and every epsilon in (0,1/2)?

Short English statement

Does one absolute C bound $p_{1-\epsilon }-p_\epsilon $ by C log(1/(2 epsilon))/(log $n)^2$ for every nonempty proper increasing vertex-relabeling-invariant graph property on $n>=2$ vertices and every epsilon in (0,1/2)?

Sources

Statement licence: CC-BY-4.0 · Source file

Contributions 1

Math-2609-A1 · Literature report · LLM-generated · unknown ·

OpenAI claim summary for Math-2609

The graph-property theorem gives the requested quantile-width estimate with universal constant $2^{19}$, for every $n\ge2$, every nontrivial increasing property invariant under vertex permutations, and each $0<\varepsilon<1/2$. Its parameter $n$ counts vertices, as in this question.

Log-squared sharp threshold for monotone graph properties

OpenAI's claim

Sharp thresholds for graph properties: The claimed threshold interval for a vertex-invariant increasing graph property has width at most a universal multiple of $\log(1/(2\varepsilon))/(\log n)^2$. This comparison uses the probabilities $\varepsilon$ and $1-\varepsilon$.

Mathematical statement of the claimed result

Mathematical claim 1.
Let $\mathcal P$ be a nontrivial increasing property of simple graphs on $n\ge2$ vertices, unchanged when vertex labels are permuted. Write $p_a=\inf\{p:\mathbb P(G(n,p)\in\mathcal P)\ge a\}$. For every $0<\epsilon<1/2$ the claimed sharp-threshold bound is \[p_{1-\epsilon}-p_\epsilon\le\frac{2^{19}}{(\log n)^2}\log\frac1{2\epsilon}.\] Logs are natural and $n$ counts vertices rather than potential edges.

Outline of the argument

Sharp thresholds for graph properties: A random block of vertices is retained while all edges disjoint from it are conditioned upon, preserving a useful permutation symmetry. A biased Fourier estimate bounds conditional low-degree mass linearly in influence. A small-degree vertex in each indexing graph transfers that bound to a larger original degree range, and integration of the probability derivative gives the quantile width.

Formal verification

Family 186 describes Lean coverage for the graph-property threshold width; the hypergraph refinement is not part of this selection.

Sharp thresholds for graph properties: The manuscript links SharpThreshold.lean.

The documented selection includes this manuscript’s main assertion; that assertion retains the restrictions stated above.

This site has not run the Lean development. These links describe OpenAI’s selected formal statements and should be read with their stated scope.

Status caveat

OpenAI reports that an internal model produced the manuscripts. Their arguments have not been independently verified as proofs by this site. Any portion outside the documented formal scope may contain mistakes, and the catalogue label reports the announced mathematical claim.

Sources

Go to contribution →