Help me prove the Four Color Theorem!

Question

This is not just another challenge asking you to color random maps... In this challenge, you are asked to write a program that is actually used in the formal proof of the Four Color Theorem.

First I shall describe the challenge without any background or motivation, for the impatient.

A chromogram is a list made of the symbols - [ ]0 ]1, where the brackets are required to match. A coloring is just a list made of 1, 2 and 3's whose bitwise sum (i.e. XOR) is zero. A coloring is said to fit a chromogram if:

• They are of the same length.
• -'s in the chromogram corresponds to 1's in the coloring at the same positions.
• Brackets corresponds to 2's and 3's. For matching brackets, if they are [ ]0 then they correspond to the same color, and different colors if they are [ ]1.

Some examples:

Chromogram      <-> Coloring
[ [ - ]1 - ]0 - <-> 2 3 1 2 1 2 1
[ [ - ]1 - ]0 - <-> 3 3 1 2 1 3 1
[ ]1 -          <-> 2 3 1
[ ]1 -          <-> 3 2 1

Given colorings \$C\$, a compatible coloring is one such that each of its chromograms fits with some \$c\in C\$ (different chromograms can fit different colorings). More formally, we define "\$c'\$ is compatible with \$C\$" as the logical proposition "for each chromogram \$\gamma\$ that fits \$c'\$, there exists \$c\in C\$ such that \$\gamma\$ fits \$c\$." We define a suitable coloring with the following rules:

• All colors in \$C\$ are suitable.
• For a suitable coloring, switching 1, 2 and 3's consistently produces another suitable coloring. E.g. 12321 -> 21312 or 32123 or 13231, but not 11311 or 12331. Formally, if \$\rho\$ is a permutation of \$\{1,2,3\}\$, then if \$\langle c_1, c_2, \dots, c_n \rangle\$ is a suitable coloring, \$\langle \rho c_1, \rho c_2, \dots, \rho c_n \rangle\$ is also one.
• For a set of suitable coloring \$D\$, all its compatible colorings are suitable. Note that if you put more suitable colorings into the set \$D\$, an originally compatible coloring will never cease to be compatible. So in your code, you can greedily add suitable colorings without worrying that you will "miss the chance" to apply this rule.
• All the suitable colorings are generated by the rules above.

As an example, take \$C\$ to have two colorings 1111, 2323. You can use the second rule to claim that 2222 is suitable. Then 2233 is suitable using the third rule, because it fits two chromograms [ ]0 [ ]0 and [ [ ]1 ]1, the first of which fits 2222, and the second fits 2323.

Now the challenge:

Challenge. Input a set of coloring \$C\$, determine if all the colorings of the same length are suitable. This is code-golf.

A hint: A sequence of 1, 2 and 3's have the bitwise sum (XOR) zero if and only if the parity of each kind of number are the same, i.e. the numbers of occurrences of 1's, 2's and 3's are all odd or all even. But probably XOR'ing all of them is more golfy.

---

Now it's time for stories. The Four Color Theorem states that any planar map can be colored with four colors, so that the regions that meet at boundaries are colored differently. I'll try to briefly describe the proof of the Four Color Theorem, in steps.

1. First, if you create a tiny region at every corner (i.e. where three or more regions meet), you get a map where no more than three regions meet at a point, and if you can color these kind of maps, you can remove the added region and recover a coloring of the original map. These special maps are called cubic.
2. Now we reason by reductio ad absurdum. Consider the smallest cubic counterexample. Any map smaller than that will be 4-colorable.
3. Next, by a method of discharging, we compute a score for each region, ensuring that the average score is less than 6. This means that there must be at least one region with score less than 6. In this way we locate a "weak spot" of the putative counterexample, where we are going to attack.
4. We, by the aid of a program (not related to this challenge), prove that the neighborhood of the weak spots that we may find always falls in one of the 633 possibilities. This allows us to do a case-by-case analysis.
5. In each case, we remove some boundaries in the neighborhood of the weak spot, creating a smaller map. By hypothesis, this map is 4-colorable. We then try to recolor the original map based on the smaller map, only adjusting the colors in the neighborhood. This is not always possible. So we try to adjust the outer regions also. This is difficult because changing one regions's color may affect other regions. We now develop a more convenient tool.
6. Notice that if, instead of coloring the regions by colors \$0,1,2,3\$, we color the boundaries of the map, by computing the bitwise sum of the two regions on either side of the boundaries, we can color the boundaries with \$1,2,3\$. It can be proven that the original coloring can always be recovered from the boundary coloring. Now the situation is clearer. Note that exactly 3 boundaries meet at a corner, and they always have different colors. Suppose we want to change an boundary color from 2 to 3 (the boundary sticks out from the neighborhood we just considered, so it will be consistent with the colors in the neighborhood), the only hinderance is the edge colored 3 connected to it (there is only one such edge extending outwards, can you see why?). If we change that 3 into 2, a further edge colored 2 will protest! In this way, we can go on and on in a chain. And the key insight is that the chain cannot intersect itself, so it will always come back sticking into the neighborhood again.
7. So now, the boundaries colored 2/3 will form arches standing on the edge of the neighborhood we are considering. These arching structures are captured by our chromograms, and the colors of the boundaries sticking out of the neighborhood are represented by the colorings in our challenge. Now if you reread the challenge, you will understand that, given the recoloring that we have for the neighborhood, the challenge is to determine if every possible coloring for the outer map can be adjusted to match.

---

Phew! That was, alas, the briefest that I can manage without losing too much detail! You can see that our challenge is only concerned with the last step, and there are more potential challenges lurking about. But this I leave to those who are interested. You can consult this paper for a more detailed account. I hope this challenge can kindle some interest in the four color theorem and its proof.

---

Routine code-golf test cases:

T 123
T 1111,2323
F 1111,2332
T 11123,12113,12311
F 11123,12113,12131
T 111111,123132,123231,123312,123213,112323,121222,122122,122212
F 123132,123231,123312,123213,112323,121222,122122,122212
F 123231,123312,123213,112323,121222,122122,122212
F 111111,123312,123213,112323,121222,122122,122212
T 111111,123231,123213,112323,121222,122122,122212
F 111111,123231,123312,112323,121222,122122,122212
F 111111,123231,123312,123213,121222,122122,122212
F 111111,123231,123312,123213,112323,122122,122212
T 111111,123231,123312,123213,112323,121222,122212
F 111111,123231,123312,123213,112323,121222,122122
F 111111,123132,123312,123213,112323,121222,122122,122212
T 111111,123132,123231,123213,112323,121222,122122,122212
F 111111,123132,123231,123312,112323,121222,122122,122212
F 111111,123132,123231,123312,123213,121222,122122,122212
F 111111,123132,123231,123312,123213,112323,122122,122212
T 111111,123132,123231,123312,123213,112323,121222,122212
F 111111,123132,123231,123312,123213,112323,121222,122122

I hesitate to include larger test cases, because to do those in reasonable time, some algorithm other than the most naive one is needed. I don't want to complicate things too much, since they are already so complicated. Better algorithms can be found in the linked paper.

Answer 1

Python 3.8 (pre-release), 835 bytes

E=enumerate
G=len
def m(c,o):
 i=o;b=0
 for v in c[o:]:
  b+=(v==1)-(v>1)
  if b==0:break
  i+=1
 return i
f=lambda c,C:G(c)==G(C)and all(C[i]<2if V<1else V!=1or(h:=m(c,i))<G(C)and eval(f'1<C[i]{"  =!"[c[h]]}=C[h]>1')for i,V in E(c))
def N(l,L):
 if L<2:return[[V]for V in l]
 r=[]
 for V in l:
  for g in N(l,L-1):r+=[[V,*g]]
 return r
def A(s,B=[]):
 W=[C for C in N([1,2,3],G(s[0]))if eval('^'.join(str(Q)for Q in C))==0]
 S=s+[C for C in W if all(any(f(c,T)for T in s)for c in N([0,1,2,3],G(C))if all(V!=1or m(c,i)<G(c)for i,V in E(c))and c.count(1)==c.count(2)+c.count(3)and f(c,C))]
 for C in[*S]:
  for p in[[1,2,3],[1,3,2],[2,1,3],[2,3,1],[3,1,2],[3,2,1]]:S+=[[p[o-1]for o in C]]
 S=[''.join(str(o)for o in C)for C in S];S=[*{*S}];S=[[int(Y)for Y in C] for C in S];D=[G(B),G(W)]
 if G(S)in D:return D.index(G(S))
 return A(S,s)

Try it online!

Thanks @Steffan for -11 bytes.

Not exactly the golfiest version that could be produced. I will continue to golf this code.

Not very efficient. Takes at least 15 3 minutes to complete all 22 testcases. Thus, don't expect the TIO link to work. You can, however, run it locally if Python is on your machine. The TIO link includes a test suite that compares the outputs against the expected outputs.

Explanation

Just implements the question's spec literally. Defines a helper function f that checks if a chromogram fits a coloring. In the main function A, starts off with the inputted set plus set of compatible colorings (implemented based on the question's definition, making sure to check that lists that are purportedly chromograms and colorings are actually chromograms and colorings), then adds the permutations, removes duplicates, then:

• if every coloring of the same length as each coloring of the inputted set is in the set generated according to the above, then return 1.
• if no new colorings were added (i.e. length of generated set is the same as that of the previous set [c.f. below]), return 0. (once we add all the colorings of the same length, the function returns 1 before calling itself, thus avoiding returning 0)
• otherwise, recall the function with the new set and passing the previous set (which starts empty).

Ungolfed version (2778 bytes):

def matching_bracket(c,o):
 index = opening
 bracket_level = 0
 for value in chromogram[opening:]:
  if value == 1:
   bracket_level += 1
  if value > 1:
   bracket_level -= 1
  if bracket_level == 0:
   break
  index += 1
 return index

def valid_brackets(chromogram, coloring, opening):
 index = matching_bracket(chromogram, opening)
 try:
  if chromogram[index] == 2:
   return 1 < coloring[opening] == coloring[index]
  return 1 < coloring[opening] != coloring[index] > 1
 except IndexError:
  return False

def fits(chromogram, coloring):
 return (len(chromogram) == len(coloring)) and \
        (all([coloring[i] == 1 if value == 0 else value != 1 or valid_brackets(chromogram, coloring, i) for i, value in enumerate(chromogram)]))

def generate_nary(l, length):
 if length < 2:
  return [[val] for val in l]
 return_list = []
 for val in l:
  for generated in generate_nary(l, length - 1):
   return_list.append([val, *generated])
 return return_list

def generate_all_chromograms(length):
 return generate_nary([0, 1, 2, 3], length)

def all_fitted_chromograms(coloring):
 return [chromogram for chromogram in generate_all_chromograms(len(coloring)) if [value != 1 or matching_bracket(chromogram, i) < len(chromogram) for i, value in enumerate(chromogram)] and chromogram.count(1) == chromogram.count(2) + chromogram.count(3) and fits(chromogram, coloring)]

def is_compatible(coloring, _set):
 all_chromos = all_fitted_chromograms(coloring)
 return all([
  any([fits(chromo, c) for c in _set])
  for chromo in all_chromos
 ])

def all_colorings(length):
 return [c for c in generate_nary([1, 2, 3], length) if eval('^'.join([str(num) for num in c])) == 0]

def permutations_of_coloring(coloring):
 colorings = []
 for permutation in [[1, 2, 3], [1, 3, 2], [2, 1, 3], [2, 3, 1], [3, 1, 2], [3, 2, 1]]:
  colorings.append([permutation[num - 1] for num in coloring])
 return colorings

def all_suitable_colorings(_set, before = []):
 # 1) all colorings in _set are suitable.
 colorings = all_colorings(len(_set[0]))
 # let us add our compatible colorings.
 initial_set = _set + [coloring for coloring in colorings if is_compatible(coloring, _set)]
 # then, we get all the permutations of each of those colorings.
 for coloring in [*initial_set]:
  for permutated in permutations_of_coloring(coloring):
   initial_set.append(permutated)
 initial_set = [''.join([str(num) for num in coloring]) for coloring in initial_set]
 initial_set = [*{*initial_set}] # remove duplicates
 initial_set = [[int(char) for char in coloring] for coloring in initial_set]
 if len(initial_set) in [len(before), len(colorings)]:
  return initial_set
 return all_suitable_colorings(initial_set, _set)

def main(_set):
 return len(all_suitable_colorings(_set)) == len(all_colorings(len(_set[0])))
```