Quantitative critical-comb consequence
Lax54.CriticalCombInput · concepts/Lax54/CriticalCombInput.lean · lax-54
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Lemma
This statement combines Lemmas 3.1 and 4.3 with the choice of parameters in the proof of Theorem 4.4. There are integers and such that every -critical induced--free graph contains, either in or in its complement, a stable hubbed comb with teeth and for every block . The complementary alternative is required because Lemma 4.3 gives low maximum degree in either or its complement; both induced--freeness and -criticality are invariant under complementation.
Concept map
Evidence
Each proof establishes this claim relative to its assumptions.
In the paper
- page 11 of this submission's paper
Lean source view on GitHub
| 1 | import Lax54.GraphDefinitions |
| 2 | |
| 3 | /-! |
| 4 | --- |
| 5 | title: Quantitative critical-comb consequence |
| 6 | type: lemma |
| 7 | --- |
| 8 | This statement combines Lemmas 3.1 and 4.3 with the choice of parameters in |
| 9 | the proof of Theorem 4.4. There are integers and |
| 10 | such that every -critical induced--free graph |
| 11 | contains, either in or in its complement, a stable hubbed comb with |
| 12 | teeth and |
| 13 | for every block . The complementary alternative |
| 14 | is required because Lemma 4.3 gives low maximum degree in either or its |
| 15 | complement; both induced--freeness and -criticality are invariant |
| 16 | under complementation. |
| 17 | -/ |
| 18 | |
| 19 | open scoped SimpleGraph |
| 20 | |
| 21 | namespace Lax54.CriticalCombInput |
| 22 | |
| 23 | open Lax54.GraphDefinitions |
| 24 | |
| 25 | universe u |
| 26 | |
| 27 | /-- The quantitative critical-comb statement used in the proof of Theorem 4.4. -/ |
| 28 | axiom exists_critical_comb_parameters : |
| 29 | ∃ q A : ℕ, 3 ≤ q ∧ A ≤ 2 ^ (q - 2) ∧ |
| 30 | ∀ {V : Type u} [Fintype V] [DecidableEq V] (G : SimpleGraph V), |
| 31 | IsC5Free G → IsQCritical q G → |
| 32 | (∃ (t : ℕ) (C : StableHubComb G t), |
| 33 | 2 ≤ t ∧ |
| 34 | ∀ i : Fin t, Fintype.card V ≤ A * t ^ 2 * (C.block i).card) ∨ |
| 35 | (∃ (t : ℕ) (C : StableHubComb Gᶜ t), |
| 36 | 2 ≤ t ∧ |
| 37 | ∀ i : Fin t, Fintype.card V ≤ A * t ^ 2 * (C.block i).card) |
| 38 | |
| 39 | end Lax54.CriticalCombInput |
| 40 |
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments