DenseTriangleFreeConfigurations

Abstract

Finite graph structure, degree counting, and perfect matchings.

Definition 1.1 (A3Edges).

$$(A3Edges:\mathrm{Finset}(\mathrm{Fin}8\times \mathrm{Fin}8))=\{(0,3),(0,4),(0,5),(1,4),(1,5),(1,6),(2,5),(2,6),(2,7),(3,0),(3,6),(3,7),(4,0),(4,1),(4,7),(5,0),(5,1),(5,2),(6,1),(6,2),(6,3),(7,2),(7,3),(7,4)\}$$

Formalization. D5/S3/Combinatorics/Graph/Walks/DenseTriangleFreeConfigurations.A3Edges (✓ std3).

Source. Repository-derived.

Acknowledgement. M. Ahanjideh; T. Ekim; M. A. Yıldız (2022). Maximum size of a triangle-free graph with bounded maximum degree and matching number. DOI: 10.1007/s10878-024-01123-z. URL: https://arxiv.org/abs/2207.02271v1.

Commentary.

The listed ordered pairs give both orientations of the edges of the eight-vertex Andrásfai graph.

Definition 1.2 (MycEdges).

$$(\mathrm{MycEdges}:\mathrm{Finset}(\mathrm{Fin}11\times \mathrm{Fin}11))=\{(0,1),(0,4),(0,6),(0,9),(1,0),(1,2),(1,5),(1,7),(2,1),(2,3),(2,6),(2,8),(3,2),(3,4),(3,7),(3,9),(4,0),(4,3),(4,5),(4,8),(5,1),(5,4),(5,10),(6,0),(6,2),(6,10),(7,1),(7,3),(7,10),(8,2),(8,4),(8,10),(9,0),(9,3),(9,10),(10,5),(10,6),(10,7),(10,8),(10,9)\}$$

Formalization. D5/S3/Combinatorics/Graph/Walks/DenseTriangleFreeConfigurations.MycEdges (✓ std3).

Source. Repository-derived.

Acknowledgement. M. Ahanjideh; T. Ekim; M. A. Yıldız (2022). Maximum size of a triangle-free graph with bounded maximum degree and matching number. DOI: 10.1007/s10878-024-01123-z. URL: https://arxiv.org/abs/2207.02271v1.

Commentary.

The edge list specifies the eleven-vertex Mycielski graph built from a five-cycle.

Definition 1.3 (A3).

$$\forall (ij:\mathrm{Fin}8),(A3.\mathrm{Adj}ij)⟺((i,j)\in A3Edges)$$

Formalization. D5/S3/Combinatorics/Graph/Walks/DenseTriangleFreeConfigurations.A3 (✓ std3).

Source. Repository-derived.

Acknowledgement. M. Ahanjideh; T. Ekim; M. A. Yıldız (2022). Maximum size of a triangle-free graph with bounded maximum degree and matching number. DOI: 10.1007/s10878-024-01123-z. URL: https://arxiv.org/abs/2207.02271v1.

Commentary.

Adjacency is membership in the displayed Andrásfai edge list.

Definition 1.4 (Myc).

$$\forall (ij:\mathrm{Fin}11),(\mathrm{Myc}.\mathrm{Adj}ij)⟺((i,j)\in \mathrm{MycEdges})$$

Formalization. D5/S3/Combinatorics/Graph/Walks/DenseTriangleFreeConfigurations.Myc (✓ std3).

Source. Repository-derived.

Acknowledgement. M. Ahanjideh; T. Ekim; M. A. Yıldız (2022). Maximum size of a triangle-free graph with bounded maximum degree and matching number. DOI: 10.1007/s10878-024-01123-z. URL: https://arxiv.org/abs/2207.02271v1.

Commentary.

Adjacency is membership in the displayed Mycielski edge list.

Theorem 1.5 (pentagon edge iff).

$$\forall (ij:\mathrm{Fin}5),((\mathrm{SimpleGraph}.\mathrm{cycleGraph}5).\mathrm{comap}(fun(t:\mathrm{Fin}5)\mapsto 3\cdot t)).\mathrm{Adj}ij⟺((j=i+2)\vee (j=i+3))$$

Proof. Machine-checked in Lean as D5/S3/Combinatorics/Graph/Walks/DenseTriangleFreeConfigurations.pentagon_edge_iff (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. M. Ahanjideh; T. Ekim; M. A. Yıldız (2022). Maximum size of a triangle-free graph with bounded maximum degree and matching number. DOI: 10.1007/s10878-024-01123-z. URL: https://arxiv.org/abs/2207.02271v1.

Commentary.

Multiplication by three identifies the standard five-cycle adjacency with steps two and three.

Definition 1.6 (Pentagon).

$$\forall (V:\mathrm{Type}),\forall (G:\mathrm{SimpleGraph}V),\forall (p:(\mathrm{Fin}5)\to (V)),(\mathrm{Pentagon}Gp)⟺((\forall (ij:\mathrm{Fin}5),((\mathrm{SimpleGraph}.\mathrm{cycleGraph}5).\mathrm{comap}(fun(t:\mathrm{Fin}5)\mapsto 3\cdot t)).\mathrm{Adj}ij\to G.\mathrm{Adj}(pi)(pj)))$$

Formalization. D5/S3/Combinatorics/Graph/Walks/DenseTriangleFreeConfigurations.Pentagon (✓ std3).

Source. Repository-derived.

Acknowledgement. M. Ahanjideh; T. Ekim; M. A. Yıldız (2022). Maximum size of a triangle-free graph with bounded maximum degree and matching number. DOI: 10.1007/s10878-024-01123-z. URL: https://arxiv.org/abs/2207.02271v1.

Commentary.

A map from the five-cycle preserves every adjacency in its step-two cyclic ordering.

Definition 1.7 (Twin).

$$\forall (V:\mathrm{Type}),\forall (G:\mathrm{SimpleGraph}V),\forall (p:(\mathrm{Fin}5)\to (V)),\forall (x:V),\forall (i:\mathrm{Fin}5),(\mathrm{Twin}Gpxi)⟺((\forall (j:\mathrm{Fin}5),(G.\mathrm{Adj}x(pj))⟺(((\mathrm{SimpleGraph}.\mathrm{cycleGraph}5).\mathrm{comap}(fun(t:\mathrm{Fin}5)\mapsto 3\cdot t)).\mathrm{Adj}ij)))$$

Formalization. D5/S3/Combinatorics/Graph/Walks/DenseTriangleFreeConfigurations.Twin (✓ std3).

Source. Repository-derived.

Acknowledgement. M. Ahanjideh; T. Ekim; M. A. Yıldız (2022). Maximum size of a triangle-free graph with bounded maximum degree and matching number. DOI: 10.1007/s10878-024-01123-z. URL: https://arxiv.org/abs/2207.02271v1.

Commentary.

A vertex has precisely the same neighbors on the chosen pentagon as its indexed pentagon vertex.

Definition 1.8 (NoHex).

$$\forall (V:\mathrm{Type}),\forall (G:\mathrm{SimpleGraph}V),(\mathrm{NoHex}G)⟺((\forall (abcdef:V),(G.\mathrm{Adj}ab)\to ((G.\mathrm{Adj}bc)\to ((G.\mathrm{Adj}cd)\to ((G.\mathrm{Adj}de)\to ((G.\mathrm{Adj}ef)\to ((G.\mathrm{Adj}fa)\to (((G.\mathrm{Adj}ad)\vee ((G.\mathrm{Adj}be)\vee (G.\mathrm{Adj}cf)))))))))))$$

Formalization. D5/S3/Combinatorics/Graph/Walks/DenseTriangleFreeConfigurations.NoHex (✓ std3).

Source. Repository-derived.

Acknowledgement. M. Ahanjideh; T. Ekim; M. A. Yıldız (2022). Maximum size of a triangle-free graph with bounded maximum degree and matching number. DOI: 10.1007/s10878-024-01123-z. URL: https://arxiv.org/abs/2207.02271v1.

Commentary.

Every closed six-edge walk has at least one of the three opposite diagonals.

Theorem 1.9 (twin of two).

$$\forall (V:\mathrm{Type}),\forall (G:\mathrm{SimpleGraph}V),(\forall (abc:V),(G.\mathrm{Adj}ab)\to ((G.\mathrm{Adj}bc)\to (\neg G.\mathrm{Adj}ac)))\to (\forall (p:(\mathrm{Fin}5)\to (V)),((\mathrm{Pentagon}Gp))\to ((\forall (x:V),\forall (i:\mathrm{Fin}5),((G.\mathrm{Adj}x(p(i+2))))\to ((((G.\mathrm{Adj}x(p(i+3))))\to ((\mathrm{Twin}Gpxi)))))))$$

Proof. Machine-checked in Lean as D5/S3/Combinatorics/Graph/Walks/DenseTriangleFreeConfigurations.twin_of_two (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. M. Ahanjideh; T. Ekim; M. A. Yıldız (2022). Maximum size of a triangle-free graph with bounded maximum degree and matching number. DOI: 10.1007/s10878-024-01123-z. URL: https://arxiv.org/abs/2207.02271v1.

Commentary.

Triangle-freeness determines the entire pentagon neighborhood from the two required adjacent positions.

Theorem 1.10 (twin edge zero two).

$$\forall (V:\mathrm{Type}),\forall (G:\mathrm{SimpleGraph}V),(\forall (abc:V),(G.\mathrm{Adj}ab)\to ((G.\mathrm{Adj}bc)\to (\neg G.\mathrm{Adj}ac)))\to (((\mathrm{NoHex}G))\to (((\forall (ab:V),(\neg G.\mathrm{Adj}ab)\to (\exists (r:V),(G.\mathrm{Adj}ar)\wedge (G.\mathrm{Adj}br)))\to (((\neg \mathrm{Nonempty}(SimpleGraph.Hom\left(A3,G\right))))\to ((\forall (p:(\mathrm{Fin}5)\to (V)),((\mathrm{Pentagon}Gp))\to ((\forall (x:V),\forall (y:V),((\mathrm{Twin}Gpx0))\to ((((\mathrm{Twin}Gpy2))\to ((G.\mathrm{Adj}xy))))))))))))$$

Proof. Machine-checked in Lean as D5/S3/Combinatorics/Graph/Walks/DenseTriangleFreeConfigurations.twin_edge_zero_two (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. M. Ahanjideh; T. Ekim; M. A. Yıldız (2022). Maximum size of a triangle-free graph with bounded maximum degree and matching number. DOI: 10.1007/s10878-024-01123-z. URL: https://arxiv.org/abs/2207.02271v1.

Commentary.

In a triangle-free graph with no induced hexagon, a common neighbor for every nonedge, and no homomorphism from A3, twins at pentagon positions zero and two are adjacent.

Theorem 1.11 (triangle free of clique free).

$$\forall (V:\mathrm{Type}),\forall [\mathrm{Fintype}V],\forall [\mathrm{DecidableEq}V],\forall (G:\mathrm{SimpleGraph}V),\forall [\mathrm{DecidableRel}G.\mathrm{Adj}],((G.\mathrm{CliqueFree}3))\to ((\forall (a:V),\forall (b:V),\forall (c:V),((G.\mathrm{Adj}ab))\to ((((G.\mathrm{Adj}bc))\to ((\neg G.\mathrm{Adj}ac))))))$$

Proof. Machine-checked in Lean as D5/S3/Combinatorics/Graph/Walks/DenseTriangleFreeConfigurations.triangle_free_of_clique_free (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. M. Ahanjideh; T. Ekim; M. A. Yıldız (2022). Maximum size of a triangle-free graph with bounded maximum degree and matching number. DOI: 10.1007/s10878-024-01123-z. URL: https://arxiv.org/abs/2207.02271v1.

Commentary.

A graph with no three-vertex clique has no triangle: two consecutive edges rule out the edge joining their other endpoints.

Theorem 1.12 (no a3).

$$\forall (V:\mathrm{Type}),\forall [\mathrm{Fintype}V],\forall [\mathrm{DecidableEq}V],\forall (G:\mathrm{SimpleGraph}V),\forall [\mathrm{DecidableRel}G.\mathrm{Adj}],(\forall (abc:V),(G.\mathrm{Adj}ab)\to ((G.\mathrm{Adj}bc)\to (\neg G.\mathrm{Adj}ac)))\to (((3\cdot \mathrm{Fintype}.\mathrm{card}V<8\cdot G.\mathrm{minDegree}))\to ((\neg \mathrm{Nonempty}(SimpleGraph.Hom\left(A3,G\right)))))$$

Proof. Machine-checked in Lean as D5/S3/Combinatorics/Graph/Walks/DenseTriangleFreeConfigurations.no_a3 (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. M. Ahanjideh; T. Ekim; M. A. Yıldız (2022). Maximum size of a triangle-free graph with bounded maximum degree and matching number. DOI: 10.1007/s10878-024-01123-z. URL: https://arxiv.org/abs/2207.02271v1.

Commentary.

The strict three-eighths degree bound excludes a homomorphism from the eight-vertex Andrásfai graph.

Theorem 1.13 (no myc).

$$\forall (V:\mathrm{Type}),\forall [\mathrm{Fintype}V],\forall [\mathrm{DecidableEq}V],\forall (G:\mathrm{SimpleGraph}V),\forall [\mathrm{DecidableRel}G.\mathrm{Adj}],(\forall (abc:V),(G.\mathrm{Adj}ab)\to ((G.\mathrm{Adj}bc)\to (\neg G.\mathrm{Adj}ac)))\to (((3\cdot \mathrm{Fintype}.\mathrm{card}V<8\cdot G.\mathrm{minDegree}))\to ((\neg \mathrm{Nonempty}(SimpleGraph.Hom\left(\mathrm{Myc},G\right)))))$$

Proof. Machine-checked in Lean as D5/S3/Combinatorics/Graph/Walks/DenseTriangleFreeConfigurations.no_myc (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. M. Ahanjideh; T. Ekim; M. A. Yıldız (2022). Maximum size of a triangle-free graph with bounded maximum degree and matching number. DOI: 10.1007/s10878-024-01123-z. URL: https://arxiv.org/abs/2207.02271v1.

Commentary.

The Mycielski weighted independent-set bound excludes a homomorphism into a graph above the strict three-eighths density threshold.

Theorem 1.14 (d2).

$$\forall (V:\mathrm{Type}),\forall [\mathrm{Fintype}V],\forall [\mathrm{DecidableEq}V],\forall (G:\mathrm{SimpleGraph}V),\forall [\mathrm{DecidableRel}G.\mathrm{Adj}],((3\cdot \mathrm{Fintype}.\mathrm{card}V<8\cdot G.\mathrm{minDegree}))\to ((\forall (f:(\mathrm{Fin}6)\to (V)),\exists (v:V),3\le (\mathrm{Finset}.\mathrm{univ}.\mathrm{filter}(fun(i:\mathrm{Fin}6)\mapsto G.\mathrm{Adj}v(fi))).\mathrm{card}))$$

Proof. Machine-checked in Lean as D5/S3/Combinatorics/Graph/Walks/DenseTriangleFreeConfigurations.d2 (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. M. Ahanjideh; T. Ekim; M. A. Yıldız (2022). Maximum size of a triangle-free graph with bounded maximum degree and matching number. DOI: 10.1007/s10878-024-01123-z. URL: https://arxiv.org/abs/2207.02271v1.

Commentary.

Double counting the adjacencies to six indexed positions supplies a common neighbor of at least three positions.

Theorem 1.15 (d3).

$$\forall (V:\mathrm{Type}),\forall [\mathrm{Fintype}V],\forall [\mathrm{DecidableEq}V],\forall (G:\mathrm{SimpleGraph}V),\forall [\mathrm{DecidableRel}G.\mathrm{Adj}],((3\cdot \mathrm{Fintype}.\mathrm{card}V<8\cdot G.\mathrm{minDegree}))\to ((\forall (f:(\mathrm{Fin}9)\to (V)),\exists (v:V),4\le (\mathrm{Finset}.\mathrm{univ}.\mathrm{filter}(fun(i:\mathrm{Fin}9)\mapsto G.\mathrm{Adj}v(fi))).\mathrm{card}))$$

Proof. Machine-checked in Lean as D5/S3/Combinatorics/Graph/Walks/DenseTriangleFreeConfigurations.d3 (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. M. Ahanjideh; T. Ekim; M. A. Yıldız (2022). Maximum size of a triangle-free graph with bounded maximum degree and matching number. DOI: 10.1007/s10878-024-01123-z. URL: https://arxiv.org/abs/2207.02271v1.

Commentary.

Double counting the adjacencies to nine indexed positions supplies a common neighbor of at least four positions.

Definition 1.16 (D2).

$$\forall (V:\mathrm{Type}),\forall (G:\mathrm{SimpleGraph}V),\forall [\mathrm{DecidableRel}G.\mathrm{Adj}],(D2G)⟺((\forall (f:(\mathrm{Fin}6)\to (V)),\exists (x:V),3\le (\mathrm{Finset}.\mathrm{univ}.\mathrm{filter}(fun(i:\mathrm{Fin}6)\mapsto G.\mathrm{Adj}x(fi))).\mathrm{card}))$$

Formalization. D5/S3/Combinatorics/Graph/Walks/DenseTriangleFreeConfigurations.D2 (✓ std3).

Source. Repository-derived.

Acknowledgement. M. Ahanjideh; T. Ekim; M. A. Yıldız (2022). Maximum size of a triangle-free graph with bounded maximum degree and matching number. DOI: 10.1007/s10878-024-01123-z. URL: https://arxiv.org/abs/2207.02271v1.

Commentary.

Among any six indexed positions, one vertex is adjacent to at least three positions.

Definition 1.17 (D3).

$$\forall (V:\mathrm{Type}),\forall (G:\mathrm{SimpleGraph}V),\forall [\mathrm{DecidableRel}G.\mathrm{Adj}],(D3G)⟺((\forall (f:(\mathrm{Fin}9)\to (V)),\exists (x:V),4\le (\mathrm{Finset}.\mathrm{univ}.\mathrm{filter}(fun(i:\mathrm{Fin}9)\mapsto G.\mathrm{Adj}x(fi))).\mathrm{card}))$$

Formalization. D5/S3/Combinatorics/Graph/Walks/DenseTriangleFreeConfigurations.D3 (✓ std3).

Source. Repository-derived.

Acknowledgement. M. Ahanjideh; T. Ekim; M. A. Yıldız (2022). Maximum size of a triangle-free graph with bounded maximum degree and matching number. DOI: 10.1007/s10878-024-01123-z. URL: https://arxiv.org/abs/2207.02271v1.

Commentary.

Among any nine indexed positions, one vertex is adjacent to at least four positions.

Theorem 1.18 (no hexagon).

$$\forall (V:\mathrm{Type}),\forall (G:\mathrm{SimpleGraph}V),\forall [\mathrm{DecidableRel}G.\mathrm{Adj}],(\forall (abc:V),(G.\mathrm{Adj}ab)\to ((G.\mathrm{Adj}bc)\to (\neg G.\mathrm{Adj}ac)))\to (((D2G))\to ((((D3G))\to (((\forall (ab:V),(\neg G.\mathrm{Adj}ab)\to (\exists (r:V),(G.\mathrm{Adj}ar)\wedge (G.\mathrm{Adj}br)))\to (((\neg \mathrm{Nonempty}(SimpleGraph.Hom\left(\mathrm{Myc},G\right))))\to ((\mathrm{NoHex}G))))))))$$

Proof. Machine-checked in Lean as D5/S3/Combinatorics/Graph/Walks/DenseTriangleFreeConfigurations.no_hexagon (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. M. Ahanjideh; T. Ekim; M. A. Yıldız (2022). Maximum size of a triangle-free graph with bounded maximum degree and matching number. DOI: 10.1007/s10878-024-01123-z. URL: https://arxiv.org/abs/2207.02271v1.

Commentary.

The six- and nine-position common-neighbor properties, together with a common neighbor for each nonadjacent pair and the excluded Mycielski homomorphism, force a diagonal in every closed hexagon.

References

• Truth anchor: D5/S3/Combinatorics/Graph/Walks/DenseTriangleFreeConfigurations.A3
• Truth anchor: D5/S3/Combinatorics/Graph/Walks/DenseTriangleFreeConfigurations.A3Edges
• Truth anchor: D5/S3/Combinatorics/Graph/Walks/DenseTriangleFreeConfigurations.D2
• Truth anchor: D5/S3/Combinatorics/Graph/Walks/DenseTriangleFreeConfigurations.D3
• Truth anchor: D5/S3/Combinatorics/Graph/Walks/DenseTriangleFreeConfigurations.Myc
• Truth anchor: D5/S3/Combinatorics/Graph/Walks/DenseTriangleFreeConfigurations.MycEdges
• Truth anchor: D5/S3/Combinatorics/Graph/Walks/DenseTriangleFreeConfigurations.NoHex
• Truth anchor: D5/S3/Combinatorics/Graph/Walks/DenseTriangleFreeConfigurations.Pentagon
• Truth anchor: D5/S3/Combinatorics/Graph/Walks/DenseTriangleFreeConfigurations.Twin
• Truth anchor: D5/S3/Combinatorics/Graph/Walks/DenseTriangleFreeConfigurations.d2
• Truth anchor: D5/S3/Combinatorics/Graph/Walks/DenseTriangleFreeConfigurations.d3
• Truth anchor: D5/S3/Combinatorics/Graph/Walks/DenseTriangleFreeConfigurations.no_a3
• Truth anchor: D5/S3/Combinatorics/Graph/Walks/DenseTriangleFreeConfigurations.no_hexagon
• Truth anchor: D5/S3/Combinatorics/Graph/Walks/DenseTriangleFreeConfigurations.no_myc
• Truth anchor: D5/S3/Combinatorics/Graph/Walks/DenseTriangleFreeConfigurations.pentagon_edge_iff
• Truth anchor: D5/S3/Combinatorics/Graph/Walks/DenseTriangleFreeConfigurations.triangle_free_of_clique_free
• Truth anchor: D5/S3/Combinatorics/Graph/Walks/DenseTriangleFreeConfigurations.twin_edge_zero_two
• Truth anchor: D5/S3/Combinatorics/Graph/Walks/DenseTriangleFreeConfigurations.twin_of_two