In previous threads, we discussed the Hat tiling and an algorithm for Polygon fragmentation. Michael Trott also gave an alternative Polygon fragmentation algorithm, which can potentially provide an alternative approach to the following proof. Observing vertex classes of just one Hat tile, we notice five 1/3 vertices and ask about their combinatorics: how many ways can three hat tiles be arranged legally around three 1/3 vertices? The answer is only 10 different ways, and moreover, none of these configurations involves a reflected Hat tile! The purpose of this memo is to prove the ten vertex theorem as a means to start understanding structure of the triality trees and the new Hat tiling from David Smith et al.

previous code (David Smith’s Hat tile)


previous code (region solver)


Annotating the Hat tile

Here it is again, another depiction of David Smith’s wonderful hat tile:
In[]:=
Graphics[{LightGray,EdgeForm[Black],​​TilePolygon[Tile[1][{0,0},0,#,0]],​​Red,PointSize[Large],Point[{0,0}]}]&/@{False}
Out[]=


It has thirteen vertices, which we’ve numbered from 0 to 12, counter-clockwise, starting from the concave vertex on the brim. Each vertex gets a rational number describing how much of the surrounding figure is completed by the one tile taken alone:
In[]:=
vertexAngles=Association[​​{​​0->3/4,​​1->1/3,​​2->1/4,​​3->1/3,​​4->3/4,​​5->1/3,​​6->1/4,​​7->2/3,​​8->1/4,​​9->2/3,​​10->1/4,​​11->1/3,​​12->1/3​​}];
Classified separately, they are:
In[]:=
oneThirdVertices=Select[vertexAngles,And[Denominator[#]==3,Numerator[#]==1]&]
Out[]=
1
1
3
,3
1
3
,5
1
3
,11
1
3
,12
1
3

In[]:=
twoThirdVertices=Select[vertexAngles,And[Denominator[#]==3,Numerator[#]==2]&]
Out[]=
7
2
3
,9
2
3

In[]:=
oneFourthVertices=Select[vertexAngles,And[Denominator[#]==4,Numerator[#]==1]&]
Out[]=
2
1
4
,6
1
4
,8
1
4
,10
1
4

In[]:=
threeFourthVertices=Select[vertexAngles,And[Denominator[#]==4,Numerator[#]==3]&]
Out[]=
0
3
4
,4
3
4

From one particular orientation of the hat tile, we can also assume a local 1/12 angular grid, and write down exactly which parts of the vertex figure are covered by the one tile taken alone:
In[]:=
pointToAngle=Association[{​​0->{12,1,2,3,4,5,6,7,8},​​1->{2,3,4,5},​​2->{5,6,7},​​3->{7,8,9,10},​​4->{4,5,6,7,8,9,10,11,12},​​5->{6,7,8,9},​​6->{9,10,11},​​7->{7,8,9,10,11,12,1,2},​​8->{10,11,12},​​9->{8,9,10,11,12,1,2,3},​​10->{11,12,1},​​11->{1,2,3,4},​​12->{3,4,5,6}​​}];
Of course, the Hat tile will need to be rotated, and then these numbers also need to be rotated.

Proof of the 10 Vertex Theorem

We start by fixing the orientation of one tile, and listing it in all possible throuples:
In[]:=
cases=Flatten[Outer[{​​{0,False,#1[[1]]},​​{#4,#2,#1[[2]]},​​{#5,#3,#1[[3]]}​​}&,​​Tuples[Keys[oneThirdVertices],3],​​{True,False},​​{True,False},​​Range[0,11],​​Range[0,11],​​1​​],4];
In[]:=
Length@cases
Out[]=
72000
Using angular data, we can immediately reduce the number of cases:
In[]:=
complete=Union[Map[Sort,​​Select[cases,Length[Union@@MapApply[​​Mod[(1-2Boole[#2])(pointToAngle[#3]+#1)+7(Boole[#2]),​​12]&,#]]==12&]]];
Before moving on, let’s briefly check that a random sample of the excise has an incomplete vertex figure, which also implies invalid overlapping:
In[]:=
Table[Graphics[{Opacity[0.25],EdgeForm[Black],TilePolygon[Apply[Tile[1],Prepend[#,{0,0}]]]&/@RandomChoice[Complement[cases,complete]],​​Opacity[1],Red,Point[{0,0}]​​},ImageSize->100],5]
Out[]=

,
,
,
,

Another possibility is that our list of complete figures contains duplicates by permutation of order and / or concurrent rotation of all tiles. This is reduced accordingly:
In[]:=
AllRotations[code_]:=Sort[Map[Sort,​​Transpose[{code[[All,3]],code[[All,2]],#}​​]&/@Outer[Mod[#1+#2,12]&,2#&/@Range[6],​​code[[All,1]],1]]]
In[]:=
Length@complete​​Length[candidates=DeleteDuplicatesBy[complete,AllRotations]]
Out[]=
480
Out[]=
435
We’ve reduced the number of tests to only 435. For each test, we run the throuple of polygons through a fragmentation procedure:
In[]:=
CodeToInputData[code_]:=Module[{segs,vertices,toIndex},​​segs=Union[Sort/@Catenate[Partition[​​TilePolygon[Apply[Tile[1],​​Prepend[#,{0,0}]]][[1]],2,1,1]&/@code]];​​toIndex=Association[MapIndexed[#1->#2[[1]]&,Catenate[segs]]];​​vertices=Association[MapIndexed[#2[[1]]->#1&,Catenate[segs]]];​​{Lookup[toIndex,#]&/@segs,vertices}​​]
In[]:=
FragmentationDiagram[code_]:=Module[{res,polys},​​res=Apply[SolvePlanarIntersections,​​CodeToInputData[code]];​​polys=ExtractPolygons[res["Edges"]];​​polys=Polygon[Lookup[res["Vertices"],#]]&/@polys;​​polys=Most[SortBy[polys,Length]];​​{Graphics[MapIndexed[{​​Hue[(#2[[1]]-1)/Length[polys]],​​EdgeForm[Black],#1​​}&,polys]],Length@*First/@polys}​​]
This is the only significant time cost in the computer proof, which is much less than the amount of time it took to write all the code. Filtering these results is trivial, we just throw out cases where some of the result polygons have fewer than 13 vertices:
This step is subject to doubt and failure analysis, but I’ve looked at it quite closely and have convinced myself that it’s fine. There are only 33 results in two different reflection classes:
Mixing reflected and unreflected tiles, we get only configurations with a rectangular cap gap that obviously can not be filled by adding another hat tile:
For throuples of just one parity, we get 10 valid results, only eight of which actually appear in a valid hat tiling:
The coloring conventions are about the same as used in the documentation for WFR`HatTrialityTree. Thus the theorem is proven, but *a lot* more work remains to be done. For a next step, can anyone prove that the last two figures don’t appear in a valid hat tiling?

CITE THIS NOTEBOOK

Hat combinatorics: the ten vertex theorem​
by Brad Klee​
Wolfram Community, STAFF PICKS, June 12 2023
​https://community.wolfram.com/groups/-/m/t/2935078