ExampleConstruction: AI-adaptedVerification: AI-adaptedprecheck passaudited 2026-08-13

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

A parameter ledger for the high-girth, high-chromatic alteration proof

Example

For the targets $k = 2$ and $ℓ = 3$ , choose $n = 2^{60}, p = n^{- 5 / 6} = 2^{- 50}, s = n / 4 = 2^{58} .$ These parameters make both failure probabilities in the alteration proof less than $1 / 2$ .

Facts & Assumptions

Given: The explicit parameters in the Example.

[L1]

The expected number of cycles of length at most $3$ is at most $n^{3} p^{3} / 6$ (The expected number of cycles of length at most $ℓ$ in $G (n, p)$ ).

[L2]

$P (α (G (n, p)) \geq s) \leq \exp (s \log n - p (\binom{s}{2}))$ ( $P (α (G (n, p)) \geq s) \leq (\binom{n}{s}) (1 - p)^{(\binom{s}{2})} \leq n^{s} \exp (- p (\binom{s}{2}))$ for $s \leq n$ ).

[L3]

The exponential is strictly increasing and positive, $\exp (- x) = 1 / \exp (x)$ , $1 + x \leq \exp (x)$ , and the logarithm is the increasing inverse of the exponential with its product law (The real exponential function and the number $e$ by a power series, The natural logarithm as the inverse of the exponential function, Order, continuity, range, and the product, quotient, and reciprocal laws for the natural logarithm, $1 + x \leq \exp (x)$ for every real $x$ , hence $(1 - p)^{m} \leq \exp (- m p)$ , The exponential is positive and satisfies $\exp (- x) = 1 / \exp (x)$ , The exponential function is strictly increasing).

[L4]

Markov bounds nonnegative upper tails; the union bound controls finite unions; complements have complementary probabilities; and positive probability gives a witness (Markov's inequality on a finite probability space, The finite union bound, Normalization, nonnegativity, monotonicity, complements, and differences in a finite probability space, An event of positive probability in a finite probability space is nonempty).

[L5]

The high-girth alteration deletes one vertex per short cycle and compares the surviving order with the independence number (For all positive $k, ℓ$ , some finite graph has girth greater than $ℓ$ and chromatic number greater than $k$ ).

Verification

technique · constructive

1.1

Here $n^{3} p^{3} / 6 = n^{1 / 2} / 6$ , so [L4] at the threshold $n / 2$ bounds the short-cycle failure probability by $n^{- 1 / 2} / 3 < 1 / 2$ .

L1L4algebra

1.2

Since $p (s - 1) / 2 = 2^{- 51} (2^{58} - 1) > 127$ , while [L3] gives $\log n = 60 \log 2 \leq 60$ , one has $s \log n - p (\binom{s}{2}) = s (\log n - p (s - 1) / 2) < - 67 s < - 1$ . Thus [L2] and [L3] bound the independence failure probability by a number less than $\exp (- 1) = 1 / e \leq 1 / 2$ .

L2L3algebra

2.1

By [L4], the union of the two failure events has probability less than $1$ , so its complement has positive probability and contains a graph with fewer than $n / 2$ triangles and independence number below $n / 4$ . Delete one vertex per triangle. More than $n / 2$ vertices survive, no triangle survives, and any two-colouring would have an independent colour class larger than $n / 4$ .

step 1.1step 1.2L4L5construct

3.1

Hence the survivor has girth greater than $3$ and chromatic number greater than $2$ , with every integrality and strict inequality explicit.

step 2.1L5discharge-construct∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

49 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Y. Zhao, MIT 18.218 Probabilistic Method in Combinatorics, proof of Theorem 6.3 (standard reference, not scraped)