PASS A_E = I_4 + B (B = 4-cycle)

== G: graph facts (primitivity, L_A, out-degrees, |Aut(A)|)
PASS J_4: primitive (A^1 > 0), L_A = 2 (expected 2), |Aut| = 24 (expected 24), out-degrees [4, 4, 4, 4]
PASS J_5: primitive (A^1 > 0), L_A = 2 (expected 2), |Aut| = 120 (expected 120), out-degrees [5, 5, 5, 5, 5]
PASS J_4-I_4: primitive (A^2 > 0), L_A = 2 (expected 2), |Aut| = 24 (expected 24), out-degrees [3, 3, 3, 3]
PASS J_5-I_5: primitive (A^2 > 0), L_A = 2 (expected 2), |Aut| = 120 (expected 120), out-degrees [4, 4, 4, 4, 4]
PASS A_D: primitive (A^2 > 0), L_A = 3 (expected 3), |Aut| = 4 (expected 4), out-degrees [3, 3, 2, 2]
PASS A_E: primitive (A^2 > 0), L_A = 3 (expected 3), |Aut| = 8 (expected 8), out-degrees [3, 3, 3, 3]
PASS A_hub: primitive (A^2 > 0), L_A = 3 (expected 3), |Aut| = 24 (expected 24), out-degrees [2, 2, 2, 2, 5]
PASS A_7: primitive (A^6 > 0), L_A = 5 (expected 5), |Aut| = 24 (expected 24), out-degrees [1, 1, 1, 1, 2, 1, 4]
PASS A_D: out-degrees (3,3,2,2); A_D^2 > 0
PASS A_E: 3-regular, A_E^2 > 0
PASS A_hub: out-degrees (2,2,2,2,5), hub is the only vertex of out-degree 5
PASS Aut(A_E) = Aut(B) has order 8, contains (1 3), and is non-abelian (dihedral)
PASS Aut(A_D) = {id, (1 2), (3 4), (1 2)(3 4)} = Z2 x Z2
PASS A_D = [[I_2, J_2],[J_2, 0]]
PASS A_hub: (1,1,1,1,2)/6 is a positive eigenvector (eigenvalue 3), hence the right PF vector
PASS A_hub: admissible words of length 2 are exactly tt, t5, 5t, 55
PASS A_hub: (a,5,c) admissible for all a,c <= 4
PASS A_7: letters from T in an admissible word (length <= 9) are at least 4 positions apart
PASS A_7: d(t,t') = 4 for t != t' in T, all other distances <= 3

== M: exact models
PASS q (4x4, entries in M_4(Q)) is a magic unitary
PASS q has non-commuting entries: q_11 q_33 != q_33 q_11  [first non-commuting pair (0-indexed) (0, 0, 2, 2)]
PASS q commutes with J_4 and with J_4 - I_4 (so gives a model of QAut = S_4^+)
PASS q (+) 1 is magic and commutes with A_hub
PASS q (+) I_3 is magic and commutes with A_7
PASS A_D model: e, f projections with ef != fe; p = [[e,1-e],[1-e,e]] (+) [[f,1-f],[1-f,f]] magic, commutes with A_D

== E: Lemma 5.2 and Proposition 5.3 (A_E = C_4 + I) in two exact models
PASS [paper model C^2+C^2] p is a magic unitary commuting with B and with A_E
PASS [paper model C^2+C^2] (a) p_(i+2,j+2) = p_ij and p_(i+2,j) = p_(i,j+2)
PASS [paper model C^2+C^2] p commutes with R (antipodal permutation) and B^2 = 2I + 2R
PASS [paper model C^2+C^2] a = p11-p13, b = p12-p14, c = p21-p23, d = p22-p24
PASS [paper model C^2+C^2] (b) self-adjoint, ab=cd=ac=bd=0, a^2=d^2=e, b^2=c^2=1-e, x^3=x
PASS [paper model C^2+C^2] (b) the vanishing terms p11p23 = p13p21 = p12p24 = p14p22 = 0 (Lemma 2.3(c) for B)
PASS [paper model C^2+C^2] (c) e is a projection commuting with every p_ij
PASS [paper model C^2+C^2] C(QAut(A_E)) model non-commutative  [non-commuting pair (0, 0, 1, 1)]
PASS [paper model C^2+C^2] (d) Delta(a)=a(x)a+b(x)c, Delta(b)=a(x)b+b(x)d, Delta(c)=c(x)a+d(x)c, Delta(d)=c(x)b+d(x)d
PASS [paper model C^2+C^2] (e) Delta(e) = Delta(a)^2 = e(x)e+(1-e)(x)(1-e), Delta(g) = g(x)g, g unitary, g != 1
PASS [paper model C^2+C^2] Prop 5.3: entries of w are self-adjoint partial isometries; P' = Q' = eI + (1-e)Sigma
PASS [paper model C^2+C^2] Prop 5.3: (I) P', Q' magic, fix the constant PF vector; (II) A_E P' = Q' A_E
PASS [paper model C^2+C^2] Prop 5.3: (III) all products over admissible word pairs of length <= 7 are partial isometries  [non-zero products per level [6, 22, 70, 214, 646, 1942, 5830]]
PASS [paper model C^2+C^2] Prop 5.3: all products over arbitrary word pairs of length <= 5 are partial isometries  [non-zero products per level [6, 28, 120, 496, 2016]]
PASS [paper model C^2+C^2] Prop 5.3: sum_k w_ik (x) w_kj = Delta(w_ij) for all i, j (the map intertwines coproducts)
PASS [paper model C^2+C^2] canonical relations for A_E first fail at level 2 <= L_A = 3
PASS [paper model C^2+C^2] Theorem 3.1 for A_E, a=1, c=3, alpha=(1, 2, 3): identity (1) for all b,d; telescoping sums = 1; T=0 for non-admissible beta
PASS [paper model] e = 1 (+) 0; p_11 = (1+s_1)/2 (+) 0 and p_22 = (1+s_2)/2 (+) 0 do not commute
PASS [new model Q^3+Q^2] p is a magic unitary commuting with B and with A_E
PASS [new model Q^3+Q^2] (a) p_(i+2,j+2) = p_ij and p_(i+2,j) = p_(i,j+2)
PASS [new model Q^3+Q^2] p commutes with R (antipodal permutation) and B^2 = 2I + 2R
PASS [new model Q^3+Q^2] a = p11-p13, b = p12-p14, c = p21-p23, d = p22-p24
PASS [new model Q^3+Q^2] (b) self-adjoint, ab=cd=ac=bd=0, a^2=d^2=e, b^2=c^2=1-e, x^3=x
PASS [new model Q^3+Q^2] (b) the vanishing terms p11p23 = p13p21 = p12p24 = p14p22 = 0 (Lemma 2.3(c) for B)
PASS [new model Q^3+Q^2] (c) e is a projection commuting with every p_ij
PASS [new model Q^3+Q^2] C(QAut(A_E)) model non-commutative  [non-commuting pair (0, 0, 1, 1)]
PASS [new model Q^3+Q^2] (d) Delta(a)=a(x)a+b(x)c, Delta(b)=a(x)b+b(x)d, Delta(c)=c(x)a+d(x)c, Delta(d)=c(x)b+d(x)d
PASS [new model Q^3+Q^2] (e) Delta(e) = Delta(a)^2 = e(x)e+(1-e)(x)(1-e), Delta(g) = g(x)g, g unitary, g != 1
PASS [new model Q^3+Q^2] Prop 5.3: entries of w are self-adjoint partial isometries; P' = Q' = eI + (1-e)Sigma
PASS [new model Q^3+Q^2] Prop 5.3: (I) P', Q' magic, fix the constant PF vector; (II) A_E P' = Q' A_E
PASS [new model Q^3+Q^2] Prop 5.3: (III) all products over admissible word pairs of length <= 7 are partial isometries  [non-zero products per level [6, 22, 70, 214, 646, 1942, 5830]]
PASS [new model Q^3+Q^2] Prop 5.3: all products over arbitrary word pairs of length <= 5 are partial isometries  [non-zero products per level [6, 28, 120, 496, 2016]]
PASS [new model Q^3+Q^2] Prop 5.3: sum_k w_ik (x) w_kj = Delta(w_ij) for all i, j (the map intertwines coproducts)
PASS [new model Q^3+Q^2] canonical relations for A_E first fail at level 2 <= L_A = 3
PASS [new model Q^3+Q^2] Theorem 3.1 for A_E, a=1, c=3, alpha=(1, 2, 3): identity (1) for all b,d; telescoping sums = 1; T=0 for non-admissible beta

== D: Proposition 5.1 (A_D)
PASS A_D: s = 2e-1, t = 2f-1 are symmetries with st != ts; P' = Q' = I_4 for w = diag(s,t,1,1)
PASS A_D: (I) P' = Q' = I magic and fix every vector, (II) A_D P' = Q' A_D
PASS A_D: all products over arbitrary word pairs of length <= 7 are partial isometries (0 or unitary)  [non-zero products per level [4, 16, 64, 256, 1024, 4096, 16384]]
PASS A_D: Delta(e) = e(x)e + (1-e)(x)(1-e), Delta(s) = s(x)s, Delta(t) = t(x)t
PASS A_D: sum_k w_ik (x) w_kj = Delta(w_ij) for all i, j
PASS A_D: canonical relations first fail at level 2 <= L_A = 3

== C: levels of the canonical relations (Theorem 3.1, Remark 3.2, Example 4.2)
PASS J_4: canonical relations hold at levels < 2 and first fail at level 2 = L_A = 2  [non-zero products per level [16, 96]]
PASS J_4-I_4: canonical relations hold at levels < 2 and first fail at level 2 = L_A = 2  [non-zero products per level [16, 80]]
PASS A_hub: canonical relations hold at levels < 3 and first fail at level 3 = L_A = 3  [non-zero products per level [17, 49, 193]]
PASS A_7: canonical relations hold at levels < 5 and first fail at level 5 = L_A = 5  [non-zero products per level [19, 35, 67, 115, 259]]
PASS Remark 3.2: T_{(1,5,6,7,3),(1,5,6,7,3)} = q_11 q_33 is not a partial isometry
PASS Example 4.2(ii): w = q (+) 1 has P' = Q' = w, (I) with the PF vector, (II)
PASS Example 4.2(ii)/(iii): relations of level <= 2 hold for w; level 3 fails
PASS Example 4.2(iii): w_{(1,5,3),(1,5,3)} = q_11 q_33 is not a partial isometry
PASS Theorem 3.1 for A_7, a=1, c=3, alpha=(1, 5, 6, 7, 3): identity (1) for all b,d; telescoping sums = 1; T=0 for non-admissible beta
PASS Theorem 3.1 for A_hub, a=1, c=2, alpha=(1, 5, 2): identity (1) for all b,d; telescoping sums = 1; T=0 for non-admissible beta

== X: Lemma 2.2 on exact instances
PASS Lemma 2.2(b): P = diag(1,0), Q = (1/2)[[1,1],[1,1]]: PQ is not a partial isometry and PQ != QP
PASS Lemma 2.2(a) instance W1: VW partial isometry <=> [V*V, WW*] = 0 (both sides agree)
PASS Lemma 2.2(a) instance W2: VW partial isometry <=> [V*V, WW*] = 0 (both sides agree)
PASS Lemma 2.2(a) instance W3 (range rotated): [V*V, WW*] != 0 and VW is not a partial isometry

81/81 checks pass
ALL PASS
