Superexponential lower bounds for multicolor triangle Ramsey numbers

Source: url:https://github.com/openai/ten-proofs Authors: OpenAI Status: verified Main declarations: ErdosProblems.MulticolourTriangleRamsey.erdos_problem_183_explicit Tags: extremal-combinatorics, ramsey-theory, graph-coloring, erdos-problems MSC: 05D10, 05C55

def ErdosProblems.MulticolourTriangleRamsey.TriangleFree {n k : ℕ} (C : SimpleGraph.TopEdgeLabeling (Fin n) (Fin k)) : Prop

An edge coloring in which every color class is triangle-free.

Equations

• ErdosProblems.MulticolourTriangleRamsey.TriangleFree C = ∀ (colour : Fin k), (SimpleGraph.EdgeLabeling.labelGraph C colour).CliqueFree 3

theorem ErdosProblems.MulticolourTriangleRamsey.labelGraph_pullback_embedding {U : Type u_1} {V : Type u_2} {K : Type u_3} (C : SimpleGraph.TopEdgeLabeling V K) (f : U ↪ V) (colour : K) : SimpleGraph.EdgeLabeling.labelGraph (C.pullback f) colour = SimpleGraph.comap (⇑f) (SimpleGraph.EdgeLabeling.labelGraph C colour)

theorem ErdosProblems.MulticolourTriangleRamsey.cliqueFree_pullback_embedding {U : Type u_1} {V : Type u_2} {K : Type u_3} (C : SimpleGraph.TopEdgeLabeling V K) (f : U ↪ V) (hC : ∀ (colour : K), (SimpleGraph.EdgeLabeling.labelGraph C colour).CliqueFree 3) (colour : K) : (SimpleGraph.EdgeLabeling.labelGraph (C.pullback f) colour).CliqueFree 3

theorem ErdosProblems.MulticolourTriangleRamsey.colorable_pullback_embedding {U : Type u_1} {V : Type u_2} {K : Type u_3} {j : ℕ} (C : SimpleGraph.TopEdgeLabeling V K) (f : U ↪ V) (colour : K) (hC : (SimpleGraph.EdgeLabeling.labelGraph C colour).Colorable j) : (SimpleGraph.EdgeLabeling.labelGraph (C.pullback f) colour).Colorable j

theorem ErdosProblems.MulticolourTriangleRamsey.cliqueFree_compRight_embedding {V : Type u_1} {K : Type u_2} {K' : Type u_3} (C : SimpleGraph.TopEdgeLabeling V K) (e : K ↪ K') (hC : ∀ (colour : K), (SimpleGraph.EdgeLabeling.labelGraph C colour).CliqueFree 3) (colour : K') : ((SimpleGraph.EdgeLabeling.compRight C ⇑e).labelGraph colour).CliqueFree 3

noncomputable def ErdosProblems.MulticolourTriangleRamsey.omittedColourEquiv (k : ℕ) (omitted : Fin (k + 1)) : { colour : Fin (k + 1) // colour ≠ omitted } ≃ Fin k

Identifies all colors except one distinguished color with Fin k.

Equations

• ErdosProblems.MulticolourTriangleRamsey.omittedColourEquiv k omitted = Fintype.equivFinOfCardEq ⋯

noncomputable def ErdosProblems.MulticolourTriangleRamsey.activeColourEquiv (N t : ℕ) (P : Finset (Fin N)) (hP : P.card = t) : Fin (N - t) ≃ { colour : Fin N // colour ∉ P }

Identifies the colors outside a palette of size t with Fin (N - t).

Equations

• ErdosProblems.MulticolourTriangleRamsey.activeColourEquiv N t P hP = (Fintype.equivFinOfCardEq ⋯).symm

noncomputable def ErdosProblems.MulticolourTriangleRamsey.activeColourPreimage (N t : ℕ) (P : Finset (Fin N)) (hP : P.card = t) (colour : Fin N) (hactive : colour ∉ P) : Fin (N - t)

The reduced-palette index of an active color.

Equations

• ErdosProblems.MulticolourTriangleRamsey.activeColourPreimage N t P hP colour hactive = (ErdosProblems.MulticolourTriangleRamsey.activeColourEquiv N t P hP).symm ⟨colour, hactive⟩

noncomputable def ErdosProblems.MulticolourTriangleRamsey.paletteRelabel {V : Type u_1} {N t : ℕ} (C : SimpleGraph.TopEdgeLabeling V (Fin (N - t))) (P : Finset (Fin N)) (hP : P.card = t) : SimpleGraph.TopEdgeLabeling V (Fin N)

Relabels a coloring on the active colors into the full palette.

Equations

• One or more equations did not get rendered due to their size.

theorem ErdosProblems.MulticolourTriangleRamsey.paletteRelabel_adj_iff {V : Type u_1} {N t : ℕ} (C : SimpleGraph.TopEdgeLabeling V (Fin (N - t))) (P : Finset (Fin N)) (hP : P.card = t) (colour : Fin N) (hactive : colour ∉ P) (u v : V) : (SimpleGraph.EdgeLabeling.labelGraph (paletteRelabel C P hP) colour).Adj u v ↔ (SimpleGraph.EdgeLabeling.labelGraph C (activeColourPreimage N t P hP colour hactive)).Adj u v

theorem ErdosProblems.MulticolourTriangleRamsey.paletteRelabel_missing_no_adj {V : Type u_1} {N t : ℕ} (C : SimpleGraph.TopEdgeLabeling V (Fin (N - t))) (P : Finset (Fin N)) (hP : P.card = t) (colour : Fin N) (hmissing : colour ∈ P) (u v : V) : ¬(SimpleGraph.EdgeLabeling.labelGraph (paletteRelabel C P hP) colour).Adj u v

noncomputable def ErdosProblems.MulticolourTriangleRamsey.paletteBlockLabel {V : Type u_1} {N t j : ℕ} (C : SimpleGraph.TopEdgeLabeling V (Fin (N - t))) (hC : ∀ (colour : Fin (N - t)), (SimpleGraph.EdgeLabeling.labelGraph C colour).Colorable j) (P : Finset (Fin N)) (hP : P.card = t) (colour : Fin N) (hactive : colour ∉ P) : V → Fin j

A proper vertex label inside one active-color block.

Equations

• ErdosProblems.MulticolourTriangleRamsey.paletteBlockLabel C hC P hP colour hactive v = (Classical.choice ⋯) v

theorem ErdosProblems.MulticolourTriangleRamsey.paletteBlockLabel_valid {V : Type u_1} {N t j : ℕ} (C : SimpleGraph.TopEdgeLabeling V (Fin (N - t))) (hC : ∀ (colour : Fin (N - t)), (SimpleGraph.EdgeLabeling.labelGraph C colour).Colorable j) (P : Finset (Fin N)) (hP : P.card = t) (colour : Fin N) (hactive : colour ∉ P) (u v : V) (hadj : (SimpleGraph.EdgeLabeling.labelGraph (paletteRelabel C P hP) colour).Adj u v) : paletteBlockLabel C hC P hP colour hactive u ≠ paletteBlockLabel C hC P hP colour hactive v

theorem ErdosProblems.MulticolourTriangleRamsey.paletteRelabel_cliqueFree {V : Type u_1} {N t : ℕ} (C : SimpleGraph.TopEdgeLabeling V (Fin (N - t))) (hC : ∀ (colour : Fin (N - t)), (SimpleGraph.EdgeLabeling.labelGraph C colour).CliqueFree 3) (P : Finset (Fin N)) (hP : P.card = t) (colour : Fin N) : (SimpleGraph.EdgeLabeling.labelGraph (paletteRelabel C P hP) colour).CliqueFree 3

noncomputable def ErdosProblems.MulticolourTriangleRamsey.deleteUnusedColour {V : Type u_1} {k : ℕ} (C : SimpleGraph.TopEdgeLabeling V (Fin (k + 1))) (omitted : Fin (k + 1)) (hunused : ∀ (edge : ↑⊤.edgeSet), C edge ≠ omitted) : SimpleGraph.TopEdgeLabeling V (Fin k)

Deletes a color that is unused by an edge coloring.

Equations

• ErdosProblems.MulticolourTriangleRamsey.deleteUnusedColour C omitted hunused edge = (ErdosProblems.MulticolourTriangleRamsey.omittedColourEquiv k omitted) ⟨C edge, ⋯⟩

theorem ErdosProblems.MulticolourTriangleRamsey.triangleFree_deleteUnusedColour {n k : ℕ} (C : SimpleGraph.TopEdgeLabeling (Fin n) (Fin (k + 1))) (omitted : Fin (k + 1)) (hunused : ∀ (edge : ↑⊤.edgeSet), C edge ≠ omitted) (hC : TriangleFree C) : TriangleFree (deleteUnusedColour C omitted hunused)

def ErdosProblems.MulticolourTriangleRamsey.ForcesMonochromaticTriangle (n k : ℕ) : Prop

Every k-coloring of the complete graph on n vertices has a monochromatic triangle.

Equations

• ErdosProblems.MulticolourTriangleRamsey.ForcesMonochromaticTriangle n k = ∀ (C : SimpleGraph.TopEdgeLabeling (Fin n) (Fin k)), ¬ErdosProblems.MulticolourTriangleRamsey.TriangleFree C

theorem ErdosProblems.MulticolourTriangleRamsey.forcesMonochromaticTriangle_mono {m n k : ℕ} (hmn : m ≤ n) (hm : ForcesMonochromaticTriangle m k) : ForcesMonochromaticTriangle n k

theorem ErdosProblems.MulticolourTriangleRamsey.forcesMonochromaticTriangle_zero : ForcesMonochromaticTriangle 2 0

theorem ErdosProblems.MulticolourTriangleRamsey.forcesMonochromaticTriangle_succ {n k : ℕ} (hn : ForcesMonochromaticTriangle n k) : ForcesMonochromaticTriangle (1 + (k + 1) * n) (k + 1)

theorem ErdosProblems.MulticolourTriangleRamsey.exists_forcesMonochromaticTriangle (k : ℕ) : ∃ (n : ℕ), ForcesMonochromaticTriangle n k

noncomputable def ErdosProblems.MulticolourTriangleRamsey.triangleRamseyNumber (k : ℕ) : ℕ

The least order forcing a monochromatic triangle in every k-edge-coloring.

Equations

• ErdosProblems.MulticolourTriangleRamsey.triangleRamseyNumber k = sInf {n : ℕ | ErdosProblems.MulticolourTriangleRamsey.ForcesMonochromaticTriangle n k}

theorem ErdosProblems.MulticolourTriangleRamsey.triangleRamseyNumber_forces (k : ℕ) : ForcesMonochromaticTriangle (triangleRamseyNumber k) k

theorem ErdosProblems.MulticolourTriangleRamsey.triangleRamseyNumber_succ_le (k : ℕ) : triangleRamseyNumber (k + 1) ≤ 1 + (k + 1) * triangleRamseyNumber k

theorem ErdosProblems.MulticolourTriangleRamsey.triangleRamseyNumber_factorial_upper (k : ℕ) : triangleRamseyNumber k ≤ 4 * k.factorial

theorem ErdosProblems.MulticolourTriangleRamsey.triangleFree_lt_triangleRamseyNumber {n k : ℕ} (C : SimpleGraph.TopEdgeLabeling (Fin n) (Fin k)) (hC : TriangleFree C) : n < triangleRamseyNumber k

theorem ErdosProblems.MulticolourTriangleRamsey.triangleRamseyNumber_mono {k l : ℕ} (hkl : k ≤ l) : triangleRamseyNumber k ≤ triangleRamseyNumber l

theorem ErdosProblems.MulticolourTriangleRamsey.no_three_pairwise_palette_disagreements {α : Type u_1} (P Q R : Finset α) (colour : α) (hPQ : (colour ∈ P) ≠ (colour ∈ Q)) (hQR : (colour ∈ Q) ≠ (colour ∈ R)) (hRP : (colour ∈ R) ≠ (colour ∈ P)) : False

noncomputable def ErdosProblems.MulticolourTriangleRamsey.differenceColourEmbedding {α : Type u_1} [DecidableEq α] (P Q : Finset α) {s : ℕ} (hcard : s ≤ (Q \ P).card) : Fin s ↪ α

Embeds a finite index set into the colors present in one palette but not another.

Equations

• ErdosProblems.MulticolourTriangleRamsey.differenceColourEmbedding P Q hcard = { toFun := fun (i : Fin s) => ↑(((Fin.castLEEmb hcard).trans (Q \ P).equivFin.symm.toEmbedding) i), inj' := ⋯ }

theorem ErdosProblems.MulticolourTriangleRamsey.differenceColourEmbedding_mem {α : Type u_1} [DecidableEq α] (P Q : Finset α) {s : ℕ} (hcard : s ≤ (Q \ P).card) (i : Fin s) : (differenceColourEmbedding P Q hcard) i ∈ Q \ P

def ErdosProblems.MulticolourTriangleRamsey.IsPaletteSeparated {α : Type u_1} [DecidableEq α] (s : ℕ) (family : Finset (Finset α)) : Prop

A palette family whose ordered differences all contain at least s colors.

Equations

• ErdosProblems.MulticolourTriangleRamsey.IsPaletteSeparated s family = ∀ P ∈ family, ∀ Q ∈ family, P ≠ Q → s ≤ (P \ Q).card

theorem ErdosProblems.MulticolourTriangleRamsey.paletteSeparated_insert {α : Type u_1} [DecidableEq α] {s : ℕ} {family : Finset (Finset α)} {P : Finset α} (hseparated : IsPaletteSeparated s family) (hequal : ∀ Q ∈ family, Q.card = P.card) (hfar : ∀ Q ∈ family, s ≤ (P \ Q).card) : IsPaletteSeparated s (insert P family)

theorem ErdosProblems.MulticolourTriangleRamsey.exists_maximal_separated_palette_cover {α : Type u_1} [DecidableEq α] (ambient : Finset (Finset α)) (s : ℕ) (hs : 0 < s) (hequal : ∀ P ∈ ambient, ∀ Q ∈ ambient, P.card = Q.card) : ∃ family ⊆ ambient, IsPaletteSeparated s family ∧ ∀ P ∈ ambient, ∃ Q ∈ family, (P \ Q).card < s

noncomputable def ErdosProblems.MulticolourTriangleRamsey.paletteBall {α : Type u_1} [DecidableEq α] (ambient : Finset (Finset α)) (Q : Finset α) (s : ℕ) : Finset (Finset α)

Palettes of fixed size whose one-sided distance from a center is below s.

Equations

• ErdosProblems.MulticolourTriangleRamsey.paletteBall ambient Q s = {P ∈ ambient | (P \ Q).card < s}

noncomputable def ErdosProblems.MulticolourTriangleRamsey.paletteShell (N t : ℕ) (Q : Finset (Fin N)) (d : ℕ) : Finset (Finset (Fin N))

The shell of t-element palettes at one-sided distance d from Q.

Equations

• ErdosProblems.MulticolourTriangleRamsey.paletteShell N t Q d = {P ∈ Finset.powersetCard t Finset.univ | (P \ Q).card = d}

noncomputable def ErdosProblems.MulticolourTriangleRamsey.paletteShellEmbedding (N t d : ℕ) (Q : Finset (Fin N)) (hQ : Q.card = t) : ↥(paletteShell N t Q d) ↪ ↥(Finset.powersetCard d Q) × ↥(Finset.powersetCard d (Finset.univ \ Q))

Encodes a palette shell by the elements removed from and added to its center.

Equations

• One or more equations did not get rendered due to their size.

theorem ErdosProblems.MulticolourTriangleRamsey.paletteShell_card_le (N t d : ℕ) (Q : Finset (Fin N)) (hQ : Q.card = t) : (paletteShell N t Q d).card ≤ t.choose d * (N - t).choose d

theorem ErdosProblems.MulticolourTriangleRamsey.palette_packing_card_le {α : Type u_1} [DecidableEq α] (ambient family : Finset (Finset α)) (s ballBound : ℕ) (hcover : ∀ P ∈ ambient, ∃ Q ∈ family, (P \ Q).card < s) (hball : ∀ Q ∈ family, (paletteBall ambient Q s).card ≤ ballBound) : ambient.card ≤ family.card * ballBound

theorem ErdosProblems.MulticolourTriangleRamsey.paletteBall_card_le_binomial_sum (N t s : ℕ) (Q : Finset (Fin N)) (hQ : Q.card = t) : (paletteBall (Finset.powersetCard t Finset.univ) Q s).card ≤ ∑ d ∈ Finset.range s, t.choose d * (N - t).choose d

theorem ErdosProblems.MulticolourTriangleRamsey.exists_separated_palette_packing (N t s : ℕ) (hs : 0 < s) : ∃ family ⊆ Finset.powersetCard t Finset.univ, IsPaletteSeparated s family ∧ N.choose t ≤ family.card * ∑ d ∈ Finset.range s, t.choose d * (N - t).choose d

def ErdosProblems.MulticolourTriangleRamsey.transversalCoordinateEmbedding (j t : ℕ) (choice : Fin t → Fin j) : Fin t ↪ Fin (j * t)

Embeds one selected coordinate from each of t blocks of width j.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def ErdosProblems.MulticolourTriangleRamsey.transversalPalette (j t : ℕ) (choice : Fin t → Fin j) : Finset (Fin (j * t))

The palette consisting of the selected coordinate in every block.

Equations

• ErdosProblems.MulticolourTriangleRamsey.transversalPalette j t choice = Finset.map (ErdosProblems.MulticolourTriangleRamsey.transversalCoordinateEmbedding j t choice) Finset.univ

noncomputable def ErdosProblems.MulticolourTriangleRamsey.transversalPaletteEmbedding (j t : ℕ) : (Fin t → Fin j) ↪ ↥(Finset.powersetCard t Finset.univ)

Embeds blockwise choices into their transversal palettes.

Equations

• One or more equations did not get rendered due to their size.

theorem ErdosProblems.MulticolourTriangleRamsey.stage_palette_numerator_bound (j t : ℕ) : j ^ t ≤ (j * t).choose t

theorem ErdosProblems.MulticolourTriangleRamsey.choose_le_choose_of_le_half {N d s : ℕ} (hds : d ≤ s) (hhalf : 2 * s ≤ N) : N.choose d ≤ N.choose s

theorem ErdosProblems.MulticolourTriangleRamsey.factorial_exp_lower (s : ℕ) (hs : 0 < s) : (↑s / Real.exp 1) ^ s ≤ ↑s.factorial

theorem ErdosProblems.MulticolourTriangleRamsey.choose_le_exp_mul_div_pow (N s : ℕ) (hs : 0 < s) : ↑(N.choose s) ≤ (Real.exp 1 * ↑N / ↑s) ^ s

theorem ErdosProblems.MulticolourTriangleRamsey.palette_binomial_sum_le (N t s : ℕ) (hhalf : 2 * s ≤ t) (htN : t ≤ N) : ∑ d ∈ Finset.range s, t.choose d * (N - t).choose d ≤ s * t.choose s * N.choose s

theorem ErdosProblems.MulticolourTriangleRamsey.exists_stage_palette_packing_binomial (j t s : ℕ) (hs : 0 < s) (hj : 0 < j) (hhalf : 2 * s ≤ t) : ∃ family ⊆ Finset.powersetCard t Finset.univ, IsPaletteSeparated s family ∧ j ^ t ≤ family.card * (s * t.choose s * (j * t).choose s)

theorem ErdosProblems.MulticolourTriangleRamsey.exists_stage_palette_packing_exp (j a s : ℕ) (hj : 0 < j) (ha : 2 ≤ a) (hs : 0 < s) : ∃ family ⊆ Finset.powersetCard (a * s) Finset.univ, IsPaletteSeparated s family ∧ ↑j ^ (a * s) ≤ ↑family.card * ↑s * (Real.exp 1 ^ 2 * ↑a ^ 2 * ↑j) ^ s

def ErdosProblems.MulticolourTriangleRamsey.IsCoordinateCovering {H s : ℕ} (f g : (Fin s → Fin H) → Fin s → Fin H) : Prop

Two transformations cover every input vector in at least one coordinate.

Equations

• ErdosProblems.MulticolourTriangleRamsey.IsCoordinateCovering f g = ∀ (x y : Fin s → Fin H), (∃ (d : Fin s), x d = f y d) ∨ ∃ (d : Fin s), y d = g x d

noncomputable def ErdosProblems.MulticolourTriangleRamsey.recursiveCrossColour {K : Type u_1} {H s : ℕ} (a b : Fin s ↪ K) (f g : (Fin s → Fin H) → Fin s → Fin H) (hcover : IsCoordinateCovering f g) (x y : Fin s → Fin H) : K

Selects a cross-block color from a coordinate-covering pair of transformations.

Equations

• One or more equations did not get rendered due to their size.

theorem ErdosProblems.MulticolourTriangleRamsey.recursiveCrossColour_spec {K : Type u_1} {H s : ℕ} (a b : Fin s ↪ K) (f g : (Fin s → Fin H) → Fin s → Fin H) (hcover : IsCoordinateCovering f g) (x y : Fin s → Fin H) : (∃ (d : Fin s), recursiveCrossColour a b f g hcover x y = a d ∧ x d = f y d) ∨ ∃ (d : Fin s), recursiveCrossColour a b f g hcover x y = b d ∧ y d = g x d

theorem ErdosProblems.MulticolourTriangleRamsey.recursiveCrossColour_changes_membership {K : Type u_1} [DecidableEq K] {H s : ℕ} (P Q : Finset K) (a b : Fin s ↪ K) (ha : ∀ (d : Fin s), a d ∈ Q \ P) (hb : ∀ (d : Fin s), b d ∈ P \ Q) (f g : (Fin s → Fin H) → Fin s → Fin H) (hcover : IsCoordinateCovering f g) (x y : Fin s → Fin H) : (recursiveCrossColour a b f g hcover x y ∈ P) ≠ (recursiveCrossColour a b f g hcover x y ∈ Q)

theorem ErdosProblems.MulticolourTriangleRamsey.recursiveCrossColour_same_left_coordinate {K : Type u_1} [DecidableEq K] {H s : ℕ} (P Q : Finset K) (a b : Fin s ↪ K) (_ha : ∀ (d : Fin s), a d ∈ Q \ P) (hb : ∀ (d : Fin s), b d ∈ P \ Q) (f g : (Fin s → Fin H) → Fin s → Fin H) (hcover : IsCoordinateCovering f g) (x x' y : Fin s → Fin H) (colour : K) (hactive : colour ∉ P) (hxy : recursiveCrossColour a b f g hcover x y = colour) (hx'y : recursiveCrossColour a b f g hcover x' y = colour) : ∃ (d : Fin s), colour = a d ∧ x d = x' d

theorem ErdosProblems.MulticolourTriangleRamsey.recursiveCrossColour_same_right_coordinate {K : Type u_1} [DecidableEq K] {H s : ℕ} (P Q : Finset K) (a b : Fin s ↪ K) (ha : ∀ (d : Fin s), a d ∈ Q \ P) (_hb : ∀ (d : Fin s), b d ∈ P \ Q) (f g : (Fin s → Fin H) → Fin s → Fin H) (hcover : IsCoordinateCovering f g) (x y y' : Fin s → Fin H) (colour : K) (hactive : colour ∉ Q) (hxy : recursiveCrossColour a b f g hcover x y = colour) (hxy' : recursiveCrossColour a b f g hcover x y' = colour) : ∃ (d : Fin s), colour = b d ∧ y d = y' d

noncomputable def ErdosProblems.MulticolourTriangleRamsey.paletteBlockVector {V : Type u_1} {N t j H s : ℕ} (C : SimpleGraph.TopEdgeLabeling V (Fin (N - t))) (hC : ∀ (colour : Fin (N - t)), (SimpleGraph.EdgeLabeling.labelGraph C colour).Colorable j) (hj : j ≤ H) (P : Finset (Fin N)) (hP : P.card = t) (colours : Fin s ↪ Fin N) (hcolours : ∀ (d : Fin s), colours d ∉ P) (u : V) : Fin s → Fin H

The vector of internal proper-coloring labels attached to a palette block vertex.

Equations

• ErdosProblems.MulticolourTriangleRamsey.paletteBlockVector C hC hj P hP colours hcolours u d = Fin.castLE hj (ErdosProblems.MulticolourTriangleRamsey.paletteBlockLabel C hC P hP (colours d) ⋯ u)

noncomputable def ErdosProblems.MulticolourTriangleRamsey.paletteCrossColour {V : Type u_1} {N t j H s : ℕ} (C : SimpleGraph.TopEdgeLabeling V (Fin (N - t))) (hC : ∀ (colour : Fin (N - t)), (SimpleGraph.EdgeLabeling.labelGraph C colour).Colorable j) (hj : j ≤ H) (P Q : Finset (Fin N)) (hP : P.card = t) (hQ : Q.card = t) (a b : Fin s ↪ Fin N) (ha : ∀ (d : Fin s), a d ∈ Q \ P) (hb : ∀ (d : Fin s), b d ∈ P \ Q) (f g : (Fin s → Fin H) → Fin s → Fin H) (hcover : IsCoordinateCovering f g) (u v : V) : Fin N

The color assigned to an edge crossing two palette blocks.

Equations

• One or more equations did not get rendered due to their size.

theorem ErdosProblems.MulticolourTriangleRamsey.paletteCrossColour_changes_membership {V : Type u_1} {N t j H s : ℕ} (C : SimpleGraph.TopEdgeLabeling V (Fin (N - t))) (hC : ∀ (colour : Fin (N - t)), (SimpleGraph.EdgeLabeling.labelGraph C colour).Colorable j) (hj : j ≤ H) (P Q : Finset (Fin N)) (hP : P.card = t) (hQ : Q.card = t) (a b : Fin s ↪ Fin N) (ha : ∀ (d : Fin s), a d ∈ Q \ P) (hb : ∀ (d : Fin s), b d ∈ P \ Q) (f g : (Fin s → Fin H) → Fin s → Fin H) (hcover : IsCoordinateCovering f g) (u v : V) : (paletteCrossColour C hC hj P Q hP hQ a b ha hb f g hcover u v ∈ P) ≠ (paletteCrossColour C hC hj P Q hP hQ a b ha hb f g hcover u v ∈ Q)

theorem ErdosProblems.MulticolourTriangleRamsey.paletteCrossColour_same_left_label {V : Type u_1} {N t j H s : ℕ} (C : SimpleGraph.TopEdgeLabeling V (Fin (N - t))) (hC : ∀ (colour : Fin (N - t)), (SimpleGraph.EdgeLabeling.labelGraph C colour).Colorable j) (hj : j ≤ H) (P Q : Finset (Fin N)) (hP : P.card = t) (hQ : Q.card = t) (a b : Fin s ↪ Fin N) (ha : ∀ (d : Fin s), a d ∈ Q \ P) (hb : ∀ (d : Fin s), b d ∈ P \ Q) (f g : (Fin s → Fin H) → Fin s → Fin H) (hcover : IsCoordinateCovering f g) (u u' v : V) (colour : Fin N) (hactive : colour ∉ P) (hu : paletteCrossColour C hC hj P Q hP hQ a b ha hb f g hcover u v = colour) (hu' : paletteCrossColour C hC hj P Q hP hQ a b ha hb f g hcover u' v = colour) : paletteBlockLabel C hC P hP colour hactive u = paletteBlockLabel C hC P hP colour hactive u'

theorem ErdosProblems.MulticolourTriangleRamsey.paletteCrossColour_same_right_label {V : Type u_1} {N t j H s : ℕ} (C : SimpleGraph.TopEdgeLabeling V (Fin (N - t))) (hC : ∀ (colour : Fin (N - t)), (SimpleGraph.EdgeLabeling.labelGraph C colour).Colorable j) (hj : j ≤ H) (P Q : Finset (Fin N)) (hP : P.card = t) (hQ : Q.card = t) (a b : Fin s ↪ Fin N) (ha : ∀ (d : Fin s), a d ∈ Q \ P) (hb : ∀ (d : Fin s), b d ∈ P \ Q) (f g : (Fin s → Fin H) → Fin s → Fin H) (hcover : IsCoordinateCovering f g) (u v v' : V) (colour : Fin N) (hactive : colour ∉ Q) (hv : paletteCrossColour C hC hj P Q hP hQ a b ha hb f g hcover u v = colour) (hv' : paletteCrossColour C hC hj P Q hP hQ a b ha hb f g hcover u v' = colour) : paletteBlockLabel C hC Q hQ colour hactive v = paletteBlockLabel C hC Q hQ colour hactive v'

structure ErdosProblems.MulticolourTriangleRamsey.PaletteBlockCertificate {I : Type u_1} {V : Type u_2} {K : Type u_3} [DecidableEq K] (C : SimpleGraph.TopEdgeLabeling (I × V) K) (j : ℕ) : Type (max (max u_1 u_2) u_3)

Data certifying that a blockwise edge coloring contains no monochromatic triangle.

• palette : I → Finset K

  The colors omitted from internal edges of each block.

• label (i : I) (colour : K) : colour ∉ self.palette i → V → Fin j

  A proper internal vertex coloring for every active color in a block.

• internal_no_triangle (i : I) (colour : K) (u v w : V) : ¬((SimpleGraph.EdgeLabeling.labelGraph C colour).Adj (i, u) (i, v) ∧ (SimpleGraph.EdgeLabeling.labelGraph C colour).Adj (i, u) (i, w) ∧ (SimpleGraph.EdgeLabeling.labelGraph C colour).Adj (i, v) (i, w))
• missing_has_no_internal_edge (i : I) (colour : K) : colour ∈ self.palette i → ∀ (u v : V), ¬(SimpleGraph.EdgeLabeling.labelGraph C colour).Adj (i, u) (i, v)
• internal_labels_proper (i : I) (colour : K) (hactive : colour ∉ self.palette i) (u v : V) : (SimpleGraph.EdgeLabeling.labelGraph C colour).Adj (i, u) (i, v) → self.label i colour hactive u ≠ self.label i colour hactive v
• cross_edge_changes_membership (i i' : I) (colour : K) (u v : V) : i ≠ i' → (SimpleGraph.EdgeLabeling.labelGraph C colour).Adj (i, u) (i', v) → (colour ∈ self.palette i) ≠ (colour ∈ self.palette i')
• cross_edges_force_equal_active_labels (i i' : I) (colour : K) (u u' v : V) (_hne : i ≠ i') (hactive : colour ∉ self.palette i) : (SimpleGraph.EdgeLabeling.labelGraph C colour).Adj (i, u) (i', v) → (SimpleGraph.EdgeLabeling.labelGraph C colour).Adj (i, u') (i', v) → self.label i colour hactive u = self.label i colour hactive u'

theorem ErdosProblems.MulticolourTriangleRamsey.PaletteBlockCertificate.noMonochromaticTriangle {I : Type u_1} {V : Type u_2} {K : Type u_3} [DecidableEq K] {C : SimpleGraph.TopEdgeLabeling (I × V) K} {j : ℕ} (certificate : PaletteBlockCertificate C j) (colour : K) : (SimpleGraph.EdgeLabeling.labelGraph C colour).CliqueFree 3

noncomputable def ErdosProblems.MulticolourTriangleRamsey.PaletteBlockCertificate.globalLabel {I : Type u_1} {V : Type u_2} {K : Type u_3} [DecidableEq K] {C : SimpleGraph.TopEdgeLabeling (I × V) K} {j : ℕ} (certificate : PaletteBlockCertificate C j) (colour : K) (x : I × V) : Fin (j + 1)

Extends the internal labels by a final label for omitted colors.

Equations

• certificate.globalLabel colour x = if h : colour ∈ certificate.palette x.1 then Fin.last j else (certificate.label x.1 colour h x.2).castSucc

theorem ErdosProblems.MulticolourTriangleRamsey.PaletteBlockCertificate.colourGraph_colorable {I : Type u_1} {V : Type u_2} {K : Type u_3} [DecidableEq K] {C : SimpleGraph.TopEdgeLabeling (I × V) K} {j : ℕ} (certificate : PaletteBlockCertificate C j) (colour : K) : (SimpleGraph.EdgeLabeling.labelGraph C colour).Colorable (j + 1)

noncomputable def ErdosProblems.MulticolourTriangleRamsey.paletteFamilyForwardList {N s : ℕ} (family : Finset (Finset (Fin N))) (hseparated : IsPaletteSeparated s family) (i i' : ↥family) (hne : i ≠ i') : Fin s ↪ Fin N

Lists s colors witnessing an ordered difference between two palettes.

Equations

• ErdosProblems.MulticolourTriangleRamsey.paletteFamilyForwardList family hseparated i i' hne = ErdosProblems.MulticolourTriangleRamsey.differenceColourEmbedding ↑i ↑i' ⋯

theorem ErdosProblems.MulticolourTriangleRamsey.paletteFamilyForwardList_mem {N s : ℕ} (family : Finset (Finset (Fin N))) (hseparated : IsPaletteSeparated s family) (i i' : ↥family) (hne : i ≠ i') (d : Fin s) : (paletteFamilyForwardList family hseparated i i' hne) d ∈ ↑i' \ ↑i

noncomputable def ErdosProblems.MulticolourTriangleRamsey.paletteFamilyCrossColour {V : Type u_1} {N t j H s : ℕ} (C : SimpleGraph.TopEdgeLabeling V (Fin (N - t))) (hC : ∀ (colour : Fin (N - t)), (SimpleGraph.EdgeLabeling.labelGraph C colour).Colorable j) (hj : j ≤ H) (family : Finset (Finset (Fin N))) (hcard : ∀ P ∈ family, P.card = t) (hseparated : IsPaletteSeparated s family) (f g : (Fin s → Fin H) → Fin s → Fin H) (hcover : IsCoordinateCovering f g) (i i' : ↥family) (hne : i ≠ i') (u v : V) : Fin N

Chooses a cross-block color from two separated palettes and coordinate vectors.

Equations

• One or more equations did not get rendered due to their size.

theorem ErdosProblems.MulticolourTriangleRamsey.paletteFamilyCrossColour_changes_membership {V : Type u_1} {N t j H s : ℕ} (C : SimpleGraph.TopEdgeLabeling V (Fin (N - t))) (hC : ∀ (colour : Fin (N - t)), (SimpleGraph.EdgeLabeling.labelGraph C colour).Colorable j) (hj : j ≤ H) (family : Finset (Finset (Fin N))) (hcard : ∀ P ∈ family, P.card = t) (hseparated : IsPaletteSeparated s family) (f g : (Fin s → Fin H) → Fin s → Fin H) (hcover : IsCoordinateCovering f g) (i i' : ↥family) (hne : i ≠ i') (u v : V) : (paletteFamilyCrossColour C hC hj family hcard hseparated f g hcover i i' hne u v ∈ ↑i) ≠ (paletteFamilyCrossColour C hC hj family hcard hseparated f g hcover i i' hne u v ∈ ↑i')

theorem ErdosProblems.MulticolourTriangleRamsey.paletteFamilyCrossColour_same_left_label {V : Type u_1} {N t j H s : ℕ} (C : SimpleGraph.TopEdgeLabeling V (Fin (N - t))) (hC : ∀ (colour : Fin (N - t)), (SimpleGraph.EdgeLabeling.labelGraph C colour).Colorable j) (hj : j ≤ H) (family : Finset (Finset (Fin N))) (hcard : ∀ P ∈ family, P.card = t) (hseparated : IsPaletteSeparated s family) (f g : (Fin s → Fin H) → Fin s → Fin H) (hcover : IsCoordinateCovering f g) (i i' : ↥family) (hne : i ≠ i') (u u' v : V) (colour : Fin N) (hactive : colour ∉ ↑i) (hu : paletteFamilyCrossColour C hC hj family hcard hseparated f g hcover i i' hne u v = colour) (hu' : paletteFamilyCrossColour C hC hj family hcard hseparated f g hcover i i' hne u' v = colour) : paletteBlockLabel C hC ↑i ⋯ colour hactive u = paletteBlockLabel C hC ↑i ⋯ colour hactive u'

theorem ErdosProblems.MulticolourTriangleRamsey.paletteFamilyCrossColour_same_right_label {V : Type u_1} {N t j H s : ℕ} (C : SimpleGraph.TopEdgeLabeling V (Fin (N - t))) (hC : ∀ (colour : Fin (N - t)), (SimpleGraph.EdgeLabeling.labelGraph C colour).Colorable j) (hj : j ≤ H) (family : Finset (Finset (Fin N))) (hcard : ∀ P ∈ family, P.card = t) (hseparated : IsPaletteSeparated s family) (f g : (Fin s → Fin H) → Fin s → Fin H) (hcover : IsCoordinateCovering f g) (i i' : ↥family) (hne : i ≠ i') (u v v' : V) (colour : Fin N) (hactive : colour ∉ ↑i') (hv : paletteFamilyCrossColour C hC hj family hcard hseparated f g hcover i i' hne u v = colour) (hv' : paletteFamilyCrossColour C hC hj family hcard hseparated f g hcover i i' hne u v' = colour) : paletteBlockLabel C hC ↑i' ⋯ colour hactive v = paletteBlockLabel C hC ↑i' ⋯ colour hactive v'

noncomputable def ErdosProblems.MulticolourTriangleRamsey.recursivePaletteEdgeColour {V : Type u_1} {N t j H s : ℕ} (C : SimpleGraph.TopEdgeLabeling V (Fin (N - t))) (hC : ∀ (colour : Fin (N - t)), (SimpleGraph.EdgeLabeling.labelGraph C colour).Colorable j) (hj : j ≤ H) (family : Finset (Finset (Fin N))) (hcard : ∀ P ∈ family, P.card = t) (hseparated : IsPaletteSeparated s family) (f g : (Fin s → Fin H) → Fin s → Fin H) (hcover : IsCoordinateCovering f g) (x y : ↥family × V) (hne : x ≠ y) : Fin N

Assigns colors recursively to edges between members of a palette family.

Equations

• One or more equations did not get rendered due to their size.

theorem ErdosProblems.MulticolourTriangleRamsey.recursivePaletteEdgeColour_symm {V : Type u_1} {N t j H s : ℕ} (C : SimpleGraph.TopEdgeLabeling V (Fin (N - t))) (hC : ∀ (colour : Fin (N - t)), (SimpleGraph.EdgeLabeling.labelGraph C colour).Colorable j) (hj : j ≤ H) (family : Finset (Finset (Fin N))) (hcard : ∀ P ∈ family, P.card = t) (hseparated : IsPaletteSeparated s family) (f g : (Fin s → Fin H) → Fin s → Fin H) (hcover : IsCoordinateCovering f g) (x y : ↥family × V) (hne : x ≠ y) : recursivePaletteEdgeColour C hC hj family hcard hseparated f g hcover y x ⋯ = recursivePaletteEdgeColour C hC hj family hcard hseparated f g hcover x y hne

noncomputable def ErdosProblems.MulticolourTriangleRamsey.recursivePaletteColouring {V : Type u_1} {N t j H s : ℕ} (C : SimpleGraph.TopEdgeLabeling V (Fin (N - t))) (hC : ∀ (colour : Fin (N - t)), (SimpleGraph.EdgeLabeling.labelGraph C colour).Colorable j) (hj : j ≤ H) (family : Finset (Finset (Fin N))) (hcard : ∀ P ∈ family, P.card = t) (hseparated : IsPaletteSeparated s family) (f g : (Fin s → Fin H) → Fin s → Fin H) (hcover : IsCoordinateCovering f g) : SimpleGraph.TopEdgeLabeling (↥family × V) (Fin N)

The complete edge coloring assembled recursively from a palette family.

Equations

• One or more equations did not get rendered due to their size.

theorem ErdosProblems.MulticolourTriangleRamsey.recursivePaletteColouring_get {V : Type u_1} {N t j H s : ℕ} (C : SimpleGraph.TopEdgeLabeling V (Fin (N - t))) (hC : ∀ (colour : Fin (N - t)), (SimpleGraph.EdgeLabeling.labelGraph C colour).Colorable j) (hj : j ≤ H) (family : Finset (Finset (Fin N))) (hcard : ∀ P ∈ family, P.card = t) (hseparated : IsPaletteSeparated s family) (f g : (Fin s → Fin H) → Fin s → Fin H) (hcover : IsCoordinateCovering f g) (x y : ↥family × V) (hne : x ≠ y) : SimpleGraph.EdgeLabeling.get (recursivePaletteColouring C hC hj family hcard hseparated f g hcover) x y hne = recursivePaletteEdgeColour C hC hj family hcard hseparated f g hcover x y hne

theorem ErdosProblems.MulticolourTriangleRamsey.recursivePaletteColouring_internal_adj_iff {V : Type u_1} {N t j H s : ℕ} (C : SimpleGraph.TopEdgeLabeling V (Fin (N - t))) (hC : ∀ (colour : Fin (N - t)), (SimpleGraph.EdgeLabeling.labelGraph C colour).Colorable j) (hj : j ≤ H) (family : Finset (Finset (Fin N))) (hcard : ∀ P ∈ family, P.card = t) (hseparated : IsPaletteSeparated s family) (f g : (Fin s → Fin H) → Fin s → Fin H) (hcover : IsCoordinateCovering f g) (i : ↥family) (colour : Fin N) (u v : V) : (SimpleGraph.EdgeLabeling.labelGraph (recursivePaletteColouring C hC hj family hcard hseparated f g hcover) colour).Adj (i, u) (i, v) ↔ (SimpleGraph.EdgeLabeling.labelGraph (paletteRelabel C ↑i ⋯) colour).Adj u v

theorem ErdosProblems.MulticolourTriangleRamsey.recursivePaletteColouring_cross_adj_iff_of_lt {V : Type u_1} {N t j H s : ℕ} (C : SimpleGraph.TopEdgeLabeling V (Fin (N - t))) (hC : ∀ (colour : Fin (N - t)), (SimpleGraph.EdgeLabeling.labelGraph C colour).Colorable j) (hj : j ≤ H) (family : Finset (Finset (Fin N))) (hcard : ∀ P ∈ family, P.card = t) (hseparated : IsPaletteSeparated s family) (f g : (Fin s → Fin H) → Fin s → Fin H) (hcover : IsCoordinateCovering f g) (i i' : ↥family) (hne : i ≠ i') (horder : family.equivFin i < family.equivFin i') (colour : Fin N) (u v : V) : (SimpleGraph.EdgeLabeling.labelGraph (recursivePaletteColouring C hC hj family hcard hseparated f g hcover) colour).Adj (i, u) (i', v) ↔ paletteFamilyCrossColour C hC hj family hcard hseparated f g hcover i i' hne u v = colour

theorem ErdosProblems.MulticolourTriangleRamsey.paletteFamily_reverse_rank_lt {N : ℕ} (family : Finset (Finset (Fin N))) (i i' : ↥family) (hne : i ≠ i') (hnot : ¬family.equivFin i < family.equivFin i') : family.equivFin i' < family.equivFin i

noncomputable def ErdosProblems.MulticolourTriangleRamsey.recursivePaletteCertificate {V : Type u_1} {N t j H s : ℕ} (C : SimpleGraph.TopEdgeLabeling V (Fin (N - t))) (htriangle : ∀ (colour : Fin (N - t)), (SimpleGraph.EdgeLabeling.labelGraph C colour).CliqueFree 3) (hC : ∀ (colour : Fin (N - t)), (SimpleGraph.EdgeLabeling.labelGraph C colour).Colorable j) (hj : j ≤ H) (family : Finset (Finset (Fin N))) (hcard : ∀ P ∈ family, P.card = t) (hseparated : IsPaletteSeparated s family) (f g : (Fin s → Fin H) → Fin s → Fin H) (hcover : IsCoordinateCovering f g) : PaletteBlockCertificate (recursivePaletteColouring C hC hj family hcard hseparated f g hcover) j

The triangle-free certificate for the recursive palette coloring.

Equations

• One or more equations did not get rendered due to their size.

def ErdosProblems.MulticolourTriangleRamsey.IsSaturated {H m s : ℕ} (A : Fin s → (Fin m → Fin H) → Fin H) : Prop

Every word is matched in some coordinate by at least s rows of a matrix.

Equations

• ErdosProblems.MulticolourTriangleRamsey.IsSaturated A = ∀ (T : Finset (Fin m → Fin H)), T.card = m + 1 → ∃ (row : Fin s), ∀ (symbol : Fin H), ∃ column ∈ T, A row column = symbol

def ErdosProblems.MulticolourTriangleRamsey.RowCovers {H m : ℕ} (T : Finset (Fin m → Fin H)) (row : (Fin m → Fin H) → Fin H) : Prop

A matrix row agrees with a word in at least one coordinate.

Equations

• ErdosProblems.MulticolourTriangleRamsey.RowCovers T row = ∀ (symbol : Fin H), ∃ column ∈ T, row column = symbol

noncomputable def ErdosProblems.MulticolourTriangleRamsey.badSaturationRows (H m : ℕ) (T : Finset (Fin m → Fin H)) : Finset ((Fin m → Fin H) → Fin H)

Rows that fail to cover a fixed word.

Equations

• ErdosProblems.MulticolourTriangleRamsey.badSaturationRows H m T = {row : (Fin m → Fin H) → Fin H | ¬ErdosProblems.MulticolourTriangleRamsey.RowCovers T row}

noncomputable def ErdosProblems.MulticolourTriangleRamsey.missingSymbolRows (H m : ℕ) (T : Finset (Fin m → Fin H)) (symbol : Fin H) : Finset ((Fin m → Fin H) → Fin H)

Rows omitting a chosen symbol from all coordinates.

Equations

• ErdosProblems.MulticolourTriangleRamsey.missingSymbolRows H m T symbol = Fintype.piFinset fun (column : Fin m → Fin H) => if column ∈ T then Finset.univ.erase symbol else Finset.univ

theorem ErdosProblems.MulticolourTriangleRamsey.mem_missingSymbolRows (H m : ℕ) (T : Finset (Fin m → Fin H)) (symbol : Fin H) (row : (Fin m → Fin H) → Fin H) : row ∈ missingSymbolRows H m T symbol ↔ ∀ column ∈ T, row column ≠ symbol

theorem ErdosProblems.MulticolourTriangleRamsey.card_missingSymbolRows (H m : ℕ) (T : Finset (Fin m → Fin H)) (symbol : Fin H) : (missingSymbolRows H m T symbol).card = (H - 1) ^ T.card * H ^ (H ^ m - T.card)

theorem ErdosProblems.MulticolourTriangleRamsey.card_badSaturationRows_le (H m : ℕ) (T : Finset (Fin m → Fin H)) : (badSaturationRows H m T).card ≤ H * ((H - 1) ^ T.card * H ^ (H ^ m - T.card))

theorem ErdosProblems.MulticolourTriangleRamsey.missing_symbol_power_bound (H m : ℕ) (hH : 2 ≤ H) (hm : 2 * ↑H * Real.log ↑H ≤ ↑m) : ↑H ^ 2 * (↑H - 1) ^ (m + 1) < ↑H ^ (m + 1)

theorem ErdosProblems.MulticolourTriangleRamsey.missing_symbol_power_bound_nat (H m : ℕ) (hH : 2 ≤ H) (hm : 2 * ↑H * Real.log ↑H ≤ ↑m) : H ^ 2 * (H - 1) ^ (m + 1) < H ^ (m + 1)

theorem ErdosProblems.MulticolourTriangleRamsey.card_badSaturationRows_mul_lt (H m : ℕ) (hH : 2 ≤ H) (hm : 2 * ↑H * Real.log ↑H ≤ ↑m) (T : Finset (Fin m → Fin H)) (hT : T.card = m + 1) : (badSaturationRows H m T).card * H < H ^ H ^ m

theorem ErdosProblems.MulticolourTriangleRamsey.card_badSaturationRows_lt_pow (H m : ℕ) (hH : 2 ≤ H) (hm : 2 * ↑H * Real.log ↑H ≤ ↑m) (T : Finset (Fin m → Fin H)) (hT : T.card = m + 1) : (badSaturationRows H m T).card < H ^ (H ^ m - 1)

noncomputable def ErdosProblems.MulticolourTriangleRamsey.badSaturationMatrices (H m s : ℕ) (T : Finset (Fin m → Fin H)) : Finset (Fin s → (Fin m → Fin H) → Fin H)

Matrices for which some word is covered by fewer than s rows.

Equations

• ErdosProblems.MulticolourTriangleRamsey.badSaturationMatrices H m s T = Fintype.piFinset fun (x : Fin s) => ErdosProblems.MulticolourTriangleRamsey.badSaturationRows H m T

theorem ErdosProblems.MulticolourTriangleRamsey.card_badSaturationMatrices (H m s : ℕ) (T : Finset (Fin m → Fin H)) : (badSaturationMatrices H m s T).card = (badSaturationRows H m T).card ^ s

theorem ErdosProblems.MulticolourTriangleRamsey.exists_saturated_of_bad_row_union_bound (H m s : ℕ) (hbound : ∑ T ∈ Finset.powersetCard (m + 1) Finset.univ, (badSaturationRows H m T).card ^ s < Fintype.card (Fin s → (Fin m → Fin H) → Fin H)) : ∃ (A : Fin s → (Fin m → Fin H) → Fin H), IsSaturated A

theorem ErdosProblems.MulticolourTriangleRamsey.exists_saturated_matrix (H m : ℕ) (hH : 2 ≤ H) (hm : 2 * ↑H * Real.log ↑H ≤ ↑m) : ∃ (A : Fin (m * (m + 1) + 1) → (Fin m → Fin H) → Fin H), IsSaturated A

noncomputable def ErdosProblems.MulticolourTriangleRamsey.saturatedMatrixWidth (H : ℕ) : ℕ

The width parameter used for the saturated-matrix construction.

Equations

• ErdosProblems.MulticolourTriangleRamsey.saturatedMatrixWidth H = ⌈2 * ↑H * Real.log ↑H⌉₊

noncomputable def ErdosProblems.MulticolourTriangleRamsey.saturatedMatrixRows (H : ℕ) : ℕ

The row-count parameter used for the saturated-matrix construction.

Equations

• One or more equations did not get rendered due to their size.

theorem ErdosProblems.MulticolourTriangleRamsey.exists_saturated_matrix_ceil (H : ℕ) (hH : 2 ≤ H) : ∃ (A : Fin (saturatedMatrixRows H) → (Fin (saturatedMatrixWidth H) → Fin H) → Fin H), IsSaturated A

noncomputable def ErdosProblems.MulticolourTriangleRamsey.exceptionalColumns {H m s : ℕ} (A : Fin s → (Fin m → Fin H) → Fin H) (y : Fin s → Fin H) : Finset (Fin m → Fin H)

Columns on which a matrix row differs from a prescribed word.

Equations

• ErdosProblems.MulticolourTriangleRamsey.exceptionalColumns A y = {z : Fin m → Fin H | ∀ (row : Fin s), A row z ≠ y row}

theorem ErdosProblems.MulticolourTriangleRamsey.mem_exceptionalColumns {H m s : ℕ} (A : Fin s → (Fin m → Fin H) → Fin H) (y : Fin s → Fin H) (z : Fin m → Fin H) : z ∈ exceptionalColumns A y ↔ ∀ (row : Fin s), A row z ≠ y row

theorem ErdosProblems.MulticolourTriangleRamsey.card_exceptionalColumns_le {H m s : ℕ} (A : Fin s → (Fin m → Fin H) → Fin H) (hA : IsSaturated A) (y : Fin s → Fin H) : (exceptionalColumns A y).card ≤ m

noncomputable def ErdosProblems.MulticolourTriangleRamsey.exceptionalColumnIndex {H m s : ℕ} (A : Fin s → (Fin m → Fin H) → Fin H) (hA : IsSaturated A) (y : Fin s → Fin H) : ↥(exceptionalColumns A y) ↪ Fin m

An enumeration of the exceptional columns for one row.

Equations

• ErdosProblems.MulticolourTriangleRamsey.exceptionalColumnIndex A hA y = (ErdosProblems.MulticolourTriangleRamsey.exceptionalColumns A y).equivFin.toEmbedding.trans (Fin.castLEEmb ⋯)

def ErdosProblems.MulticolourTriangleRamsey.backwardGuess {H m s : ℕ} (A : Fin s → (Fin m → Fin H) → Fin H) (hms : m ≤ s) (x : Fin s → Fin H) : Fin s → Fin H

A word obtained by reading one selected matrix row.

Equations

• ErdosProblems.MulticolourTriangleRamsey.backwardGuess A hms x row = A row fun (coordinate : Fin m) => x (Fin.castLE hms coordinate)

noncomputable def ErdosProblems.MulticolourTriangleRamsey.forwardGuess {H m s : ℕ} (A : Fin s → (Fin m → Fin H) → Fin H) (hA : IsSaturated A) (hH : 0 < H) (hms : m ≤ s) (y : Fin s → Fin H) (row : Fin s) : Fin H

A word chosen to disagree with a target on its exceptional columns.

Equations

• One or more equations did not get rendered due to their size.

theorem ErdosProblems.MulticolourTriangleRamsey.saturated_coordinate_covering {H m s : ℕ} (A : Fin s → (Fin m → Fin H) → Fin H) (hA : IsSaturated A) (hH : 0 < H) (hms : m ≤ s) : ∃ (f : (Fin s → Fin H) → Fin s → Fin H) (g : (Fin s → Fin H) → Fin s → Fin H), ∀ (x y : Fin s → Fin H), (∃ (row : Fin s), x row = f y row) ∨ ∃ (row : Fin s), y row = g x row

theorem ErdosProblems.MulticolourTriangleRamsey.exists_coordinate_covering (H : ℕ) (hH : 2 ≤ H) : ∃ (f : (Fin (saturatedMatrixRows H) → Fin H) → Fin (saturatedMatrixRows H) → Fin H) (g : (Fin (saturatedMatrixRows H) → Fin H) → Fin (saturatedMatrixRows H) → Fin H), IsCoordinateCovering f g

theorem ErdosProblems.MulticolourTriangleRamsey.exists_recursivePaletteColouring_fin {n N t j H : ℕ} (C : SimpleGraph.TopEdgeLabeling (Fin n) (Fin (N - t))) (htriangle : ∀ (colour : Fin (N - t)), (SimpleGraph.EdgeLabeling.labelGraph C colour).CliqueFree 3) (hC : ∀ (colour : Fin (N - t)), (SimpleGraph.EdgeLabeling.labelGraph C colour).Colorable j) (hH : 2 ≤ H) (hj : j ≤ H) (family : Finset (Finset (Fin N))) (hcard : ∀ P ∈ family, P.card = t) (hseparated : IsPaletteSeparated (saturatedMatrixRows H) family) : ∃ (C' : SimpleGraph.TopEdgeLabeling (Fin (family.card * n)) (Fin N)), TriangleFree C' ∧ ∀ (colour : Fin N), (SimpleGraph.EdgeLabeling.labelGraph C' colour).Colorable (j + 1)

def ErdosProblems.MulticolourTriangleRamsey.singletonZeroColouring : SimpleGraph.TopEdgeLabeling (Fin 1) (Fin 0)

The unique edge coloring of a singleton vertex set with color zero.

Equations

• ErdosProblems.MulticolourTriangleRamsey.singletonZeroColouring edge = ⋯.elim

def ErdosProblems.MulticolourTriangleRamsey.PaletteGrowthBound (a s j n : ℕ) : Prop

A stagewise lower bound on the size of a recursively constructed coloring.

Equations

• ErdosProblems.MulticolourTriangleRamsey.PaletteGrowthBound a s j n = (↑j.factorial ^ (a * s) ≤ ↑n * ↑s ^ j * (Real.exp 1 ^ 2 * ↑a ^ 2) ^ (s * j) * ↑j.factorial ^ s)

theorem ErdosProblems.MulticolourTriangleRamsey.paletteGrowthBound_succ {a s j n B : ℕ} (hstage : ↑(j + 1) ^ (a * s) ≤ ↑B * ↑s * (Real.exp 1 ^ 2 * ↑a ^ 2 * ↑(j + 1)) ^ s) (hprevious : PaletteGrowthBound a s j n) : PaletteGrowthBound a s (j + 1) (B * n)

theorem ErdosProblems.MulticolourTriangleRamsey.exists_recursivePaletteStage (H a j : ℕ) (hH : 2 ≤ H) (ha : 2 ≤ a) (hj : j ≤ H) : ∃ (n : ℕ) (C : SimpleGraph.TopEdgeLabeling (Fin n) (Fin (j * (a * saturatedMatrixRows H)))), TriangleFree C ∧ (∀ (colour : Fin (j * (a * saturatedMatrixRows H))), (SimpleGraph.EdgeLabeling.labelGraph C colour).Colorable (j + 1)) ∧ PaletteGrowthBound a (saturatedMatrixRows H) j n

theorem ErdosProblems.MulticolourTriangleRamsey.palette_exp_loss_bound (H a s : ℕ) (hH : 2 ≤ H) (ha : 2 ≤ a) (hs : 0 < s) (hlogH : Real.log ↑H ≤ ↑a) : (↑H / Real.exp 4) ^ (H * (a * s)) ≤ (↑H / Real.exp 1) ^ (H * ((a - 1) * s)) / (↑s ^ H * (Real.exp 1 ^ 2 * ↑a ^ 2) ^ (s * H))

theorem ErdosProblems.MulticolourTriangleRamsey.recursivePaletteRamsey_exponential_bound (H a : ℕ) (hH : 2 ≤ H) (ha : 2 ≤ a) (hloga : Real.log ↑H ≤ ↑a) : (↑H / Real.exp 4) ^ (H * (a * saturatedMatrixRows H)) ≤ ↑(triangleRamseyNumber (H * (a * saturatedMatrixRows H)))

noncomputable def ErdosProblems.MulticolourTriangleRamsey.paletteLogWidth (H : ℕ) : ℕ

The logarithmic block width at stage H.

Equations

• ErdosProblems.MulticolourTriangleRamsey.paletteLogWidth H = max 2 ⌈Real.log ↑H⌉₊

noncomputable def ErdosProblems.MulticolourTriangleRamsey.paletteColourCount (H : ℕ) : ℕ

The cumulative number of colors available through stage H.

Equations

• One or more equations did not get rendered due to their size.

theorem ErdosProblems.MulticolourTriangleRamsey.paletteLogWidth_two_le (H : ℕ) : 2 ≤ paletteLogWidth H

theorem ErdosProblems.MulticolourTriangleRamsey.log_le_paletteLogWidth (H : ℕ) : Real.log ↑H ≤ ↑(paletteLogWidth H)

theorem ErdosProblems.MulticolourTriangleRamsey.stageWidths_succ_le (H : ℕ) (hH : 1 ≤ H) : paletteLogWidth (H + 1) ≤ paletteLogWidth H + 1 ∧ saturatedMatrixWidth (H + 1) ≤ saturatedMatrixWidth H + 2 * paletteLogWidth H + 4

theorem ErdosProblems.MulticolourTriangleRamsey.one_le_log_nat_of_three_le (H : ℕ) (hH : 3 ≤ H) : 1 ≤ Real.log ↑H

theorem ErdosProblems.MulticolourTriangleRamsey.paletteLogWidth_le_two_log (H : ℕ) (hH : 3 ≤ H) : ↑(paletteLogWidth H) ≤ 2 * Real.log ↑H

theorem ErdosProblems.MulticolourTriangleRamsey.paletteLogWidth_le_stage (H : ℕ) (hH : 2 ≤ H) : paletteLogWidth H ≤ H

theorem ErdosProblems.MulticolourTriangleRamsey.paletteColourCount_mono {H H' : ℕ} (hH : 1 ≤ H) (hHH' : H ≤ H') : paletteColourCount H ≤ paletteColourCount H'

theorem ErdosProblems.MulticolourTriangleRamsey.two_mul_stage_le_paletteColourCount (H : ℕ) : 2 * H ≤ paletteColourCount H

theorem ErdosProblems.MulticolourTriangleRamsey.exists_paletteStage_bracket (k : ℕ) (hk : paletteColourCount 2 ≤ k) : ∃ (H : ℕ), 2 ≤ H ∧ paletteColourCount H ≤ k ∧ k < paletteColourCount (H + 1)

theorem ErdosProblems.MulticolourTriangleRamsey.stage_mul_paletteWidth_le_matrixWidth_sharp (H : ℕ) (hH : 3 ≤ H) : H * paletteLogWidth H ≤ saturatedMatrixWidth H

theorem ErdosProblems.MulticolourTriangleRamsey.saturatedMatrixRows_adjacent_scaled_sharp (H : ℕ) (hH : 3 ≤ H) : H * saturatedMatrixRows (H + 1) ≤ (H + 14) * saturatedMatrixRows H

theorem ErdosProblems.MulticolourTriangleRamsey.paletteColourCount_adjacent_scaled_sharp (H : ℕ) (hH : 3 ≤ H) : paletteLogWidth H * paletteColourCount (H + 1) ≤ (paletteLogWidth H + 34) * paletteColourCount H

theorem ErdosProblems.MulticolourTriangleRamsey.palette_exponential_adjacent_transfer_sharp (H a k₀ k : ℕ) (hH : 3 ≤ H) (hlog : Real.log ↑H ≤ ↑a) (hk₀ : k₀ ≤ k) (hratio : a * k ≤ (a + 34) * k₀) : (↑H / Real.exp 38) ^ k ≤ (↑H / Real.exp 4) ^ k₀

theorem ErdosProblems.MulticolourTriangleRamsey.allColourPaletteRamsey_exponential_bound_sharp (k : ℕ) (hk : paletteColourCount 3 ≤ k) : ∃ (H : ℕ), 3 ≤ H ∧ paletteColourCount H ≤ k ∧ k < paletteColourCount (H + 1) ∧ (↑H / Real.exp 38) ^ k ≤ ↑(triangleRamseyNumber k)

theorem ErdosProblems.MulticolourTriangleRamsey.paletteColourCount_le_twenty_six_sharp (H : ℕ) (hH : 3 ≤ H) : ↑(paletteColourCount H) ≤ 26 * ↑H ^ 3 * Real.log ↑H ^ 3

theorem ErdosProblems.MulticolourTriangleRamsey.paletteStage_cube_root_control_six_sharp (H k : ℕ) (hH : 3 ≤ H) (hlower : paletteColourCount H ≤ k) (hupper : k < paletteColourCount (H + 1)) : ↑k ^ (1 / 3) ≤ 6 * ↑H * Real.log ↑k

theorem ErdosProblems.MulticolourTriangleRamsey.paletteColourCount_three : paletteColourCount 3 = 342

theorem ErdosProblems.MulticolourTriangleRamsey.quantitativeLowerBound_explicit_small (k : ℕ) (hk : 2 ≤ k) (hsmall : k < 342) : (1 / (6 * Real.exp 38) * ↑k ^ (1 / 3) / Real.log ↑k) ^ k ≤ ↑(triangleRamseyNumber k)

theorem ErdosProblems.MulticolourTriangleRamsey.quantitativeLowerBound_explicit_all (k : ℕ) : 2 ≤ k → (1 / (6 * Real.exp 38) * ↑k ^ (1 / 3) / Real.log ↑k) ^ k ≤ ↑(triangleRamseyNumber k)

theorem ErdosProblems.MulticolourTriangleRamsey.triangleRamseyNumber_log_sharp_coefficients (ε : ℝ) : 0 < ε → ∀ᶠ (k : ℕ) in Filter.atTop, (1 / 3 - ε) * ↑k * Real.log ↑k ≤ Real.log ↑(triangleRamseyNumber k) ∧ Real.log ↑(triangleRamseyNumber k) ≤ (1 + ε) * ↑k * Real.log ↑k

theorem ErdosProblems.MulticolourTriangleRamsey.triangleRamseyNumber_log_eventually_bounds : ∀ᶠ (k : ℕ) in Filter.atTop, 1 / 6 * ↑k * Real.log ↑k ≤ Real.log ↑(triangleRamseyNumber k) ∧ Real.log ↑(triangleRamseyNumber k) ≤ 2 * ↑k * Real.log ↑k

theorem ErdosProblems.MulticolourTriangleRamsey.triangleRamseyNumber_log_isTheta : (fun (k : ℕ) => Real.log ↑(triangleRamseyNumber k)) =Θ[Filter.atTop] fun (k : ℕ) => ↑k * Real.log ↑k

theorem ErdosProblems.MulticolourTriangleRamsey.divergentRamseyRoot : Filter.Tendsto (fun (k : ℕ) => ↑(triangleRamseyNumber k) ^ (1 / ↑k)) Filter.atTop Filter.atTop

theorem ErdosProblems.MulticolourTriangleRamsey.erdos_183 : Filter.Tendsto (fun (k : ℕ) => ↑(triangleRamseyNumber k) ^ (1 / ↑k)) Filter.atTop Filter.atTop

theorem ErdosProblems.MulticolourTriangleRamsey.erdos_problem_183_explicit : (∀ (k : ℕ), 2 ≤ k → (1 / (6 * Real.exp 38) * ↑k ^ (1 / 3) / Real.log ↑k) ^ k ≤ ↑(triangleRamseyNumber k)) ∧ Filter.Tendsto (fun (k : ℕ) => ↑(triangleRamseyNumber k) ^ (1 / ↑k)) Filter.atTop Filter.atTop