Lax54.CriticalCombInput
Quantitative critical-comb consequence
concepts/Lax54/CriticalCombInput.lean · lax-54
No public endorsements yet.
Loading review…
Sign in with ORCIDConcept map
Evidence
Each proof establishes this claim relative to its assumptions.
Theorem
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.
Lean source view on GitHub
| 1 | import Lax54.GraphDefinitions |
| 2 | |
| 3 | /-! |
| 4 | --- |
| 5 | title: Quantitative critical-comb consequence |
| 6 | type: theorem |
| 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 |
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