Triadic complexes

A TriadicComplex3 V is the bounded-complexity object over which an arity-three regular approximation of a coloring of the triples of V is measured. It chooses its own finite palette Fin C.pairColorCount of pair colors, carries a lower skeleton over that palette (vertex cells and a coherent pair coloring), and selects a finite family of polyads over that skeleton.

Its complexity C.complexity is the number of vertex cells plus the number of pair colors plus the number of selected polyads, so it bounds each of these quantities. Since the selected polyads are polyads over the skeleton, the complexity is in turn bounded in terms of the lower data alone.

Forgetting colors and roles, C.toHypergraphComplex is a hypergraph complex of rank three: its levels zero, one and two are complete, since the pair coloring is total, and its level three consists of the underlying unordered triples of the selected polyad supports.

C.IsPolyadDecomposition says that every injective triple lies in the support of a selected polyad. As distinct polyads have disjoint supports, the selected supports then partition the |V| (|V| - 1) (|V| - 2) injective triples. C.VertexCellsControlled t₀ says that the vertex cells form an equipartition with at least t₀ cells; each cell then has at most |V| / t₀ + 1 vertices.

Finally, for a coloring H of the triples, H.exceptionalPolyadMass C η r is the proportion of the selected support carried by polyads over which H is not (η, r)-top-regular, and H.TopRegularOverMostPolyads C η ε r bounds this proportion by ε. Since the selected supports are disjoint sets of injective triples, the irregular polyads then carry at most ε |V| (|V| - 1) (|V| - 2) triples. Consequently, at most k.choose 3 * H.exceptionalPolyadMass C η r * |V| ^ k embeddings Fin k ↪ V send some increasing triple into the support of an irregular selected polyad. This is the part of an induced count of a k-vertex pattern that top regularity does not control, and is charged to the exceptional mass instead.

Main definitions

• TauCeti.TriadicComplex3: a lower skeleton over a chosen pair palette with selected polyads.
• TauCeti.TriadicComplex3.complexity: vertex cells plus pair colors plus polyads.
• TauCeti.TriadicComplex3.toHypergraphComplex: the underlying hypergraph complex of rank three.
• TauCeti.TriadicComplex3.IsPolyadDecomposition: the selected polyads cover all injective triples.
• TauCeti.TriadicComplex3.VertexCellsControlled: equitable vertex cells, at least t₀ of them.
• TauCeti.Colored3Graph.exceptionalPolyadMass: the support proportion of irregular polyads.
• TauCeti.Colored3Graph.TopRegularOverMostPolyads: top regularity off an ε-proportion.

Main results

• TauCeti.TriadicComplex3.complexity_le: the complexity is bounded by the lower data.
• TauCeti.TriadicComplex3.faces_three: the triple faces are the selected support triples.
• TauCeti.TriadicComplex3.isPolyadDecomposition_iff_forall_mem_of_nonempty: a polyad family is a decomposition exactly when it contains every polyad with nonempty support.
• TauCeti.TriadicComplex3.IsPolyadDecomposition.sum_card_support: the selected supports have |V|.descFactorial 3 triples in total.
• TauCeti.TriadicComplex3.sum_card_support_le: in general they have at most that many.
• TauCeti.TriadicComplex3.VertexCellsControlled.card_le: controlled cells are small.
• TauCeti.Colored3Graph.topRegularOverMostPolyads_iff_sum_card_support_le: the support of the irregular polyads is at most an ε-proportion of the selected support.
• TauCeti.Colored3Graph.exceptional_route_mass_le: the embeddings of Fin k meeting an irregular polyad in an increasing triple are at most a k.choose 3 multiple of the exceptional mass, at scale |V| ^ k.

References

• V. Rödl and M. Schacht, Regular partitions of hypergraphs: regularity lemmas, Combin. Probab. Comput. 16 (2007).

structure TauCeti.TriadicComplex3 (V : Type u_2) [Fintype V] [DecidableEq V] : Type u_2

A triadic complex on V: a finite palette of pairColorCount pair colors chosen by the complex, a lower skeleton over that palette, and a finite family of polyads over that skeleton.

• pairColorCount : ℕ

  The number of pair colors in the lower palette.

• skeleton : PairSkeleton3 (Fin self.pairColorCount) V

  The lower skeleton: vertex cells and a coherent coloring of distinct pairs.

• polyads : Finset (Polyad3 self.skeleton)

  The selected polyads over the lower skeleton.

Complexity

def TauCeti.TriadicComplex3.complexity {V : Type u_1} [Fintype V] [DecidableEq V] (C : TriadicComplex3 V) : ℕ

The complexity of a triadic complex: the number of vertex cells, plus the number of pair colors, plus the number of selected polyads.

theorem TauCeti.TriadicComplex3.complexity_def {V : Type u_1} [Fintype V] [DecidableEq V] (C : TriadicComplex3 V) : C.complexity = C.skeleton.vertexPart.parts.card + C.pairColorCount + C.polyads.card

The complexity is vertex cells plus pair colors plus polyads.

theorem TauCeti.TriadicComplex3.card_parts_le_complexity {V : Type u_1} [Fintype V] [DecidableEq V] (C : TriadicComplex3 V) : C.skeleton.vertexPart.parts.card ≤ C.complexity

The complexity bounds the number of vertex cells.

theorem TauCeti.TriadicComplex3.pairColorCount_le_complexity {V : Type u_1} [Fintype V] [DecidableEq V] (C : TriadicComplex3 V) : C.pairColorCount ≤ C.complexity

The complexity bounds the number of pair colors.

theorem TauCeti.TriadicComplex3.card_polyads_le_complexity {V : Type u_1} [Fintype V] [DecidableEq V] (C : TriadicComplex3 V) : C.polyads.card ≤ C.complexity

The complexity bounds the number of selected polyads.

theorem TauCeti.TriadicComplex3.complexity_le {V : Type u_1} [Fintype V] [DecidableEq V] (C : TriadicComplex3 V) : C.complexity ≤ C.skeleton.vertexPart.parts.card + C.pairColorCount + C.skeleton.vertexPart.parts.card ^ 3 * C.pairColorCount ^ 3

The complexity is bounded in terms of the lower data alone: with t vertex cells and q pair colors there are at most t³ q³ polyads.

The underlying hypergraph complex

noncomputable def TauCeti.TriadicComplex3.topFaces {V : Type u_1} [Fintype V] [DecidableEq V] (C : TriadicComplex3 V) : Finset (Finset V)

The unordered triples underlying the supports of the selected polyads.

@[simp]

theorem TauCeti.TriadicComplex3.mem_topFaces {V : Type u_1} [Fintype V] [DecidableEq V] (C : TriadicComplex3 V) {s : Finset V} : s ∈ C.topFaces ↔ ∃ P ∈ C.polyads, ∃ x ∈ P.support, Finset.map { toFun := ↑x, inj' := ⋯ } Finset.univ = s

A top face is the underlying triple of a triple supported by a selected polyad.

theorem TauCeti.TriadicComplex3.card_eq_three_of_mem_topFaces {V : Type u_1} [Fintype V] [DecidableEq V] (C : TriadicComplex3 V) {s : Finset V} (hs : s ∈ C.topFaces) : s.card = 3

Every top face has three elements.

noncomputable def TauCeti.TriadicComplex3.toHypergraphComplex {V : Type u_1} [Fintype V] [DecidableEq V] (C : TriadicComplex3 V) : HypergraphComplex 3 V

The hypergraph complex of rank three underlying a triadic complex. Its levels zero, one and two contain all sets of the corresponding size, since the pair coloring is total; its level three consists of the unordered triples underlying the selected polyad supports. Level zero is {∅}, as in every hypergraph complex (HypergraphComplex.faces_zero).

@[simp]

theorem TauCeti.TriadicComplex3.mem_faces_toHypergraphComplex {V : Type u_1} [Fintype V] [DecidableEq V] (C : TriadicComplex3 V) {k : ℕ} (hk : k ≤ 3) {s : Finset V} : s ∈ C.toHypergraphComplex.faces k hk ↔ s.card = k ∧ (k ≤ 2 ∨ s ∈ C.topFaces)

Membership in a level of the underlying hypergraph complex.

theorem TauCeti.TriadicComplex3.faces_one {V : Type u_1} [Fintype V] [DecidableEq V] (C : TriadicComplex3 V) : C.toHypergraphComplex.faces 1 faces_one._proof_1 = Finset.powersetCard 1 Finset.univ

Every vertex is a face of the underlying hypergraph complex.

theorem TauCeti.TriadicComplex3.faces_two {V : Type u_1} [Fintype V] [DecidableEq V] (C : TriadicComplex3 V) : C.toHypergraphComplex.faces 2 faces_two._proof_1 = Finset.powersetCard 2 Finset.univ

Every unordered pair of distinct vertices is a face of the underlying hypergraph complex.

theorem TauCeti.TriadicComplex3.faces_three {V : Type u_1} [Fintype V] [DecidableEq V] (C : TriadicComplex3 V) : C.toHypergraphComplex.faces 3 faces_three._proof_1 = C.topFaces

The triple faces of the underlying hypergraph complex are exactly the unordered triples underlying the selected polyad supports.

Polyad decompositions

def TauCeti.TriadicComplex3.IsPolyadDecomposition {V : Type u_1} [Fintype V] [DecidableEq V] (C : TriadicComplex3 V) : Prop

The selected polyads decompose the injective triples: every injective triple lies in the support of a selected polyad. Distinct polyads have disjoint supports (Polyad3.pairwise_disjoint_support), so this polyad is unique.

theorem TauCeti.TriadicComplex3.isPolyadDecomposition_iff {V : Type u_1} [Fintype V] [DecidableEq V] (C : TriadicComplex3 V) : C.IsPolyadDecomposition ↔ ∀ (x : { x : Fin 3 → V // Function.Injective x }), ∃ P ∈ C.polyads, x ∈ P.support

Unfolded form of TriadicComplex3.IsPolyadDecomposition.

theorem TauCeti.TriadicComplex3.isPolyadDecomposition_iff_ofTriple_mem {V : Type u_1} [Fintype V] [DecidableEq V] (C : TriadicComplex3 V) : C.IsPolyadDecomposition ↔ ∀ (x : { x : Fin 3 → V // Function.Injective x }), Polyad3.ofTriple C.skeleton x ∈ C.polyads

The selected polyads form a decomposition exactly when they contain the polyad of every injective triple.

theorem TauCeti.TriadicComplex3.isPolyadDecomposition_iff_forall_mem_of_nonempty {V : Type u_1} [Fintype V] [DecidableEq V] (C : TriadicComplex3 V) : C.IsPolyadDecomposition ↔ ∀ (P : Polyad3 C.skeleton), P.support.Nonempty → P ∈ C.polyads

The selected polyads form a decomposition exactly when they contain every polyad over the skeleton with nonempty support.

theorem TauCeti.TriadicComplex3.IsPolyadDecomposition.existsUnique {V : Type u_1} [Fintype V] [DecidableEq V] {C : TriadicComplex3 V} (h : C.IsPolyadDecomposition) (x : { x : Fin 3 → V // Function.Injective x }) : ∃! P : Polyad3 C.skeleton, P ∈ C.polyads ∧ x ∈ P.support

In a polyad decomposition, every injective triple lies in exactly one selected polyad.

theorem TauCeti.TriadicComplex3.IsPolyadDecomposition.sum_card_support {V : Type u_1} [Fintype V] [DecidableEq V] {C : TriadicComplex3 V} (h : C.IsPolyadDecomposition) : ∑ P ∈ C.polyads, P.support.card = (Fintype.card V).descFactorial 3

The supports of the selected polyads of a decomposition contain |V| (|V| - 1) (|V| - 2) triples in total, the number of injective triples.

theorem TauCeti.TriadicComplex3.sum_card_support_le {V : Type u_1} [Fintype V] [DecidableEq V] (C : TriadicComplex3 V) : ∑ P ∈ C.polyads, P.support.card ≤ (Fintype.card V).descFactorial 3

The supports of the selected polyads contain at most |V| (|V| - 1) (|V| - 2) triples in total, with equality for a polyad decomposition (IsPolyadDecomposition.sum_card_support).

Controlled vertex cells

def TauCeti.TriadicComplex3.VertexCellsControlled {V : Type u_1} [Fintype V] [DecidableEq V] (C : TriadicComplex3 V) (t₀ : ℕ) : Prop

The vertex cells are controlled at t₀: they form an equipartition with at least t₀ cells.

theorem TauCeti.TriadicComplex3.vertexCellsControlled_iff {V : Type u_1} [Fintype V] [DecidableEq V] {C : TriadicComplex3 V} {t₀ : ℕ} : C.VertexCellsControlled t₀ ↔ C.skeleton.vertexPart.IsEquipartition ∧ t₀ ≤ C.skeleton.vertexPart.parts.card

Unfolded form of TriadicComplex3.VertexCellsControlled.

theorem TauCeti.TriadicComplex3.VertexCellsControlled.mono {V : Type u_1} [Fintype V] [DecidableEq V] {C : TriadicComplex3 V} {t₀ t : ℕ} (h : C.VertexCellsControlled t₀) (ht : t ≤ t₀) : C.VertexCellsControlled t

Control at t₀ implies control at every smaller floor.

theorem TauCeti.TriadicComplex3.VertexCellsControlled.card_le {V : Type u_1} [Fintype V] [DecidableEq V] {C : TriadicComplex3 V} {t₀ : ℕ} (h : C.VertexCellsControlled t₀) (ht₀ : 0 < t₀) {A : Finset V} (hA : A ∈ C.skeleton.vertexPart.parts) : A.card ≤ Fintype.card V / t₀ + 1

Every vertex cell of a complex controlled at a positive floor t₀ has at most |V| / t₀ + 1 vertices.

Exceptional polyads

noncomputable def TauCeti.Colored3Graph.exceptionalPolyadMass {V : Type u_1} [Fintype V] [DecidableEq V] {κ : Type u_2} [DecidableEq κ] (H : Colored3Graph κ V) (C : TriadicComplex3 V) (η : ℝ) (r : ℕ) : ℝ

The exceptional polyad mass of a coloring H over a triadic complex C: the proportion of the total support of the selected polyads carried by those over which H is not (η, r)-top-regular. It is 0 when the selected polyads have empty supports.

theorem TauCeti.Colored3Graph.exceptionalPolyadMass_def {V : Type u_1} [Fintype V] [DecidableEq V] {κ : Type u_2} [DecidableEq κ] (H : Colored3Graph κ V) (C : TriadicComplex3 V) (η : ℝ) (r : ℕ) : H.exceptionalPolyadMass C η r = (∑ P ∈ C.polyads with ¬IsTopRegularOverPolyad P H η r, ↑P.support.card) / ∑ P ∈ C.polyads, ↑P.support.card

The exceptional polyad mass is the support of the irregular polyads over the total support.

theorem TauCeti.Colored3Graph.exceptionalPolyadMass_eq_sum_div {V : Type u_1} [Fintype V] [DecidableEq V] {κ : Type u_2} [DecidableEq κ] {H : Colored3Graph κ V} {C : TriadicComplex3 V} {η : ℝ} {r : ℕ} (hC : C.IsPolyadDecomposition) : H.exceptionalPolyadMass C η r = (∑ P : Polyad3 C.skeleton with ¬IsTopRegularOverPolyad P H η r, ↑P.support.card) / ↑((Fintype.card V).descFactorial 3)

For a polyad decomposition, exceptional mass can be computed over all polyads of the skeleton, normalized by the number of injective triples. Omitted polyads have empty support.

theorem TauCeti.Colored3Graph.exceptionalPolyadMass_nonneg {V : Type u_1} [Fintype V] [DecidableEq V] {κ : Type u_2} [DecidableEq κ] {H : Colored3Graph κ V} {C : TriadicComplex3 V} {η : ℝ} {r : ℕ} : 0 ≤ H.exceptionalPolyadMass C η r

The exceptional polyad mass is nonnegative.

theorem TauCeti.Colored3Graph.exceptionalPolyadMass_le_one {V : Type u_1} [Fintype V] [DecidableEq V] {κ : Type u_2} [DecidableEq κ] {H : Colored3Graph κ V} {C : TriadicComplex3 V} {η : ℝ} {r : ℕ} : H.exceptionalPolyadMass C η r ≤ 1

The exceptional polyad mass is at most one.

theorem TauCeti.Colored3Graph.exceptionalPolyadMass_eq_zero {V : Type u_1} [Fintype V] [DecidableEq V] {κ : Type u_2} [DecidableEq κ] {H : Colored3Graph κ V} {C : TriadicComplex3 V} {η : ℝ} {r : ℕ} (h : ∀ P ∈ C.polyads, IsTopRegularOverPolyad P H η r) : H.exceptionalPolyadMass C η r = 0

The exceptional polyad mass vanishes when H is top-regular over every selected polyad.

theorem TauCeti.Colored3Graph.exceptionalPolyadMass_le_exceptionalPolyadMass {V : Type u_1} [Fintype V] [DecidableEq V] {κ : Type u_2} [DecidableEq κ] {H : Colored3Graph κ V} {C : TriadicComplex3 V} {η η' : ℝ} {r r' : ℕ} (hη : η ≤ η') (hr : r' ≤ r) : H.exceptionalPolyadMass C η' r' ≤ H.exceptionalPolyadMass C η r

The exceptional polyad mass decreases as the regularity parameter grows and as the rank drops.

def TauCeti.Colored3Graph.TopRegularOverMostPolyads {V : Type u_1} [Fintype V] [DecidableEq V] {κ : Type u_2} [DecidableEq κ] (H : Colored3Graph κ V) (C : TriadicComplex3 V) (η ε : ℝ) (r : ℕ) : Prop

H is (η, r)-top-regular over most polyads of C: the polyads over which H is not (η, r)-top-regular carry at most an ε-proportion of the selected support.

theorem TauCeti.Colored3Graph.topRegularOverMostPolyads_iff {V : Type u_1} [Fintype V] [DecidableEq V] {κ : Type u_2} [DecidableEq κ] {H : Colored3Graph κ V} {C : TriadicComplex3 V} {η ε : ℝ} {r : ℕ} : H.TopRegularOverMostPolyads C η ε r ↔ H.exceptionalPolyadMass C η r ≤ ε

Unfolded form of Colored3Graph.TopRegularOverMostPolyads.

theorem TauCeti.Colored3Graph.topRegularOverMostPolyads_iff_sum_card_support_le {V : Type u_1} [Fintype V] [DecidableEq V] {κ : Type u_2} [DecidableEq κ] {H : Colored3Graph κ V} {C : TriadicComplex3 V} {η ε : ℝ} {r : ℕ} (hε : 0 ≤ ε) : H.TopRegularOverMostPolyads C η ε r ↔ ∑ P ∈ C.polyads with ¬IsTopRegularOverPolyad P H η r, ↑P.support.card ≤ ε * ∑ P ∈ C.polyads, ↑P.support.card

Elimination form. For 0 ≤ ε, top regularity over most polyads says that the support of the irregular selected polyads is at most ε times the total selected support.

theorem TauCeti.Colored3Graph.TopRegularOverMostPolyads.nonneg {V : Type u_1} [Fintype V] [DecidableEq V] {κ : Type u_2} [DecidableEq κ] {H : Colored3Graph κ V} {C : TriadicComplex3 V} {η ε : ℝ} {r : ℕ} (h : H.TopRegularOverMostPolyads C η ε r) : 0 ≤ ε

Top regularity over most polyads forces a nonnegative exceptional proportion.

theorem TauCeti.Colored3Graph.TopRegularOverMostPolyads.sum_card_support_le {V : Type u_1} [Fintype V] [DecidableEq V] {κ : Type u_2} [DecidableEq κ] {H : Colored3Graph κ V} {C : TriadicComplex3 V} {η ε : ℝ} {r : ℕ} (h : H.TopRegularOverMostPolyads C η ε r) : ∑ P ∈ C.polyads with ¬IsTopRegularOverPolyad P H η r, ↑P.support.card ≤ ε * ↑((Fintype.card V).descFactorial 3)

The irregular polyads of a coloring top-regular over most polyads carry at most ε |V| (|V| - 1) (|V| - 2) injective triples.

theorem TauCeti.Colored3Graph.TopRegularOverMostPolyads.mono {V : Type u_1} [Fintype V] [DecidableEq V] {κ : Type u_2} [DecidableEq κ] {H : Colored3Graph κ V} {C : TriadicComplex3 V} {η η' ε ε' : ℝ} {r r' : ℕ} (h : H.TopRegularOverMostPolyads C η ε r) (hη : η ≤ η') (hε : ε ≤ ε') (hr : r' ≤ r) : H.TopRegularOverMostPolyads C η' ε' r'

Top regularity over most polyads weakens as the regularity parameter and the exceptional proportion grow and as the rank drops.

theorem TauCeti.Colored3Graph.topRegularOverMostPolyads_of_forall {V : Type u_1} [Fintype V] [DecidableEq V] {κ : Type u_2} [DecidableEq κ] {H : Colored3Graph κ V} {C : TriadicComplex3 V} {η ε : ℝ} {r : ℕ} (h : ∀ P ∈ C.polyads, IsTopRegularOverPolyad P H η r) (hε : 0 ≤ ε) : H.TopRegularOverMostPolyads C η ε r

A coloring top-regular over every selected polyad is top-regular over most polyads, for every nonnegative exceptional proportion.

theorem TauCeti.Colored3Graph.topRegularOverMostPolyads_const {V : Type u_1} [Fintype V] [DecidableEq V] {κ : Type u_2} [DecidableEq κ] (C : TriadicComplex3 V) {η ε : ℝ} (r : ℕ) (c₀ : κ) (hη : 0 < η) (hε : 0 ≤ ε) : (const c₀).TopRegularOverMostPolyads C η ε r

A constant coloring is top-regular over most polyads of every triadic complex, for every positive regularity parameter and every nonnegative exceptional proportion.

Exceptional routes

theorem TauCeti.Colored3Graph.exceptional_route_mass_le {V : Type u_1} [Fintype V] [DecidableEq V] {κ : Type u_2} [DecidableEq κ] (H : Colored3Graph κ V) (C : TriadicComplex3 V) (k : ℕ) (η : ℝ) (r : ℕ) : ↑{f : Fin k ↪ V | ∃ P ∈ C.polyads, ¬IsTopRegularOverPolyad P H η r ∧ ∃ (i : Fin k) (j : Fin k) (l : Fin k), i < j ∧ j < l ∧ ∃ x ∈ P.support, ↑x = ![f i, f j, f l]}.card ≤ ↑(k.choose 3) * H.exceptionalPolyadMass C η r * ↑(Fintype.card V) ^ k

Exceptional routes. At most k.choose 3 * H.exceptionalPolyadMass C η r * |V| ^ k embeddings f : Fin k ↪ V send some increasing triple i < j < l into the support of a selected polyad over which H is not (η, r)-top-regular. Every labelled copy of a k-vertex pattern routed through an exceptional polyad is such an embedding, so this bounds the part of an induced count that top regularity does not control. Since k.choose 3 ≤ k ^ 3, the bound is at most k ^ 3 * H.exceptionalPolyadMass C η r * |V| ^ k.