proven
No public endorsements yet.
Loading review…
Sign in with ORCIDConcept map
Evidence
Each proof establishes this claim relative to its assumptions.
Theorem
Lemma 3.1 of the paper, with reciprocal integer parameters. Let . For every sufficiently large , every , and every lower bound , there is an exponent with the following property. If is -critical, , and for every , then contains a stable hubbed comb such that and for every block .
The absolute constant replaces the constant in the paper to accommodate the integral form of Theorem 2.1. Its value does not affect the Erdős–Hajnal conclusion.
Lean source view on GitHub
| 1 | import Lax54.GraphDefinitions |
| 2 | |
| 3 | /-! |
| 4 | --- |
| 5 | title: Stable hubbed comb in a critical graph |
| 6 | type: theorem |
| 7 | --- |
| 8 | Lemma 3.1 of the paper, with reciprocal integer parameters. Let |
| 9 | . For every sufficiently large , every , and every lower |
| 10 | bound , there is an exponent with the following |
| 11 | property. If is -critical, , and |
| 12 | for every , then contains a stable hubbed |
| 13 | comb such that and |
| 14 | for every block . |
| 15 | |
| 16 | The absolute constant replaces the constant in the paper to |
| 17 | accommodate the integral form of Theorem 2.1. Its value does not affect the |
| 18 | Erdős–Hajnal conclusion. |
| 19 | -/ |
| 20 | |
| 21 | namespace Lax54.KeyCombLemma |
| 22 | |
| 23 | open Lax54.GraphDefinitions |
| 24 | |
| 25 | universe u |
| 26 | |
| 27 | /-- The absolute constant in the integral form of the key comb lemma. -/ |
| 28 | def keyCombConstant : ℕ := 2 ^ 20 |
| 29 | |
| 30 | /-- A sufficient lower bound on the sparsity parameter for obtaining at least two teeth. -/ |
| 31 | def keySparsityThreshold : ℕ := 2 * keyCombConstant |
| 32 | |
| 33 | /-- Lemma 3.1, with reciprocal integer parameters and cleared denominators. -/ |
| 34 | axiom key_comb_lemma : |
| 35 | ∀ E D Q : ℕ, keySparsityThreshold ≤ E → 0 < D → |
| 36 | ∃ q : ℕ, 3 ≤ q ∧ Q ≤ q ∧ |
| 37 | ∀ {V : Type u} [Fintype V] [DecidableEq V] |
| 38 | (G : SimpleGraph V) [DecidableRel G.Adj] (X : Finset V), |
| 39 | IsQCritical q G → |
| 40 | Fintype.card V ≤ D * X.card → |
| 41 | (∀ x : {v : V // v ∈ X}, |
| 42 | E * (G.induce (X : Set V)).degree x < X.card) → |
| 43 | ∃ (t : ℕ) (C : StableHubComb G t), |
| 44 | E ≤ keyCombConstant * t ∧ |
| 45 | ∀ i : Fin t, |
| 46 | E * X.card ≤ keyCombConstant * t ^ 2 * (C.block i).card |
| 47 | |
| 48 | end Lax54.KeyCombLemma |
| 49 |
Community review
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above; your ORCID profile must share a public name.
0 comments