The relation algebra 33₆₅: representations as graphs of diameter three, five distance-regular candidates, and group exclusions

The relation algebra 33₆₅ has a flexible atom, and whether it has a finite representation is open. This paper studies the question through distance-regular graphs. It starts from the axioms of the algebra and proves that a finite representation is the same thing as a triangle-free graph of diameter 3 in which no vertex is at distance 3 from both ends of an edge. A distance-regular graph of diameter 3 with a₁ = a₃ = 0 gives such a representation. For valency k ≤ 3000, exactly five intersection arrays pass the standard feasibility conditions: integral multiplicities, the Krein conditions, the absolute bound, Godsil’s bound, Terwilliger’s inequality and triple intersection numbers. The smallest is {126,125,9;1,9,126} on 2002 vertices. The others are {105,104,12;1,1,105}, {325,324,17;1,4,325}, {1540,1539,49;1,21,1540} and {1540,1539,25;1,15,1540}. A graph with any of these arrays would be the first finite representation of 33₆₅. For the 2002-vertex array, the paper proves the following. A graph with this array is not vertex-transitive, and every automorphism of prime order at least 11 fixes no vertex. Its automorphism group has no element of order 143 or 26, and its semiregular cyclic subgroups have order at most 22. For an element of order 22, the involution it contains has one of exactly two displacement patterns. The fixed-point-free pattern comes with a structural description of the quotient graph on 1001 vertices. On Cayley graphs, a class-size form of Higman’s character method shows the following. No Cayley graph has the array {126,125,9;1,9,126}, {105,104,12;1,1,105}, {325,324,17;1,4,325} or {1540,1539,25;1,15,1540}. On a group of order 117,992, a Cayley graph with the array {1540,1539,49;1,21,1540} would need trivial centre and no conjugacy class of size 2. A SAT search shows that 33₆₅ has no group representation over any group of order at most 71, nor over any group of odd order at most 97. This covers 574 groups, and every unsatisfiability claim carries an LRAT proof accepted by the formally verified checker cake_lpr. The graph form, the reduction to distance-regular graphs, the feasibility arithmetic of the five arrays and the numerical steps of the symmetry results are verified in Lean 4: 985 theorems in 133 files, with no sorry. Where an argument relies on textbook results (Higman’s method, equitable partitions, Delsarte’s clique bound, rational representations of cyclic groups) or on the GAP group libraries, these are cited. The ancillary archive contains the Lean sources, the SAT encodings, the certificates and logs, and the scripts.