One of the central questions in finite model theory is whether there exists a logic that captures polynomial time.

After rank logic and more general linear-algebraic logics have been separated from polynomial time, the most important candidate logics that remain are Choiceless Polynomial Time (CPT) and an extension thereof with a witnessed symmetric choice operator.

In this paper, we make progress towards separating CPT from polynomial time by firstly establishing a connection between the expressive power of CPT and the existence of certain symmetric circuit families, and secondly, proving lower bounds against
these circuits.

We focus on the isomorphism problem of unordered Cai-Fürer-Immerman-graphs (the CFI-query) as a potential candidate for separating CPT from P. Results by Dawar, Richerby and Rossman, and subsequently by Pakusa, Schalthöfer and Selman show that the CFI-query is CPT-definable on linearly ordered and preordered base graphs with small colour classes. We define a class of CPT-algorithms, that we call “CFI-symmetric algorithms”, which generalises all the known ones, and show that such algorithms can only define the CFI-query on a given class of base graphs if there exists a family of symmetric XOR-circuits with certain properties. These properties include that the circuits have the same symmetries as the base graphs, are of polynomial size, and satisfy certain fan-in restrictions.
Then we prove that such circuits with slightly strengthened requirements (i.e. stronger symmetry and fan-in and fan-out restrictions) do not exist for the $n$-dimensional hypercubes as base graphs. This almost separates the CFI-symmetric algorithms from polynomial time – up to the gap that remains between the circuits whose existence we can currently disprove and the circuits whose existence is necessary for the definability of the CFI-query by a CFI-symmetric algorithm.

To an extent, the connection between XOR-circuits and CPT-algorithms for the CFI-query can also be generalised to non-CFI-symmetric algorithms (even though such algorithms are currently not known).

§ INTRODUCTION

Choiceless Polynomial Time (CPT) <cit.> is one of the most prominent candidate logics in finite model theory for capturing polynomial time. It can be seen as an extension of fixed-point logic with counting <cit.> with hereditarily finite sets as data structures. This allows in principle to simulate arbitrary computations in CPT – the only restrictions are that the computed h.f. sets are symmetric under the automorphisms of the input structure and polynomially bounded in size.

Other less studied candidates are logics with with witnessed choice constructs, such as fixed-point logic with witnessed symmetric choice and interpretations <cit.> and CPT extended with witnessed symmetric choice <cit.>. Prior to Lichter's breakthrough <cit.>, which separates rank logic from $\ptime$ using a variation of the famous Cai-Fürer-Immerman (CFI) construction <cit.>, logics with linear-algebraic operators <cit.> were also considered reasonable candidates. However, as outlined in <cit.>, the results from <cit.> and <cit.> together imply that no set of isomorphism-invariant linear algebraic operators can be used to define a logic capturing $\ptime$. Strong lower bounds for Choiceless Polynomial Time, though, have remained elusive. Motivated by Gurevich's conjecture that no logic at all can capture polynomial time, in this article we make progress towards separating CPT from $\ptime$.
For an overview of the unresolved problem "Is there a logic for $\ptime$?" in general, as well as the logic CPT in particular, see for example <cit.>, <cit.>, <cit.>, or <cit.>.

Concerning CPT lower bounds, not very much is known so far: There is a non-definability result for a functional problem in $\ptime$, namely it is impossible to define the dual of a given finite vector space in CPT <cit.>. What we would like to have is, however, the inexpressibility of a polynomial time decision problem. We focus on a standard benchmark from finite model theory, namely the CFI-query. It asks to output, given a CFI-graph, whether it is odd or even. What this means is explained in Section <ref> (it is equivalent to the graph isomorphism problem on these instances). The CFI-query is decidable in polynomial time but not in fixed-point logic with counting nor in rank logic (for generalised CFI-structures). It is open whether it is CPT-definable on unordered instances, and our goal is to eventually answer this question in the negative. Our approach starts off from positive results: There do exist CPT-algorithms for linearly ordered and preordered versions of the CFI-query <cit.> and also CFI-graphs over base graphs of linear degree <cit.>. All these algorithms are based on the construction of hereditarily finite sets which somehow encode the parity of the given CFI-graph in their structure. These sets have been called super-symmetric in <cit.>.

In <cit.> it was shown that there exist unordered CFI-graphs (over $n$-dimensional hypercubes) whose degree is not linear and which cannot be preordered in CPT in such a way that the preorder-based algorithm from <cit.> (or the total-order-based one from <cit.>) could be applied. This shows that these known choiceless algorithms for preordered versions of the CFI-query do not generalise to the unordered case because the necessary combinatorial objects (said preorders) are not symmetric enough: The main limiting factor of CPT is that it cannot define objects which break the symmetry of the input structure “too much” – this is also why unordered (and hence highly symmetric) CFI-instances seem promising for lower bounds.

In the present paper, we take this strategy further: We define a general class of CPT-algorithms for the CFI-query, which encompasses all the known ones mentioned above, and show that their expressiveness depends on the existence of certain symmetric combinatorial objects, namely circuits with Boolean XOR-gates. We show that the CFI-query over a given class $\Kk$ of base graphs is only definable by an algorithm from that class if there exists a family of polynomial-size XOR-circuits with certain properties and, in particular, with the same symmetries as the graphs in $\Kk$ (Theorem <ref>). This means that the non-definability of the CFI-query over $\Kk$ can be shown by proving the non-existence of symmetric circuits with the required properties. Indeed, we almost achieve this goal: Our second main result is a lower bound against such circuits; it shows that if we take as $\Kk$ the family of $n$-dimensional hypercubes and make the circuit properties slightly more restrictive than required by our Theorem <ref>, then no circuit family can satisfy all these properties simultaneously. Thus, we come close to showing that the CFI-query over unordered hypercubes is undefinable by any CPT-algorithm from the general class we are considering.

We define in Section <ref> a class of CPT-algorithms for the CFI-query that contains all the currently known ones and prove that solving the CFI-query on a given class $\Kk$ of unordered base graphs by means of such an algorithm presupposes the existence of certain symmetric XOR-circuits. Following <cit.>, we denote CFI-instances over a base graph $G$ as $\GG^S$, where $S$ is the set of vertices whose CFI-gadget is odd (see Section <ref>). In the following theorem, we consider circuits whose input gates are labelled with the edges of the base graph $G_n$, and all internal gates are XOR gates. The group $\Aut(G_n) \leq \Sym(V(G_n))$ is the automorphism group of the base graph $G_n$. The $\Aut(G_n)$-orbit of the circuit refers to the set of all images of the circuit under relabelings of the input gates with permutations in $\Aut(G_n)$. A circuit is sensitive to an input bit if flipping that bit changes the output of the circuit. The fan-in dimension of a circuit is a parameter that we define in this paper; it is a generalisation of the fan-in degree. All these notions concerning our circuits are presented in detail in Section <ref>.

Let $(G_n = (V_n,E_n))_{n \in \bbN}$ be a sequence of base graphs. Let $\GG^S_n$ be a CFI-graph over $G_n$, and let $\tw_n$ denote the treewidth of $G_n$. If there exists a $\CPT$-program $\Pi$ that is super-symmetric and CFI-symmetric and decides the CFI-query on the instances $\GG_n^S$, for all $n \in \bbN$, then there also exists a family $(C_n)_{n \in \bbN}$ of XOR-circuits such that

* The number of gates in $C_n$ is polynomial in $|\GG^S_n|$.

* The $\Aut(G_n)$-orbit of the circuit has size polynomial in $|\GG^S_n|$.

* $C_n$ is sensitive to $\Omega(\tw_n)$ many input bits.

* The fan-in dimension of $C_n$ is $\Oo(\log |\GG_n^S|)$.

The detailed version of this is Theorem <ref> in Section <ref>.
The terms super-symmetric and CFI-symmetric refer to the properties of a h.f. set that is constructed by the program $\Pi$ in order to decide the CFI-query. Super-symmetry is a property of h.f. sets that goes back to <cit.> and means that a h.f. set is fixed by all edge flips of a CFI-structure $\GG^S$, not only by those which are automorphisms of $\GG^S$ (see Section <ref>). CFI-symmetry is a concept that we define in this paper and which describes the internal structure and “local symmetries” of a h.f. set. The CFI-algorithms from <cit.> and <cit.> are based on h.f. sets which are both super-symmetric and CFI-symmetric. Arguably, both these properties are crucial for the success of all these algorithms: The way they work is that they aggregate all the CFI-gadgets of $\GG^S$ into one big h.f. set $\mu$ which is symmetric under all flips of edge gadgets. Then the vertices $e_0$ and $e_1$ in the edge gadgets in $\mu$ are replaced with the constants $0$ and $1$. Since CPT is choiceless, it cannot arbitrarily choose which of the vertices $e_0, e_1$ is replaced with which constant; it has to do it in both ways. The super-symmetry of $\mu$ ensures that both these replacements lead to the same object. This is necessary to avoid the creation of an exponential number of h.f. sets when all combinations are tried out. After all atoms in $\mu$ have been replaced with $0$ and $1$, the parity of the original CFI-graph $\GG^S$ can be extracted. The property of $\mu$ that we call CFI-symmetry essentially says that $\mu$ is composed out of sub-objects which have a similar behaviour as CFI-gadgets. This seems to be a natural design pattern for super-symmetric objects which encode the parity of $\GG^S$ but one could also conceive super-symmetric objects which are not CFI-symmetric (or vice versa). In short, super-symmetry is the main property of h.f. sets that makes all known CFI-algorithms work, and CFI-symmetry is the established design principle to achieve super-symmetry.

Theorem <ref> reduces the question about the CPT-definability of the CFI-query to the question for the existence of certain non-trivial combinatorial objects, namely polynomial-size symmetric XOR-circuits. Its proof is based on a translation of h.f. sets over CFI-structures into XOR-circuits (Theorem <ref>). This is then combined with a lower bound from <cit.> on the support size of the h.f. sets required to decide the CFI-query – the support size somehow measures how asymmetric a set is (see Section <ref>).
As our second main result shows, it is not at all clear that the required circuit families do exist for all base graphs, and so, obtaining lower bounds for CPT via lower bounds for symmetric circuits may indeed be possible.

Before we come to this second result, in Section <ref>, we also prove a version of the above theorem without the restriction to CFI-symmetric algorithms. It requires that the h.f. sets that are constructed by the algorithm have certain symmetric bases, which we prove to be a more general property than CFI-symmetry. However, since all currently known CPT-algorithms for the CFI-query are CFI-symmetric, it is not clear that this more general (and much more complicated to prove) version of the theorem will actually be necessary at some point in order to separate CPT from $\ptime$. It could be that the class of choiceless algorithms satisfying the said symmetric basis condition is a strictly bigger class than the CFI-symmetric ones, but it could also be that every CPT-algorithm for the CFI-query is equivalent to a CFI-symmetric one (in which case Theorem <ref> would in principle be sufficient to separate CPT from P via symmetric circuit lower bounds).

Our second main result, which we prove in Section <ref>, shows that if we choose the $n$-dimensional hypercubes as the family of base graphs, and impose slightly stronger conditions on the circuits, then it is not possible to satisfy all of them together.

Let $(\H_n)_{n \in \bbN}$ be the family of $n$-dimensional hypercubes and let $\tw_n$ denote the treewidth of $\H_n$. Let $\HH_n^S$ denote a CFI-structure over $\H_n$. There exists no family of symmetric XOR-circuits $(C_n)_{n \in \bbN}$ such that:

* The number of gates in $C_n$ is polynomial in $|\HH^S_n|$.

* The $\Aut(\H_n)$-orbit of the circuit has size exactly one.

* $C_n$ is sensitive to $\Omega(\tw_n)$ input bits.

* For any two gates $g,h$ in $C_n$ such that $h$ is a parent of $g$, it holds $|\Orbit_{(h)}(g)| \in \Oo(\log |\HH_n^S|)$ and $|\Orbit_{(g)}(h)| \in \Oo(\log |\HH_n^S|)$.

Here, $\Orbit_{(h)}(g)$ denotes the orbit of the gate $g$ with respect to the subgroup of $\Aut(\H_n)$ that fixes the gate $h$ (and vice versa for $\Orbit_{(g)}(h)$).

If the four circuit properties were the same as in Theorem <ref>, then this would separate the class of super- and CFI-symmetric choiceless algorithms from $\ptime$. The difference between the two theorems is that here, the circuit has orbit size one, i.e. it is stabilised by the whole group $\Aut(\H_n)$, whereas in Theorem <ref>, the orbit of the circuit is only required to be polynomial. Moreover, here, we have a logarithmic bound on the parents and children (per orbit) of every gate, whereas in Theorem <ref>, the logarithmic bound is on the fan-in dimension of the gates. We define this notion in Section <ref>; we do not know if logarithmic fan-in dimension implies the orbit-wise logarithmic bound on the number of children (or vice versa), and probably, it does not imply the bound on the number of parents. So the “gap” between our two main results concerns how symmetric the circuits have to be and how restricted the connectivity between two consecutive circuit layers is. The proof of Theorem <ref> involves group theoretic techniques based on those from <cit.>.

*Related work
The study of lower bounds for symmetric circuits has proven to be fruitful in many contexts: Anderson and Dawar established families of highly symmetric Boolean circuits with majority gates as a computation model equivalent to fixed-point logic with counting <cit.>. A generalisation of these circuits also captures rank logic <cit.>. Our results regarding CPT are weaker than those in the sense that we do not give a circuit characterisation of CPT but only a structural description of the relevant h.f. sets that CPT can use to decide the CFI-query. Lower bounds against our circuits seem to be generally harder to obtain than for the circuits from <cit.> and <cit.> because our symmetry requirements are weaker (for interesting classes of base graphs, at least).

Besides these connections to logics from finite model theory, symmetric circuits are also interesting in the context of the VP vs VNP question. Dawar and Wilsenach have shown super-polynomial lower bounds on symmetric arithmetic circuits for the permanent <cit.> and determinant <cit.>, for different symmetry groups. Lifting these lower bounds to less symmetric circuits for the permanent would be a step forward towards separating VP from VNP.

Other examples for symmetric circuit lower bounds concern $\AC^0$-circuits for the parity function <cit.>, and Boolean circuits for the multiplication of permutation matrices <cit.>. An interesting aspect about Rossman's lower bound for $\AC^0$-circuits computing parity is the symmetry group he considers: Contrary to the other mentioned results, the symmetry group is in this case not a large permutation group on the input variables but a Boolean vector space which acts on the set of input literals $\{X_1,\overline{X}_1,...,X_n,\overline{X}_n\}$ by swapping specified literals $X_i$ with their respective negations. This is reminiscent of the flips of CFI-gadgets that we encounter in the present article. However, a direct connection between Rossman's lower bound and ours does not seem to exist because his lower bound concerns the parity function, which can be easily expressed in our setting with a single XOR-gate.

Another research direction that is connected with this topic is on extensions of CPT. Lichter and Schweitzer have developed Choiceless Polynomial Time with witnessed symmetric choice <cit.>. This is a logic that allows to make arbitrary choices from definable orbits of the structure, as long as the automorphisms that witness a choice set to be an orbit are also definable. This logic captures polynomial time on all classes of structures where it can define the isomorphism problem, so the witnessed choice operator essentially reduces canonisation to isomorphism testing. A question is in how far our proposed lower bound approach via symmetric circuits also applies to CPT with witnessed choice. As shown in <cit.>, CPT with witnessed choices has no difficulties to define the CFI-query on structures with a single orbit, i.e. unordered CFI-graphs. These are, however, precisely the example for which we have the circuit lower bound, so it seems like the circuit approach exploits a weakness of CPT that does not exist in the witnessed choice extension.

§ PRELIMINARIES

*Bounded variable counting logic

For $k \in \bbN$, $\Cc^k$ denotes the $k$-variable fragment of first-order logic with counting quantifiers. The counting quantifiers in this logic are of the form $\exists^i x \phi(x)$, for every $i \in \bbN$, expressing that at least $i$ elements of the structure satisfy $\phi(x)$. Note that such counting quantifiers can be simulated in ordinary $\FO$ but this requires more than one variable.
Two structures $\AA$ and $\BB$ are called $\Cc^k$-equivalent, denoted $\AA \equiv_{\Cc^k} \BB$, if they satisfy exactly the same $\Cc^k$-sentences.

The standard tool to prove $\Cc^k$-equivalence of two given structures is the bijective $k$-pebble game. It is played on a pair of structures $(\AA,\BB)$
by two players, Spoiler and Duplicator. Duplicator has a winning strategy if and only if $\AA \equiv_{\Cc^k} \BB$ <cit.>. The game proceeds as follows: A position in the game is a set of pebble-pairs $\pi \subseteq A \times B$ of size at most $k$. In each round, Spoiler may pick up any number of pebble-pairs and remove them from the board such that in the resulting position $\pi'$, less than $k$ pebble-pairs remain. Then Duplicator specifies a bijection $f: A \lra B$ such that for every $(a,b) \in \pi'$, $f(a) = b$. Spoiler now puts down a new pebble on some element $a \in A$ of his choice, and the corresponding pebble in $B$ is placed on $f(a)$. If the resulting set of pebble-pairs does not induce a local isomorphism, then Spoiler wins. Duplicator has a winning strategy if she can enforce to play forever without losing. A position $\pi = \{ (a_1,b_1),...,(a_k,b_k)  \}$ is said to induce a local isomorphism if the mapping $g$ that maps each $a_i$ to $b_i$, for $i \in [k]$, is an isomorphism from the induced substructure of $\AA$ with universe $\{a_1,...,a_k\}$ into the induced substructure of $\BB$ with universe $\{b_1,...,b_k\}$.

The positions $\pi$ from which Duplicator has a winning strategy are given by those tuples that have the same $\Cc^k$-type in $\AA$ and $\BB$. The $\Cc^k$-type of a tuple $\bar{a} \in A^{\leq k}$ is the collection of all $\Cc^k$-formulas that are satisfied by $\bar{a}$ in $\AA$. It is known that in each finite structure, every $\Cc^k$-type is definable by a single $\Cc^k$-formula, so even though a type is an infinite collection of formulas, it is semantically equivalent to one finite $\Cc^k$-formula, if the structure is fixed <cit.>.

*Hereditarily finite sets
Let $A$ be a finite set of atoms. Usually, the atoms will be the universe of a structure $\AA$ (and by convention, whenever a structure is called $\AA$, then $A$ denotes its universe).

The set of hereditarily finite objects over $A$, $\HF(A)$, is defined as $\bigcup_{i \in \bbN} \HF_i(A)$, where $\HF_0(A) := A \cup \{\emptyset\}, \HF_{i+1}(A) := \HF_{i}(A) \cup 2^{\HF_{i}(A)}$. The size of a h.f. set $x \in \HF(a)$ is measured in terms of its transitive closure $\tc(x)$: The set $\tc(x)$ is the least transitive set such that $x \in \tc(x)$. Transitivity means that for every $a \in \tc(x)$, $a \subseteq \tc(x)$. Intuitively, one can view $\tc(x)$ as the set of all sets that appear as elements at some nesting depth within $x$.

*Choiceless Polynomial Time
By CPT we always mean Choiceless Polynomial Time with counting. For details and various ways to define CPT formally, we refer to the literature: A concise survey can be found in <cit.>. The work in which Blass, Gurevich and Shelah originally introduced CPT as an abstract state machine model is <cit.> from 1999; later, more “logic-like” presentations of CPT were invented, such as Polynomial Interpretation Logic <cit.> and BGS-logic <cit.>. In short, CPT is like the better-studied fixed-point logic with counting <cit.> plus a mechanism to construct isomorphism-invariant hereditarily finite sets of polynomial size. When a CPT-sentence $\Pi$ is evaluated in a finite structure $A$, then $\Pi$ may augment $A$ with hereditarily finite sets over its universe. The total number of distinct sets appearing in them (i.e. the sum over the sizes of the transitive closures of the h.f. sets) and the number of computation steps is bounded by $p(|A|)$, where $p(n)$ is a polynomial that is explicitly part of the sentence $\Pi$. For the sake of illustration, we sketch the definition of BGS-logic:

The sentences of BGS-logic are called programs. A program is a tuple $\Pi = (\Pi_{\text{step}}(x),\\ \Pi_{\text{halt}}(x),\Pi_{\text{out}}(x),p(n))$. Here, $\Pi_{\text{step}}(x)$ is a BGS-term, $\Pi_{\text{halt}}$ and $\Pi_{\text{out}}$ are BGS-formulas, and $p(n)$ is a polynomial that bounds the time and space used by the program. BGS-terms take as input hereditarily finite sets and output a hereditarily finite set. Examples of such terms are $\Pair(x,y)$, which evaluates to $\{x,y\}$, or $\Union(x) = \bigcup_{y \in x} y$. Furthermore, if $s$ and $t$ are terms, $x$ is a variable, and $\phi$ a formula, then $\{ s(x) \ : \ x \in t \ : \ \phi(t) \}$ is a comprehension term. It applies the term $s$ to all elements of the set defined by $t$ that satisfy $\phi$, and outputs the set of the resulting objects $s(x)$. When a program is evaluated in a given finite structure $A$, then the term $\Pi_{\text{step}}(x)$ is iteratively applied to its own output, starting with $x_0 = \emptyset$. The iteration stops in step $i$ if the computed set $x_i = (\Pi_{\text{step}})^i(\emptyset)$ satisfies $A \models \Pi_{\text{halt}}(x_i)$. The formula $\Pi_{\text{out}}$ defines, in dependence of $x_i$, whether the run is accepting or rejecting, that is, whether $A \models \Pi$ or not. If the length of the run or the size of the transitive closure of $x_i$ exceeds $p(|A|)$ at some point, then the computation is aborted, and $A \not\models \Pi$.

The h.f. sets that appear in the run of a program $\Pi$ on a structure $\AA$ are called the sets that are activated by $\Pi$ on input $\AA$. Formally, the set of active objects is the union over the transitive closures of all the iteration stages $x_i$. The precise definition is not important for the purposes of this article and there exist multiple slightly varying definitions in the literature <cit.> which all essentially describe the same concept.

*Symmetry groups
The two key properties of CPT that we exploit for lower bounds are its polynomial boundedness and symmetry-invariance.
For a structure $\AA$ with universe $A$, we denote by $\Aut(\AA) \leq \Sym(A)$ its automorphism group. Any $\pi \in \Sym(A)$ also acts naturally on $\HF(A)$ by renaming the atoms of the h.f. set according to $\pi$. With this, the symmetry-invariance of CPT can be summarised as follows:

Let $\AA$ be a structure, $x \in \HF(A)$ a hereditarily finite set over $\AA$, $\pi \in \Aut(\AA)$ an automorphism. Any CPT-program that activates $x$ in its run on $\AA$ also activates $\pi(x)$.

We omit the proof because this fact is well-known and follows simply from the fact that the construction steps of the h.f. sets are logically definable. As a consequence of this proposition, CPT-definable objects are closed under their $\Aut(\AA)$-orbits. The orbit of a set $x \in \HF(A)$ is the set $\{\pi(x) \mid \pi \in \Aut(\AA)\}$ of all its images under $\Aut(\AA)$. Since CPT-definable objects must also obey a polynomial size bound, any object whose orbit size is super-polynomial in $|A|$ cannot be activated by any CPT-program on input $\AA$. This consideration is also reflected in the circuit properties from Theorem <ref>.

An important fact from group theory that we sometimes need in this context is the Orbit-Stabiliser Theorem. Applied to h.f. sets over structures, it reads as follows.

Let $\AA$ be a structure, $x \in \HF(A)$ a hereditarily finite set over $\AA$.
Then $|\Orbit(x)| = \frac{|\Aut(\AA)|}{|\Stab(x)|}$.

Here, $\Stab(x) = \{ \pi \in \Aut(\AA) \mid \pi(x) = x \}$ denotes the subgroup of the automorphism group that fixes $x$. More generally, if $H$ is a subgroup of $G$ (denoted $H \leq G$), then the index of $H$ in $G$ is $[G: H] = |G|/|H|$. This is equal to the number of cosets of $H$ in $G$, and if $H$ is the stabiliser of some object $x$, then $[G: H]$ is exactly the orbit size of $x$.

*Linear algebra
We denote by $\bbF_2$ the finite field with two elements $\{0,1\}$, and by $\bbF_2^n$ the set of $n$-tuples over $\bbF_2$, viewed as an $n$-dimensional vector space. We will also be dealing with spaces indexed by some finite (unordered) set $J$, in which case we write $\bbF_2^J$ for the $|J|$-dimensional vector space whose coordinates are the elements of $J$. Similarly, the rows and columns of a matrix can be indexed with such finite unordered sets, so a matrix $M \in \bbF_2^{I \times J}$ describes a linear transformation $M: \bbF_2^J \lra \bbF_2^I$. The image of $M$ is $\Im(M) = \{ M \cdot \mathbf{v} \mid \mathbf{v} \in \bbF_2^J \}$, and the kernel is $\Ker(M) = \{\mathbf{v} \in \bbF_2^J \mid M \cdot \mathbf{v} = \mathbf{0}\}$. The Rank Theorem states that $|J| = \rk(M) + \dim(\Ker(M))$. The rank $\rk(M)$ denotes the dimension of $\Im(M)$. It is equal both to the dimension of the space spanned by the column vectors of $M$ and the dimension of the space spanned by the row vectors.

§ UNORDERED CAI-FÜRER-IMMERMAN GRAPHS

Fix an undirected (and unordered) connected graph $G = (V,E)$ as the base graph for the CFI-construction. We turn $G$ into a CFI-graph by replacing the edges with certain edge-gadgets and the vertices with vertex-gadgets. There are two types of vertex-gadgets, called odd and even. To construct a concrete CFI-graph over $G$, we have to fix a set $S \subseteq V$ of vertices which are replaced by the odd gadget. The vertices in $V \setminus S$ will be turned into the even gadget. Following the notation in <cit.>, we denote the resulting CFI-graph by $\GG^S$. The precise definition is as follows:
Let $\widehat{E} := \{ e_0, e_1 \mid e \in E \}$.
These are the vertices that will form the edge-gadgets of $\GG^S$, so there are two vertices per edge-gadget. To define the vertices in vertex-gadgets, we let, for each $v \in V$,

\begin{align*}
v^*_S := \begin{cases}
\{  v^X \mid X \subseteq E(v), |X| \text{ even }   \} & \text{ if } v \notin S\\
\{  v^X \mid  X \subseteq E(v), |X| \text{ odd }  \} & \text{ if } v \in S
\end{cases}
\end{align*}

Here, $E(v) \subseteq E$ are the edges incident to $v$ in $G$. The vertices in $v^*_S$ form the vertex-gadget of $v$. In total, we let

\[
\widehat{V}_S := \bigcup_{v \in V} v^*_S.
\]

Then the vertex-set of $\GG^S$ is $V(\GG^S) := \widehat{V}_S \cup \widehat{E}$. The edges of the CFI-graph are given by

\[
E(\GG^S) := \{ \{ v^X, e_i  \} \mid v^X \in \widehat{V}_S, e_i \in \widehat{E}, |X \cap \{e\}| = i \} \cup \{ \{e_0,e_1\} \mid e \in E  \}.
\]

In other words, for every $v \in V$, we connect each $v^X \in v^*_S$ with the edge-gadgets of all edges $e \in E(v)$ in such a way that $v^X$ is connected with $e_0$ if $e \notin X$, and otherwise with $e_1$. Also, we connect $e_0$ and $e_1$ to ensure that no automorphism of $\GG^S$ can tear apart the edge-gadgets. Our CFI-graphs are unordered, so the only relation of the structure $\GG^S$ is the edge relation $E$.

Below are the gadgets $v^*_S, w^*_S$ for two vertices $v,w \in V$, and the gadget for the edge $e \in E$ connecting them. In this example, we have $v \notin S, w \in S$, and $E(v) = \{e,f,g\}, E(w) = \{e,h,i\}$. Only the edge $e$ is drawn. Notice that $v^*_S$ and $w^*_S$ look the same when we only consider their connections to the $e$-gadget, even though one gadget is even and the other is odd.

[dot/.style=draw,circle,minimum size=1.5mm,inner sep=0pt,outer sep=0pt,fill=blue,circ/.style=draw,circle,minimum size=2.5mm,inner sep=0pt, fill=red,
circY/.style=draw,circle,minimum size=2.5mm,inner sep=0pt, fill=yellow]
[dot,label=below:$e_0$] (e0) at (0,0) ;
[dot,label=$e_1$] (e1) at (0,1) ;

[radius=1,fill=red, opacity=0.2] (-3.75,0.5) circle;
[radius=1,fill=yellow, opacity=0.2] (3.75,0.5) circle;

[circ,label=$v^\emptyset$] (v0) at (-3.75,-0.2) ;
[circ,label=$v^{\{e,f\}}$] (vef) at (-3.75,1.2) ;
[circ,label=$v^{\{e,g\}}$] (veg) at (-4.5,0.5) ;
[circ,label=$v^{\{f,g\}}$] (vfg) at (-3,0.5) ;

[circY,label=$w^{\{e\}}$] (we) at (3.75,1.2) ;
[circY,label=$w^{\{h\}}$] (wh) at (3.75,-0.2) ;
[circY,label=$w^{\{i\}}$] (wi) at (4.5,0.5) ;
[circY,label=$w^{\{e,h,i\}}$] (wehi) at (3,0.5) ;

(v0) – (e0);
(vef) – (e1);
(veg) – (e1);
(vfg) – (e0);

(we) – (e1);
(wh) – (e0);
(wi) – (e0);
(wehi) – (e1);

(e0) – (e1);

Gadgets $v^*_S, w^*_S$, connected by the gadget for the edge $e$.

The CFI-query asks for the parity of $|S|$, given a CFI-graph $\GG^S$. This is essentially the same question as the graph isomorphism problem for CFI-graphs:

For two given CFI-graphs over the same base graph, it holds

\[
\GG^S \cong \GG^R \text{ if and only if } |S| \equiv |R| \mod 2.
\]

Alternatively, deciding the parity of $|S|$ can be phrased as a linear equation system over $\bbF_2$ in the variables $\widehat{E}$ (see <cit.>). Since the reduction to a linear equation system is easily computable from the given CFI-graph $\GG^S$, and linear equation systems can be efficiently solved using, for example, Gaussian elimination, the CFI-query is decidable in polynomial time.

For logics that lack the ability to create higher-order objects, such as bounded-variable counting logic and hence FPC, it is provably impossible to distinguish non-isomorphic CFI-graphs, provided that the treewidth of the base graphs is super-constant:

Let $G = (V,E)$ be an undirected connected graph with treewidth $t$. Then for any two sets $S, S' \subseteq V$, it holds
\GG^S \equiv_{\Cc^t} \GG^{S'},
even if $\GG^S \not\cong \GG^{S'}$.

This holds because Duplicator has a winning strategy in the bijective $t$-pebble game on $\GG^S$ and $\GG^{S'}$. Intuitively, the difference between $\GG^S$ and $\GG^{S'}$ manifests itself in one single edge whose gadget is twisted, and the aim of Duplicator is to move this twist around in such a way that it is never exposed by the $t$ pebbles. This can be achieved by playing similarly as the robber in the cops and robbers game which witnesses the treewidth to be at least $t$.

§.§ Automorphisms of unordered CFI-graphs

For a CFI-graph $\GG^S$ over an unordered base graph $G = (V,E)$, two different kinds of automorphisms play a role:
Firstly, there are what we call “CFI-automorphisms” or -isomorphisms. These are induced by swapping $e_0$ and $e_1$ in some edge-gadgets (this is called “flipping the edge”). Secondly, there are the automorphisms of the underlying graph $G$ itself.

To speak about the CFI-isomorphisms, we use the terminology from <cit.>: For a given base graph $G$, we consider not only a concrete CFI-instance with odd and even vertex gadgets, but we can also construct the “full” CFI-graph $\GG$, in which every vertex gadget is both even and odd. Formally, for $v \in V$, let $v^* := v^*_\emptyset \cup v^*_{\{v\}} = \{  v^X \mid X \subseteq E(v) \}$, and $\widehat{V} := \bigcup_{v \in V} v^*$.
The vertex-set of $\GG$ is $\widehat{V} \cup \widehat{E}$, and the edge-set is

\[
E(\GG) := \{ \{ v^X, e_i  \} \mid v^X \in \widehat{V}, e_i \in \widehat{E}, |X \cap \{e\}| = i \} \cup \{ \{e_0,e_1\} \mid e \in E  \}.
\]

Every CFI-instance $\GG^S$ is an induced subgraph of $\GG$.

For each edge $e = \{v,w\} \in E$, let $\rho_e$ denote the automorphism of $\GG$ induced by flipping the edge $e$. Formally, $\rho_e(e_0) = e_1, \rho_e(e_1) = e_0$, and $\rho_e(v^X) = v^{X \triangle \{e\}}$, $\rho_e(w^X) = w^{X \triangle \{e\}}$ for all $v^X, w^X \in v^* \cup w^*$. All other vertices in $\widehat{V}$ are fixed by $\rho_e$. One can check that this is indeed an automorphism of $\GG$; furthermore, $\rho_e$ is an isomorphism from any CFI-instance $\GG^S$ to $\GG^{S \triangle \{v,w\}}$ (see also <cit.>).
It is easy to see that these edge-flip automorphisms commute, so for $F = \{e^1,...,e^m\} \subseteq E$ we may write $\rho_F$ for $\rho_{e^1} \circ \rho_{e^2} \circ ... \circ \rho_{e^m}$. So in total, for every $F \subseteq E$, $\rho_F$ is an automorphism of $\GG$. For any edge-set $F \subseteq E$, and $v \in V$ let $\deg_F(v) := | E(v) \cap F|$, i.e. the number of incident edges that are in $F$. We have $\rho_F(\GG^S) = \GG^{S \triangle T}$, where $T = \{v \in V \mid \deg_F(v) \text{ is odd } \}.$
In particular, if every $v \in V$ is incident to an even number of edges in $F$ (so $F$ is the symmetric difference over a set of cycles in $G$), then $\rho_F$ is also an automorphism of $\GG^S$, not only of $\GG$.
To sum up, we have the following groups of CFI-automorphisms of $\GG$ and $\GG^S$:

\[
\Aut_{\CFI}(\GG) := \{\rho_F \mid F \subseteq E \}.
\]

This group is isomorphic to the Boolean vector space $\bbF_2^E$: Each $F \subseteq E$ is identified with its characteristic vector $\chi(F) \in \bbF_2^E$. It holds $\rho_F \circ \rho_{F'} = \rho_{F \triangle F'}$, and this corresponds to the vector $\chi(F) + \chi(F') \in \bbF_2^E$.

As already said, for a CFI-instance $\GG^S$, i.e. an induced subgraph of $\GG$, we have

\[
\Aut_{\CFI}(\GG^S) := \{ \rho_F \in \Aut_{\CFI}(\GG) \mid  \deg_F(v) \text{ is even for every } v \in V \}.
\]

This group is isomorphic to a subspace of $\bbF_2^E$.
In addition to the CFI-automorphisms, we also have to consider $\Aut(G) \leq \Sym(V)$, i.e. the automorphism group of the unordered underlying graph; this is different from the typical scenario studied in the literature, where $G$ is ordered and so the automorphisms of $\GG^S$ are just given by the edge-flips.
In total, the automorphism group of the full CFI-graph $\GG$ is isomorphic to the following semi-direct product:

\[
\Aut(\GG) \cong \Aut_{\CFI}(\GG) \rtimes \Aut(G)  = \{ (\rho_F, \pi) \mid \rho_F \in \Aut_{\CFI}(\GG), \pi \in \Aut(G)  \}.
\]

The action of a pair $(\rho_F, \pi)$ on $V(\GG)$ is determined by its action on $\widehat{E}$: Let $e_i \in \widehat{E}$ with $i \in \{0,1\}$ and $e = \{v,w\} \in E$. Then $(\rho_F,\pi)(e_i) = f_j$, where $f = \{\pi(v), \pi(w)\}$, and $j = i + |F \cap \{e\}| \mod 2$. This action on $\widehat{E}$ extends to an automorphism of $\GG$ in a unique way. The automorphism group $\Aut(\GG^S)$ of a concrete CFI-instance is a subgroup of this.

§.§ Symmetries and supports of hereditarily finite sets over CFI-structures

Let $\GG^S$ be a CFI-graph over $G = (V,E)$ and $x \in \HF(\widehat{E})$.
We only consider objects in $\HF(\widehat{E})$ instead of $\HF(\widehat{E} \cup \widehat{V})$ because this is easier and atoms $v^X \in \widehat{V}$ can be uniquely described by their neighbourhood in $\GG^S$, which is again a set over the atoms $\widehat{E}$. Therefore, we can pretend that any CPT-algorithm for the CFI-query only uses h.f. sets over $\widehat{E}$.

The automorphism group $\Aut(\GG^S)$, as well as the edge-flip-group $\Aut_{\CFI}(\GG)$, and the automorphisms of the base graph $\Aut(G)$ act on $\widehat{E}$ and therefore also on $\HF(\widehat{E})$: For example, let $\pi \in \Aut(G)$, and $x \in \HF(\widehat{E})$. Then $\pi x = \{ \pi y \mid y \in x  \}$. If $x$ is an atom $e_i$, with $i \in \{0,1\}$ and $e \in E$, then $\pi x = \pi(e)_i$.

An automorphism $\pi \in \Aut(G)$ stabilises an object $x \in \HF(\widehat{E})$, if $\pi x = x$. More precisely, this means that $\pi$, which acts on the atoms of $x$, extends to some automorphism $\sigma$ of the DAG-structure $(\tc(x), \in)$, such that for every atom $e_i \in \tc(x)$, $\sigma(e_i) = \pi(e)_i$. As already said, $\Aut(\GG^S)$ is composed of edge flips and automorphisms of the base graph. We separate the effect of these two subgroups on the elements of $\HF(\widehat{E})$ and consider the following orbits and stabilisers for $x \in \HF(\widehat{E})$. Since the group of edge flips, $\Aut_{\CFI}(\GG)$, is isomorphic to the Boolean vector space $\bbF_2^E$, we often identify an automorphism $\rho_F \in \Aut_{\CFI}(\GG)$ with its characteristic vector $\chi(F) \in \bbF_2^E$.

\begin{align*}
\Orb_E(x) &:= \{ \rho_F(x) \mid \rho_F  \in \Aut_{\CFI}(\GG) \}.\\
\Stab_E(x) &:= \{ \chi(F) \mid \rho_F \in \Aut_{\CFI}(\GG), \rho_F(x) = x \} \leq \bbF_2^E.\\
\Orb_{\CFI}(x) &:= \{ \rho_F(x) \mid \rho_F  \in \Aut_{\CFI}(\GG^S) \}.\\
\Stab_{\CFI}(x) &:= \{ \chi(F) \mid \rho_F \in \Aut_{\CFI}(\GG^S), \rho_F(x) = x \} \leq \bbF_2^E.\\
\Orb_{\GG^S}(x) &:= \{(\rho_F,\pi)(x) \mid (\rho_F,\pi) \in \Aut(\GG^S) \}.\\
\Stab_{\GG^S}(x) &:= \{ (\rho_F,\pi) \in \Aut(\GG^S) \mid (\rho_F,\pi)(x) = x \}.\\
\Orb_{G}(x) &:= \{(\rho_\emptyset,\pi)(x) \mid \pi \in \Aut(G) \}.\\
\Stab_{G}(x) &:= \{ \pi \in \Aut(G) \mid (\rho_{\emptyset},\pi)(x) = x \}.\\
\maxOrb_E(x) &:= \max_{y \in \tc(x)} |\Orb_E(y)|.\\
\maxOrb_\CFI(x) &:= \max_{y \in \tc(x)} |\Orb_\CFI(y)|.
\end{align*}

It should be emphasised that $\Stab_E(x)$ is a subspace of $\bbF_2^E$, so it makes sense to speak about its dimension and to apply linear transformations to it.
At this point, we observe for future reference that all objects in the same $\Aut_{\CFI}(\GG)$-orbit have the same $\Aut_{\CFI}(\GG)$-stabiliser because the group is Abelian:

Let $x, x' \in \HF(\widehat{E})$ such that $x' = \rho_F(x)$, for some $\rho_F \in \Aut_{\CFI}(\GG)$. Then $\Stab_E(x) = \Stab_E(x')$.

We have $\Stab_E(x') = \{ \chi(F) + \alpha + \chi(F) \mid \alpha \in \Stab_E(x) \}$. Since $\chi(F) = \chi(F)^{-1}$ and $\bbF_2^E$ is Abelian, we have $\Stab_E(x') = \Stab_E(x)$.

We also observe that the two different $\maxOrb$-parameters of a h.f. set can be bounded in terms of the size and orbit size of $x$.

Let $x \in \HF(\widehat{E})$. Then $\maxOrb_E(x) \leq |\Orb_E(x)| \cdot |\tc(x)|$ and
$\maxOrb_\CFI(x) \leq |\Orb_\CFI(x)| \cdot |\tc(x)|$.

Let $y \in \tc(x)$ be the set where $\maxOrb_E(x)$ is attained, i.e. $|\Orb_E(y)| = \maxOrb_E(x)$. Let $Y := \Orb_E(y) \cap \tc(x)$. Clearly, for any $\rho_F \in  \Aut_{\CFI}(\GG)$, $\rho_F(Y) \subseteq \tc(\rho_F(x))$, and $\rho_F(x) \in \Orb_E(x)$. Hence:

\[
|\Orb_E(y)| \leq   \Big| \bigcup_{\rho_F\in \Aut_{\CFI}(\GG)} \rho_F(Y) \Big| \leq |\Orb_E(x)| \cdot |\tc(x)|.
\]

Similarly, the statement for $\maxOrb_{\CFI}(x)$ is proven.

In <cit.>, the term super-symmetry was introduced for h.f. sets which are fixed by all automorphisms in $\Aut_{\CFI}(\GG)$. The notion of super-symmetry that is needed for our Theorem <ref> can be relaxed a bit, in the sense that the orbit size w.r.t. $\Aut_{\CFI}(\GG)$ does not need to be exactly one.

Fix a family of CFI-graphs $(\GG^S_n)_{n \in \bbN}$ and a $\mu_n \in \HF(\widehat{E}_n)$ for every $n$. The objects $\mu_n$ are super-symmetric if
|\Orb_E(\mu_n)| \leq \text{\upshape poly}(|\GG^S_n|).

If a set is super-symmetric and CPT-definable, then we have a handle on its parameter $\maxOrb_{E}$:

If $\mu_n$ is super-symmetric and CPT-definable in $\GG^S_n$, then $\maxOrb_{E}(\mu_n)$ is polynomially bounded in $|\GG^S_n|$.

By super-symmetry, $|\Orb_E(\mu_n)|$ is polynomially bounded. By CPT-definability, $|\tc(\mu_n)|$ is polynomially bounded. Hence the statement follows with Lemma <ref>.

So super-symmetric objects in this sense satisfy the same orbit bound with respect to the bigger symmetry group $\bbF_2^E \cong \Aut_{\CFI}(\GG)$ as all CPT-definable objects naturally do with respect to the automorphism group of the input structure.

*Supports for CFI-automorphisms
Generally, a support of a permutation group $\Gamma \leq \Sym(A)$ is a subset $S \subseteq A$ such that the pointwise stabiliser of $S$ in $\Sym(A)$ is a subgroup of $\Gamma$. A support of a h.f. set is a support of its stabiliser group. For subgroups of $\Aut_{\CFI}(\GG)$, we will use a different notion, that we call CFI-support. The reason why we need a specific type of support for these groups is because otherwise, the group $\Aut_{\CFI}(\GG)$ does not admit unique minimum supports.

A CFI-support of an object $x \in \HF(\widehat{E})$ is a subset $S \subseteq E$ such that every $\rho_F \in \Aut_{\CFI}(\GG)$ with $F \cap S = \emptyset$ fixes $x$.

There is always a unique minimal CFI-support:

Let $\GG^S$ be a CFI-instance and $x \in \HF(\widehat{E})$. Let $A_1,A_2 \subseteq E$ be CFI-supports of $x$. Then $A_1 \cap A_2$ is also a CFI-support of $x$.

Assume $A_1 \cap A_2$ was not a CFI-support of $x$. Then there is $F \subseteq E$ disjoint from $A_1 \cap A_2$ such that $\rho_F(x) \neq x$. Let $F_1 := F \cap A_1$ and $F_2 := F \cap A_2$. These sets are both non-empty, because: If $F$ did not intersect $A_1$, then $\rho_F(x) = x$ because $A_1$ is a CFI-support for $x$. Similarly for $A_2$. Also, by assumption, $F_1$ and $F_2$ are disjoint from $A_1 \cap A_2$, and therefore, also $F_1 \cap F_2 = \emptyset$. Furthermore, $F' := F \setminus (F_1 \cup F_2)$ is disjoint from $A_1 \cup A_2$ and therefore, $\rho_{F'}$ fixes $x$. It follows that flipping the edges in $F_1 \cup F_2$ moves $x$, because by assumption, $\rho_F(x) \neq x$. But this is a contradiction because $\rho_{F_1}(x) = x$ (since $F_1$ is disjoint from the support $A_2$), and analogously, $\rho_{F_2}(x) = x$.

This justifies the following definition:

For $x \in \HF(\widehat{E})$,
$\sup_{\CFI}(x) \subseteq E$ denotes
the unique minimal subset of $E$ that is a CFI-support of $x$.

As explained above, for general CPT-definable objects, the orbit size can only be bounded when the “true” automorphism group $\Aut_{\CFI}(\GG^S)$ is considered. Only when the object is additionally super-symmetric, also the $\Aut_{\CFI}(\GG)$-orbit size is polynomial.
However, depending on the structure of the base graph, we can sometimes bound the $\Aut_{\CFI}(\GG)$-orbit size as well, even if the object is not necessarily super-symmetric:

Let $\mu \in \HF(\widehat{E})$ be a h.f. set over $\GG^S$. Let $k$ be the number of connected components in the graph $G - \sup_{\CFI}(\mu)$ (i.e. the base graph after removing the edges in the minimum CFI-support).
Then $|\Orb_{E}(\mu)| \leq 2^{k^2}\cdot |\Orb_{\GG^S}(\mu)|$.

Let $A = \sup_{\CFI}(\mu) \subseteq E$ be the smallest CFI-support of $\mu$. Then for every $\rho_F \in \Aut_{\CFI}(\GG)$ with $F \cap A = \emptyset$, it holds that $\rho_F(\mu) = \mu$. Thus, the effect of an edge-flip $\rho_F$ on $\mu$ depends only on $F \cap A$. So we have:

\[
|\Orb_{E}(\mu)| \leq 2^{|A|},
\]

because there are $2^{|A|}$ ways how any $F \subseteq E$ can intersect the support $S$, and if $F \cap A = F' \cap A$, then also $\rho_F(\mu) = \rho_{F'}(\mu)$.

Now we compute a lower bound on  $|\Orb_{\GG^S}(\mu)|$ by analysing how many subsets of $A$ can occur as the intersection $F \cap A$ for an automorphism $\rho_F \in \Aut_{\CFI}(\GG^S)$. In contrast to the edge-flips in $\Aut_{\CFI}(\GG)$, these are the edge-flips along cycles in $G$. Let $X_1,...,X_k \subseteq V(G)$ denote the vertex-sets of the connected components in the graph $G - A$. We partition the edge-set $A$ into at most $k^2$ many subsets, according to the components that the edges connect. So for each pair $(i,j) \in [k]^2$, let $\Aa_{(i,j)} \subseteq A$ denote those edges in $A$ that run between the components $X_i$ and $X_j$. Now it can be seen that for every pair $i \neq j$, for every $B \subseteq \Aa_{(i,j)}$ of even cardinality, there exists some symmetric difference of cycles $C_B$ in $G$ whose intersection with $A$ is exactly $B$. This is because any two edges $e,e' \in \Aa_{(i,j)}$ lie on a cycle through the components $X_i$ and $X_j$. For $\Aa_{(i,i)} \subseteq A$, every subset $B \subseteq \Aa_{(i,i)}$ can be generated by the symmetric difference of some cycles because the endpoints of every $e \in \Aa_{{i,i}}$ are in the same connected component (but for simplicity, we pretend that also in this case, only the even subsets of $\Aa_{(i,i)}$ can be hit by the symmetric difference of some cycles). Summing up these considerations, we have:

\begin{align*}
&|\{  B \subseteq A \mid \text{ there exists a } \rho_F \in \Aut_{\CFI}(\GG^S) \text{ such that } F \cap A = B \}|\\
&\geq \prod_{(i,j) \in [k]^2} 2^{|\Aa_{(i,j)}|-1} = 2^{|A|-k^2}.
\end{align*}

Let $s$ denote the number of $B \subseteq A$ in the above set such that flipping $B$ stabilises $\mu$. Then by the Orbit-Stabiliser Theorem, we have $|\Orb_{\GG^S}(\mu)| \geq 2^{|A|-k^2}/s$ and $|\Orb_E(\mu)| \leq 2^{|A|}/s$. Putting these two inequalities together, we get the desired bound $|\Orb_{E}(\mu)| \leq 2^{k^2}\cdot |\Orb_{\GG^S}(\mu)|$.

This lemma essentially says that it does not make a difference whether we consider orbit-sizes with respect to the group $\Aut_{\CFI}(\GG)$ of all edge flips or the group $\Aut_{\CFI}(\GG^S)$ of cycle edge flips, as long as the CFI-support of an object separates the base graph only into a small number of components:

Fix a family $(\GG_n^S)_{n \in \bbN}$ of CFI-structures. Let $\mu_n \in \HF(\widehat{E}_n)$. If the number of connected components in $G_n - \sup_{\CFI}(\mu_n)$ is at most $\Oo(\sqrt{\log |\GG^S_n|})$, then $|\Orb_{E}(\mu_n)| \leq \text{\upshape poly}(|\GG^S_n|) \cdot |\Orb_{\GG^S}(\mu)|$.

§ CFI-SYMMETRIC HEREDITARILY FINITE SETS AND ALGORITHMS

The CFI-query is definable in CPT on instances that arise from linearly ordered base graphs, base graphs that come with a preorder with colour classes of logarithmic size, and base graphs of linear degree <cit.>. All these CPT-algorithms depend on the construction of a particular super-symmetric h.f. set $\mu \in\HF(\widehat{E})$ that encodes the parity of $|S|$, given an instance $\GG^S$. We isolate another property of these h.f. sets, besides super-symmetry, which is responsible for their small orbit size and suitability for encoding parities. We call this CFI-symmetry. Intuitively, a set $\mu \in \HF(\widehat{E})$ is CFI-symmetric if its “building blocks” behave similarly as CFI-gadgets in CFI-graphs, in the sense that they are “flipped” whenever an even number of “incident gadgets” is flipped. These building blocks are the connected components of sets. To define these, let a CFI-graph $\GG^S$ and a set $\mu \in \HF(\widehat{E})$ be fixed, and let $\sim_E$ be the following equivalence relation on the elements $x \in \tc(\mu)$: For $x,x' \in \tc(\mu)$, we write $x \sim_E x'$ iff there exists an edge-flip $\rho_F \in \Aut_{\CFI}(\GG)$ such that $x' = \rho_F(x)$.
The $\sim_E$-equivalence class in $\tc(\mu)$ of an object $x \in \tc(\mu)$ is denoted $[x]_{\sim_E}$ or $[x]$.
The relation $\sim_E$ induces a partition $\Cc(x)$ on each $x \in \tc(\mu)$, namely $\Cc(x) := \{([z]_{\sim_E} \cap x) \mid z \in x\}$. In <cit.>, the elements of $\Cc(x)$ are called the connected components of $x$. Now in a CFI-symmetric object, each connected component $\gamma \in \Cc(x)$, for each $x \in \tc(\mu)$, behaves like a CFI-gadget. That is, the component has exactly two images under $\Aut_{\CFI}(\GG)$: It can either be flipped or stabilised, and which of these two is the case, depends on the parity of flipped components in the elements of $\gamma$. Before we formalise this, we consider an example of a small “parity-tracking” h.f. set that is constructed similarly as in the algorithms from <cit.> and <cit.>.

Here is an example h.f. set $\mu_{\{e,f,g\}} \in \HF( \widehat{E} )$ with $E = \{e,f,g\}$. It tracks the parity of edge-flips for the edges $e,f,g$. For better readability, the set is printed in a structured form, so the sets $\mu_{\{f,g\}}$ and $\widetilde{\mu}_{\{f,g\}}$ are shown in the level below.

(mu) at (0,0) $\mu_{\{e,f,g\}} = $;
(muSet) [right = 0.1cm of mu] $\Big\{ \  \{  \mu_{\{f,g\}} , e_0  \}, \{  \widetilde{\mu}_{\{f,g\}}  , e_1 \}  \ \Big\}$;
(mufg) [below  = 0.4cm of muSet ] $\{\{ f_0, g_0 \}, \{ f_1,g_1\} \}$  ;
(muTildefg) [below right = 0.4cm and 0.1cm of muSet]  $\{ \{ f_0, g_1 \}, \{ f_1,g_0\} \}$ ;
[draw=none] (muSetSouthWest) at (2,-0.2) ;
[draw=none] (muSetSouthEast) at (4.5,-0.2) ;
(mufg) – (muSetSouthWest);
(muTildefg) – (muSetSouthEast);

Each of the $\mu$-objects has only one connected component that consists of two sets which are related by $\sim_E$. For example, the two elements of $\mu_{\{e,f,g\}}$ are mapped to each other whenever an even number of edges is flipped.      These two elements of $\mu_{\{e,f,g\}}$ themselves have two connected components: Clearly, $e_0$ and $\mu_{\{f,g\}}$ cannot be mapped to each other by any edge-flip. The same goes for example for $f_0$ and $g_0$. They form distinct components of the set $\{f_0,g_0\}$, while $\{ \{f_0, g_0\}, \{ f_1, g_1 \} \}$ again only has one component that is stabilised if and only if an even number of edges in $\{f,g\}$ is flipped. This pattern of alternation between sets with two components and sets with one component is typical of the parity-tracking objects constructed by the known CFI-algorithms.

Now we can observe that the objects which behave analogously to CFI-gadgets are the connected components inside the sets, not the sets in $\tc(\mu_{\{e,f,g\}})$ themselves. For example, the sets $\{f_0, g_0\}$ and $\{ \mu_{\{f,g\}}, e_0 \}$ cannot be “flipped” between two states, like a CFI-gadget. Their orbit with respect to edge-flips has size four. But whenever these sets occur as elements of another set, they occur together with a counterpart from their orbit, which ensures that its connected component inside the parent set again has the “CFI-property”: It has orbit-size two and is “flipped” if and only if an even number of elements are flipped. Note that the number of flipped elements is always the same in every member of a connected component. For example, in the component $\{ \{f_0, g_0 \}, \{f_1, g_1 \}  \}$, it is clear that $f_0$ is flipped iff $f_1$ is flipped and $g_0$ is flipped iff $g_1$ is; so $\{f_0, g_0  \}$ and  $\{f_1, g_1 \} $ are always affected by the same number of flips, and the same is true for $\{  \mu_{\{f,g\}} , e_0  \}$ and $\{  \widetilde{\mu}_{\{f,g\}}  , e_1 \}$. Therefore, it makes sense to view the connected components inside each set as analogues of CFI-vertex-gadgets, and the elements of each/any member of a component as its “incident edges”, whose flips affect the “vertex-gadget”.

Generalising the example, the structural pattern of such parity-tracking objects can be formalised like this:

Let $\mu \in \HF(\widehat{E})$, $x \in \tc(\mu)$, and $\gamma \subseteq x$ be a connected component of $x$. Then we say that $\gamma$ is CFI-symmetric if $|\Orb_{E}(\gamma)| = 2$ and for each $\rho_F \in \Aut_{\CFI}(\GG)$, it holds $\rho_F(\gamma) = \gamma$ iff for each/any $y \in \gamma$, the number of flipped components of $y$, that is $|\{ \gamma' \in \Cc(y) \mid \rho_F(\gamma') \neq \gamma'   \}|$, is even.

The set $\mu$ is CFI-symmetric if the following two conditions are satisfied:

* For each $\rho_F \in \Aut_{\CFI}(\GG)$, it holds $\rho_F(\mu) = \mu$ iff the number of flipped components of $\mu$, that is, $|\{ \gamma \in \Cc(\mu) \mid \rho_F(\gamma) \neq \gamma  \}|$, is even.

* For every $x \in \tc(\mu)$, every connected component $\gamma \in \Cc(x)$ is CFI-symmetric.

We will never deal with objects $\mu \in \HF(\widehat{E})$ in which only some, but not all connected components of sets in $\tc(\mu)$ are CFI-symmetric. Therefore, when we speak of “flipped components of $y$” in the above definition, and denote these as $\{ \gamma' \in \Cc(y) \mid \rho_F(\gamma') \neq \gamma' \}$, the component $\rho_F(\gamma') \neq \gamma'$ really is the “flip” of $\gamma'$, because the orbit of $\gamma'$ has size exactly two.

We still have to show that the formulation “each/any” in Definition <ref> is indeed justified, as we already indicated in the example.

Let $\mu \in \HF(\widehat{E})$, $x \in \tc(\mu)$, and $\gamma \subseteq x$ be a connected component of $x$. For any two $y,y' \in \gamma$ and every $\rho_F \in \Aut_{\CFI}(\GG)$, it holds

\[
|\{ \gamma' \in \Cc(y) \mid \rho_F(\gamma') \neq \gamma'   \}| = |\{ \gamma' \in \Cc(y') \mid \rho_F(\gamma') \neq \gamma'   \}|.
\]

Fix $\rho_F \in \Aut_{\CFI}(\GG)$. Further, let $\rho \in \Aut_{\CFI}(\GG)$ be an automorphism such that $\rho(y) = y'$. This exists because $y \sim_E y'$. Thus, $\rho$ induces a bijection from $\Cc(y)$ to $\Cc(y')$, as it maps each connected component of $y$ to a connected component of $y'$.
We show that for each component $\gamma' \in \Cc(y)$ it holds: $\rho_F(\gamma') = \gamma'$ iff $\rho_F(\rho(\gamma')) = \rho(\gamma')$. If $\rho_F(\gamma') = \gamma'$, then we have (because $\Aut_{\CFI}(\GG)$ is Abelian): $\rho_F(\rho(\gamma')) = \rho(\rho_F(\gamma')) = \rho(\gamma)$. Conversely, if $\rho_F(\rho(\gamma')) = \rho(\gamma')$, then $\gamma' = \rho^{-1}(\rho(\gamma')) = \rho^{-1}(\rho_F(\rho(\gamma'))) = \rho_F(\gamma')$, where the last equality is again by commutativity. The lemma follows because $|\Cc(y)| = |\Cc(y')|$.

A $\CPT$-program $\Pi$ that decides the CFI-query on a class $\Kk$ of base graphs is called CFI-symmetric if it activates a CFI-symmetric h.f. set $\mu \in \HF(\widehat{E})$ on every input $\GG^S$ over a base graph $G \in \Kk$ (and this set $\mu$ is necessary for deciding the CFI-query). Similarly, $\Pi$ is called super-symmetric if it necessarily activates a super-symmetric set. When $\Pi$ is both CFI- and super-symmetric, then the relevant h.f. set it activates satisfies both properties at the same time.

The condition that $\mu$ is necessary to decide the query is supposed to mean that $\Pi$ could not succeed without the activation of $\mu$. This makes sense in light of Theorem <ref>, which says that the activation of a h.f. set with large support is necessary to define the CFI-query in CPT. Every currently known CPT-algorithm for the CFI-query is CFI-symmetric in this sense. We do not explicitly prove this here because this would also require to include a survey on the algorithms from <cit.> and <cit.> in this already long article. However, it is not too difficult to verify that the h.f. sets defined in those two papers exactly satisfy the design pattern that we call CFI-symmetry here.

Now that we have established the notion of CFI-symmetric sets and algorithms, one may ask how natural this definition is and why we focus on such objects. The answer to the second question is that our construction of XOR-circuits which capture the relevant complexity parameters of sets in $\HF(\widehat{E})$ works best if we restrict our attention to CFI-symmetric sets. Towards the end of the chapter, we will discuss in how far it may be possible to overcome this restriction and transform all sets in $\HF(\widehat{E})$ into XOR-circuits.

The other motivation for defining CFI-symmetry in this way is the observation that we made in Example <ref>, and which is in fact true of any of the various super-symmetric h.f. sets that play the key role in the CFI-algorithms from <cit.> and <cit.>: All these objects are built out of sets that alternate between having one connected component and having multiple components. The sets with multiple components always introduce a new vertex or edge gadget of the input graph into the object, while the sets with one component ensure symmetry: They are “flippable” just like CFI-gadgets and their two possible “states” are well-suited to track parities, which is what the CFI-query is all about. This structural pattern, that has been applied successfully in these various CFI-algorithms, is captured by our notion of CFI-symmetry. The class of CPT-algorithms that use CFI-symmetric objects to solve the CFI-query can thus be considered a fairly natural one.

The feature that makes these objects useful for deciding the CFI-query is, however, super-symmetry and not CFI-symmetry. Super-symmetry is needed in all the known algorithms because it allows to arbitrarily substitute the vertices $e_0,e_1$ from each edge gadget with $0$ and $1$ in both possible ways without producing two distinct objects (since the object is invariant under any edge flip). The super-symmetric sets in these algorithms happen to be sets of CFI-symmetric objects. Super-symmetry is achieved by constructing an object which behaves like a CFI-vertex-gadget that is incident to every edge of the base graph twice. That is, we can imagine the construction process of the desired super-symmetric object as a successive contraction of the input CFI-graph into a single vertex gadget that has one self-loop for each edge of the original base graph.
In short, super-symmetry is the main algorithmically useful property of a h.f. set, and CFI-symmetry is a clever structural recipe for building super-symmetric sets.
Informally speaking, it seems that any sensibly constructed super-symmetric object should also be CFI-symmetric: If the CFI-symmetry is dropped, the orbit-sizes just get bigger and super-symmetry seems more difficult to achieve. Actually, CFI-symmetric objects in some sense have the smallest possible “local orbit-sizes”: If $\mu \in \HF(\widehat{E})$ is CFI-symmetric, then any object $x \in \tc(\mu)$ with orbit-size $>2$ can only occur as an element of another set $y \in \tc(\mu)$, if it occurs together with a part of its orbit, such that the orbit-size is compressed down to two again. This is in a sense smallest-possible because h.f. sets which consist only of objects (or connected components) with orbit-size one are probably rather meaningless.
Therefore, for algorithms based on super-symmetric objects (which is the only paradigm we know at the moment), we speculate that CFI-symmetry is no true restriction, i.e. that the class of “super-symmetric CFI algorithms” is a subclass of the CFI-symmetric ones.

Some properties of our constructed XOR-circuits will be particularly nice when the original object is super-symmetric. In total, our circuit construction will be most powerful for objects that are super-symmetric and CFI-symmetric at the same time. As already mentioned, this holds for all objects constructed in the known algorithms.

§ TRANSLATING HEREDITARILY FINITE SETS TO XOR-CIRCUITS

An XOR-circuit is a connected directed acyclic graph $C = (V_C,E_C)$ with a unique designated root $r$. Its internal nodes are understood as XOR-gates and its leafs correspond to the input gates of the circuit. If $(g,h) \in E_C$, then the output of gate $h$ is an input of gate $g$. Every XOR-circuit computes the Boolean XOR-function over a subset of its input bits.

Such circuits are the combinatorial objects that we will use to capture the structure of the CFI-symmetric h.f. sets in $\HF(\widehat{E})$. When we consider these h.f. sets, we always view them as objects over a given CFI-structure $\GG^S$ on some base graph $G = (V,E)$. Defining them in CPT requires to preserve the symmetries of the input structure $\GG^S$, so in particular, the automorphisms $\Aut(G)$ of the base graph. This symmetry will be reflected in the symmetry of the corresponding XOR-circuit. Therefore, we have to formalise how the automorphisms of a graph $G$ act on XOR-circuits:

We say that an XOR-circuit $C$ is a circuit over a graph $G = (V,E)$, if the input gates of $C$ are labelled with the edges in $E$. More precisely, let $L \subseteq V_C$ be the leafs of $C$. There is an injective labelling function $\ell : L \lra E$ that relates the input gates with edges of $G$. To speak about the semantics of the circuit, we introduce a set of formal propositional variables $\Vv(G) := \{X_e \mid e \in E\}$. For every input gate $g \in L$, the input bit of this gate is the value of the variable $X_{\ell(g)}$.

Since every internal gate is an XOR-gate, the function computed by it is the XOR over a subset of $\Vv(G)$. For our purposes, this subset is the main interesting property of a gate, and we call it $\Xx(g)$.
Formally, if $g \in L$, then $\Xx(g) := \{\ell(g)\} \subseteq E$.
If $g$ is an internal gate, then
\Xx(g) := \bigtriangleup_{h \in gE_C} \Xx(h),
that is, the symmetric difference over the $\Xx(h)$ for all children of $g$. In other words, $\Xx(g) \subseteq E$ is precisely the set of edges in $E$ such that $g$ computes the Boolean function $\bigoplus_{e \in \Xx(g)} X_e$. The function computed by the circuit $C$ is the XOR over $\Xx(r) \subseteq E$, where $r$ is the root of $C$. An alternative way to think about this is to say that for any gate $g$, $\Xx(g)$ is the set of input bits to which the function computed by $g$ is sensitive, that is, flipping a single input bit of the circuit changes the value of $g$ if and only if the flipped edge is in $\Xx(g)$.

§.§ Symmetries of circuits

A circuit $C$ over a graph $G$ is subject to the action of the automorphism group $\Aut(G) \leq \Sym(V)$. Any $\pi \in \Aut(G)$ changes the labels of the input gates in $L$. So let $g \in L$ with $\ell(g) = e = \{u,v\} \in E$. Then $\pi(g)$ is an input gate with $\ell(\pi(g)) = \pi(e) = \{\pi(u), \pi(v)\} \in E$. This extends to subcircuits of $C$ and to $C$ itself, so $\pi(C)$ is just $C$ with the input labels modified accordingly.
We say that $\pi$ extends to an automorphism of $C$ if there exists a bijection $\sigma : V_C \lra V_{C}$ that is an automorphism of the graph $(V_C,E_C)$ and satisfies for each input gate $g \in V_C$: $\ell(\sigma(g)) = \pi(\ell(g))$. We write

\[
\Stab_G(C)  = \{ \pi \in \Aut(G) \mid \pi \text{ extends to an automorphism of } C \} \leq \Aut(G),
\]

and: $\Orb_G(C) = \{ \pi(C) \mid \pi \in \Aut(G) \}$.

Symmetric circuits have been studied as computation models capturing FPC and rank logic by Dawar together with Anderson and Wilsenach, respectively (see <cit.> and <cit.>). Our setting here is a bit different. The symmetric circuits from the literature – roughly speaking – correspond to the case where $\Aut(G) = \Sym(V)$ and $\Stab_G(C) = \Sym(V)$, so they are invariant under all possible permutations of $V$. That is also the reason why their power can be bounded in terms of fixed-point logics, which are weaker than CPT.
In contrast, the circuits we consider here need not be symmetric in the sense that every $\pi \in \Aut(G)$ induces a circuit automorphism, but rather we will be interested in circuits whose orbit size is at most polynomial in $|G|$, w.r.t. the action of $\Aut(G)$. Also, $\Aut(G)$ may in general be much smaller than $\Sym(V)$.

Other examples for symmetric circuit lower bounds concern symmetric arithmetic circuits for the permanent <cit.> and determinant <cit.>, $\AC^0$-circuits for the parity function <cit.>, and Boolean circuits for the multiplication of permutation matrices <cit.>. An interesting aspect about Rossman's lower bound for $\AC^0$-circuits computing parity is the symmetry group he considers: Contrary to the other mentioned results, the symmetry group is in this case not a large permutation group on the input variables but a Boolean vector space which acts on the set of input literals $\{X_1,\overline{X}_1,...,X_n,\overline{X}_n\}$ by swapping specified literals $X_i$ with their respective negations. Such Boolean vector spaces appear also frequently in our proof as they correspond to the CFI-flips. Unfortunately, Rossman's lower bound does not seem to have a direct bearing on our problem, though, because he shows the hardness of computing parities, whereas our circuits can achieve this with a single XOR-gate.

§.§ The parameter fan-in dimension

The XOR-circuits we will construct from CFI-symmetric h.f. sets will satisfy a certain fan-in bound on the gates. However, this bound will not be – as it is more common – on the number of incoming wires of a gate but rather, on the “linear algebraic complexity of incoming information”, so to say.
The subsets of $E$ form a Boolean vector space together with the symmetric difference operation. This space is isomorphic to $\bbF_2^E$.

With each internal gate $g$ of an XOR-circuit $C = (V_C,E_C)$, we can associate a Boolean matrix $M(g) \in \bbF_2^{gE_C \times E}$, that we call the gate matrix: The row at index $h \in gE_C$ is defined as the characteristic vector of $\Xx(h) \subseteq E$, transposed, i.e. $M(g)_{h-} = \chi(\Xx(h))^T$. Here and in what follows, we write $\chi$ for the bijection from $\Pp(E)$ to $\bbF_2^E$ that associates with each subset of $E$ its characteristic Boolean vector. If $g$ is an input gate, then we define $M(g) \in \bbF_2^{[1] \times E}$ as the one-row matrix whose only row is $\chi(\Xx(g)))^T = \chi(\{\ell(g)\})^T$.

The fan-in dimension of a gate $g$ is the dimension of the row-space of $M(g)$, or equivalently, $\rk(M(g))$.

The fan-in dimension of $g$, restricted to the space $\Aut_{\CFI}(\GG^S)$ (also called the restricted fan-in dimension) is

\[
\dim (M(g) \cdot \Aut_{\CFI}(\GG^S)) = \dim \{ M(g) \cdot \mathbf{v} \mid \mathbf{v} \in \Aut_{\CFI}(\GG^S) \}.
\]

The (restricted) fan-in dimension of the circuit $C$ is the maximum (restricted) fan-in dimension of any of the gates in $C$.

Thus, the fan-in dimension of a gate $g$ is the dimension of the subspace of $\bbF_2^E$ that is spanned by the characteristic vectors $\chi(\Xx(h)) \in \bbF_2^E$, for all children $h$ of $g$. One interpretation of $\rk(M(g))$ is that it tells us how many different patterns of incoming bits can occur at gate $g$: When we consider all $2^{|E|}$ possible inputs of the circuit, the number of distinct binary strings in $\{0,1\}^{gE_C}$ that can arise as the values of the children of $g$ is $2^{\rk(M(g))}$.

Sometimes we will also need the restricted fan-in dimension.
This describes how many different input patterns of the gate can occur if we only allow circuit input vectors $\mathbf{x} \in \bbF_2^E$ where the $1$-entries in $\mathbf{x}$ form a set of cycles in the base graph $G$ (i.e. input vectors from $\Aut_{\CFI}(\GG^S)$).

These notions of fan-in dimension are unusual circuit parameters but as we will show, they nicely capture the orbit size of the original h.f. set with respect to the groups of edge flips $\Aut_{\CFI}(\GG)$ and $\Aut_{\CFI}(\GG^S)$. In total, the benefit of the circuit-representation of h.f. objects over CFI-graphs is that this simplifies the effect of the complicated automorphism group $\Aut(\GG^S) \leq \Aut_{\CFI}(\GG) \rtimes \Aut(G)$: In order to show that the CFI-query is not in CPT, we would ultimately like to prove that certain h.f. sets necessarily have super-polynomial orbits w.r.t. $\Aut(\GG^S)$. By translating these objects into circuits, we can express the restrictions imposed by $\Aut_{\CFI}(\GG)$ in terms of fan-in dimension, and are left with the task of analysing the orbit size w.r.t. $\Aut(G)$.

§.§ The circuit construction

The following theorem is the core of the proof of Theorem <ref>. We will prove it first and then explain in the next section which further steps are needed to conclude Theorem <ref> from it.

Fix a family $(G_n)_{n \in \bbN}$ of base graphs.
For every $n \in \bbN$, let $\GG_n^S$ be a CFI-graph over $G_n = (V_n,E_n)$ and let $\mu_n \in \HF(\widehat{E}_n)$ be a CFI-symmetric h.f. set that is $\CPT$-definable on input $\GG^S_n$ (by the same $\CPT$-program for the whole family of graphs). Then for every $n \in \bbN$, there exists an XOR-circuit $C(\mu_n) = (V_C, E_C)$ over $G_n$ which satisfies:

* The size of the circuit, i.e. $|V_C|$, is polynomial in $|\GG^S_n|$.

* The orbit-size $|\Orb_G(C(\mu_n))|$ of the circuit is polynomial in $|\GG^S_n|$.

* $C(\mu_n)$ is sensitive to an edge $e \in E_n$ if and only if $e \in \sup_{\CFI}(\mu_n)$.

* The fan-in dimension of $C(\mu)$ is $\Oo(\log(\maxOrb_E(\mu)))$. The fan-in dimension restricted to the space $\Aut_{\CFI}(\GG_n^S)$ is $\Oo(\log(\maxOrb_\CFI(\mu)))$.

We now provide the construction of the circuit and prove several lemmas from which it follows that the circuit has the desired properties.
We fix $\mu \in \HF(\widehat{E})$ and denote by $C(\mu) = (V_C,E_C)$ the corresponding XOR-circuit that we are going to define. The gates of the circuit are the $\sim_E$-equivalence classes of the objects in $\tc(\mu)$. Recall that $\sim_E$-equivalence is the same-orbit-relation with respect to the edge-flips $\Aut_{\CFI}(\GG)$. Whenever we write $[x]$ for an $x \in \tc(\mu)$, we formally mean $[x] = \{ \rho_F(x) \mid \rho_F \in \Aut_{\CFI}(\GG) \text{ such that } \rho_F(x) \in \tc(\mu)  \}$. The circuit $C(\mu)$ is defined as follows:

* $V_C := \tc(\mu)_{\sim_E} =  \{ [x] \mid x \in \tc(\mu)  \}$.

* $E_C := \{ ([x], [y]) \mid \text{there exists } y' \in [y] \text{ such that } y' \in x  \}$.

* By definition, the leafs of $C(\mu)$ correspond to $\sim_E$-classes of atoms in $\tc(\mu)$. The set of atoms is $\widehat{E}$, so any leaf of $C$ has the form $[e_0]$, for some $e \in E$. We let $\ell([e_0]) := e$.

* The root $r$ of $C(\mu)$ is $[\mu]$.

In other words, the circuit is just the DAG $(\tc(\mu),\in)$, with the $\sim_E$-equivalence factored out.

First of all, we have to check that the set of edges $E_C$ can indeed be defined in this way, i.e. that whether or not there is an $E_C$-edge between $[x]$ and $[y]$ is independent of the choice of the representative of $[x]$ in the definition. In the following lemma, let $\in^\mu$ denote the element relation on $\tc(\mu)$ within the h.f. set $\mu$.

Let $[x], [y] \subseteq \tc(\mu)$ be two $\sim_E$ classes. If there exists $y' \in [y]$ such that $y' \in^{\mu} x$, then for every $x' \in [x]$ there is a $y' \in [y]$ such that $y' \in^{\mu} x'$.

Let $y' \in [y]$ such that $y' \in^{\mu} x$. Now let $x' \in [x]$ be arbitrary, and let $\rho_F \in \Aut_{\CFI}(\GG)$ be such that $\rho_F(x) = x'$. Then $\rho_F(y') \in^\mu \rho_F(x)$  because the operation is applied element-wise. The set $\rho_F(x) \in [x]$ is an element of $\tc(\mu)$ because $[x]$ denotes the $\sim$-class inside $\tc(\mu)$.
Therefore, we also have $\rho_F(y') \in \tc(\mu)$, and thus $\rho_F(y') \in [y]$. This proves the lemma.

Property 2 from Theorem <ref> states that the $\Aut(G)$-orbit of $C(\mu)$ is sufficiently small. We prove this by showing that this orbit cannot be larger than the $\Aut(G)$-orbit of the h.f. set $\mu$; and for $\mu$, we know that its orbit is polynomial in $|\GG^S|$, because it is CPT-definable by the assumptions of Theorem <ref>.

Every $\pi \in \Stab_G(\mu) \leq \Sym(V)$ extends to an automorphism of the circuit $C(\mu)$, that is:
$\Stab_G(\mu) \leq \Stab_G(C(\mu))$.

Let $\pi \in \Stab_G(\mu) \leq \Aut(G)$. That is, $\pi$ extends to an automorphism $\sigma : \tc(\mu) \lra \tc(\mu)$ of teh DAG $(\tc(\mu),\in^\mu)$. We define $\sigma' : V_C \lra V_C$ by letting $\sigma'([x]) = [\sigma(x)]$. This is well-defined because $x \sim_E x'$ if and only if $\sigma(x) \sim_E \sigma(x')$ ($\sigma$ is an automorphism of $\mu$). Now we check that $\sigma'$ is an automorphism of $C(\mu)$ induced by $\pi$.

Clearly, $\sigma'$ is a bijection on $V_C$, i.e. on the set of $\sim_E$-classes of $\tc(\mu)$: It is surjective because $\sigma$ is, and then it is already a bijection because it maps $V_C$ to $V_C$.  Let $[e_0] \in V_C$ be an input gate. Then $\ell([e_0]) = e$. We have $\sigma(e_0) = \pi(e)_0$. So $\sigma'([e_0]) = [\pi(e)_0]$. Hence, $\ell(\sigma'([e_0])) = \pi(\ell([e_0]))$, as desired.

Now let $([x],[y]) \in E_C$. Then there exists a $y' \in [y]$ such that $y' \in^\mu x$. Then because $\sigma$ is an automorphism, it also holds $\sigma(y') \in^\mu \sigma(x)$. Therefore, $([\sigma(x)], [\sigma(y')]) \in E_C$. It holds $([\sigma(x)], [\sigma(y')]) =  (\sigma'[x], \sigma'[y']) = (\sigma'[x], \sigma'[y])$, so $(\sigma'[x], \sigma'[y]) \in E_C$.
In total, this means that $\pi \in \Aut(G)$ extends to the automorphism $\sigma'$ of the circuit $C(\mu)$.

$|\Orb_G(C(\mu))| \leq |\Orb_G(\mu)|.$

Follows from Lemma <ref> together with the Orbit-Stabiliser Theorem, which says that $|\Orb_G(C(\mu))| = | \Aut(G)  | / |\Stab_G(C(\mu))|$ and $|\Orb_G(\mu)| = | \Aut(G)  | / |\Stab_G(\mu)|$.

Next, we would like to analyse the fan-in dimension of $C(\mu)$, and the connection between $C(\mu)$ and $\sup_{\CFI}(\mu)$. The key for this is to establish a connection between the stabilisers $\Stab_E(x)$, for all $x \in \tc(\mu)$, and the kernels of the corresponding gate matrices. For the definition of these matrices, we refer back to Section <ref>.
We start with the following observation that relates the stabilisers of objects in $\tc(\mu)$ with the stabilisers of their elements.

For each $x \in \tc(\mu)$, it holds
\Stab_E(x) = \bigcap_{y \in x}  \Stab_E( [y] \cap x  ) =  \bigcap_{\gamma \in \Cc(x)} \Stab_E(\gamma).

This is true simply because $x$ is stabilised by $\rho_F \in \Aut_{\CFI}(\GG)$ iff every $\Aut_{\CFI}(\GG)$-orbit within $x$ is fixed setwise by $\rho_F$.

For every gate $[x] \in V_C$, and its gate matrix $M[x] \in \bbF_2^{[x]E_C \times E}$, it holds:

\[
\Ker(M[x]) = \Stab_E(x) = \Stab_E(x') \text{ for every } x' \in [x].
\]

For every row $M[x]_{[y]-}$, for $[y]\in[x]E_C$, it holds:

\[
\Ker(M[x]_{[y]-}) = \Stab_E([y] \cap x) \tag{$\star$}
\]

It holds $\Stab_E(x) = \Stab_E(x')$, for every $x' \in [x]$ and also $\Stab_E([y] \cap x) = \Stab_E([y] \cap x')$, for every $x' \in [x]$ (by Lemma <ref>).
Therefore, ($\star$) does not depend on the choice of representatives.
From ($\star$) it immediately follows that $\Ker(M[x]) = \Stab_E(x)$, due to Proposition <ref> and the fact that $\Ker(M[x])$ is the intersection over the kernels of the rows of $M[x]$.
We now prove ($\star$) via induction from the input gates to the root. If $[x] = [e_0]$ is an input gate, then $M[x]$ has just one row, which is $\chi(e)^T$. The kernel of $\chi(e)^T$ is the set of all vectors in $\bbF_2^E$ which are zero at index $e$. This is precisely $\Stab_E(e_0) = \Stab_E(e_1)$, as desired.
Now suppose $[x]$ is an internal gate, i.e. $x$ is a non-atomic h.f. set in $\tc(\mu)$. Each row of $M[x] \in \bbF_2^{[x]E_C \times E}$ is the characteristic vector of $\Xx[y] \subseteq E$, for a $[y] \in [x]E_C$. We have

\[
\Xx[y] = \bigtriangleup_{[w] \in [y]E_C} \Xx[w].
\]

In matrix-vector notation, we can write this as:

\[
M[x]_{[y]-} = \chi(\Xx[y])^T = \sum_{[w] \in [y]E_C} (M[y]_{[w]-})^T = (1 \ 1 \ ... \ 1) \cdot M[y].
\]

Let $\gamma \in \Cc(x)$ be the connected component such that $\gamma = [y] \cap x$. The equation above means that	$\Ker(M[x]_{[y]-}) = \mathcal{E}_y$, where $\mathcal{E}_y$ denotes the set of all vectors in $\bbF_2^E$ whose image under $M[y]$ has even Hamming weight. Thus we have to show that $\mathcal{E}_y = \Stab_E(\gamma)$.
Each row $M[y]_{[w]-}$ corresponds to a connected component $\gamma' \in \Cc(y)$ with $w \in \gamma'$.

By the induction hypothesis, we have for each row $M[y]_{[w]-}$ and each $\mathbf{v} \in \bbF_2^E$ that $M[y]_{[w]-} \cdot \mathbf{v} = 1$ iff $\mathbf{v} \notin \Stab_E([w] \cap y)$. So $M[y] \cdot \mathbf{v}$ has even Hamming weight iff $\rho_{\chi^{-1}(\mathbf{v})} \in \Aut_{\CFI}(\GG)$ flips an even number of connected components of $y$. This is true iff $\rho_{\chi^{-1}(\mathbf{v})}$ flips an even number of components in every $y' \in \gamma$ (due to Lemma <ref>). By definition of CFI-symmetry (Definition <ref>), this is the case iff $\mathbf{v} \in \Stab_E(\gamma)$, because $\mu$ is CFI-symmetric, and thus, $\gamma$ is a CFI-symmetric component. In total, we have shown that $\mathbf{v} \in \Ee_y$ iff $\mathbf{v} \in\Stab_E(\gamma)$. This proves ($\star$) for every row of $M[x]$.

As a consequence of this correspondence between kernels and stabilisers, we can bound the fan-in dimension of $C(\mu)$. This proves Property 4 from Theorem <ref>.

The fan-in dimension of $C(\mu)$ is $\log (\maxOrb_E(\mu))$.

Let $x \in \tc(\mu)$. From the Orbit-Stabiliser Theorem and the fact that $|\Aut_{\CFI}(\GG)| = 2^{|E|}$, it follows that

\[
\Orb_E(x) = \frac{2^{|E|}}{|\Stab_E(x)|} \leq \maxOrb_E(\mu).
\]

This means that
\log (\maxOrb_E(\mu)) \geq |E| - \dim \ \Stab_E(x).
By Lemma <ref>, $\Stab_E(x) = \Ker(M[x])$.

With the Rank Theorem we get:
\rk(M[x]) = |E| - \dim \ \Stab_E(x) \leq \log (\maxOrb_E(\mu)).
Since there is an object $x \in \tc(\mu)$ where $\maxOrb_E(\mu)$ is attained,  $\rk(M[x]) =\\ \log (\maxOrb_E(\mu))$ is indeed the maximum rank of any gate matrix of $C(\mu)$.

The fan-in dimension of $C(\mu)$ with respect to the space $\Aut_{\CFI}(\GG^S)$ is $\log (\maxOrb_{\CFI}(\mu))$. That is, for every gate $[x]$ in $C(\mu)$, we have

\[
\dim(M[x] \cdot \Aut_{\CFI}(\GG^S)) \leq \log (\maxOrb_{\CFI}(\mu)).
\]

Let $x \in \tc(\mu)$. With the Orbit-Stabiliser Theorem we get

\[
\Orb_\CFI(x) = \frac{| \Aut_{\CFI}(\GG^S) |}{|\Stab_\CFI(x)|} = 2^{\dim  \Aut_{\CFI}(\GG^S) - \dim \Stab_\CFI(x)} \leq \maxOrb_\CFI(\mu).
\]

\[
\log \maxOrb_\CFI(\mu) \geq \dim \Aut_{\CFI}(\GG^S) - \dim \Stab_\CFI(x).
\]

Using Lemma <ref>, we get $\Stab_\CFI(x) \subseteq \Stab_E(x) \subseteq \Ker(M[x])$. Therefore,

\[
\dim (M[x] \cdot \Aut_{\CFI}(\GG^S)) \leq \dim \Aut_{\CFI}(\GG^S) - \dim \Stab_\CFI(x) \leq \log \maxOrb_\CFI(\mu).
\]

First of all, since $\mu$ is by assumption CPT-definable in the structure $\GG^S$, the size $|\tc(\mu)|$ and the orbit $|\Orb_{\Aut(\GG^S)}(\mu)|$ are polynomial in $|\GG^S|$. Therefore, Property 1 from Theorem <ref> clearly holds for $C(\mu)$, because $|V_C| \leq |\tc(\mu)|$. Property 2 follows from the bound on $|\Orb_{\Aut(\GG^S)}(\mu)|$ together with Corollary <ref>, and the fact that $| \Orb_G(\mu)  | \leq |\Orb_{\Aut(\GG^S)}(\mu)|$.

Property 4  is proven in Lemmas <ref> and <ref>.

Finally, Property 3 can be seen as follows: Suppose $C(\mu)$ is sensitive to an edge $e \in E$. This means that $e \in \Xx(r)$, for the root $r = [\mu]$ of $C(\mu)$. This is the case iff $e \in \Xx([y])$ for an odd number of children $[y] \in [\mu]E_C$. This is the same as saying that the column $M[\mu]_{-e}$ has odd Hamming weight. By equation ($\star$) from Lemma <ref>, this holds if and only if $\chi(e) \notin \Stab_E([y] \cap x)$ for an odd number of children $[y] \in [\mu]E_C$. Since $\mu$ is CFI-symmetric, by Definition <ref> this is the case if and only if $\rho_e(\mu) \neq \mu$. And this holds iff $e \in \sup_{\CFI}(\mu)$ (because $\sup_{\CFI}(\mu)$ is the smallest possible CFI-support of $\mu$).

§.§ Proving the main theorem

So far, we have a translation of CFI-symmetric h.f. sets in $\HF(\widehat{E})$ into XOR-circuits with the properties mentioned in Theorem <ref>. What is missing in order to conclude Theorem <ref> from this is to prove that any CPT-algorithm which is both super-symmetric and CFI-symmetric and decides the CFI-query must construct a h.f. set whose properties translate into the circuit properties from Theorem <ref>. Fortunately, a result to this effect exists already. The following support lower bound for general CPT-programs deciding the CFI-query is due to Dawar, Richerby, and Rossman <cit.>.

Let $(G_n)_{n \in \bbN}$ be a family of base graphs and let $\tw_n$ denote the treewidth of $G_n$. Let $\GG_n^S, \GG_n^{S'}$ denote two non-isomorphic CFI-structures over $G_n$. Let $f(n) \leq \tw_n$ be a function such that $\GG_n^{S}$ and $\GG_n^{S'}$ are $\Cc^{\tw_n}$-homogeneous for all tuples of length $\leq 2f(n)$.

Then any $\CPT$-program that distinguishes $\GG_n^S$ and $\GG_n^{S'}$ for all $n \in \bbN$ must activate on input $\GG_n^S$ a h.f. set $x$ whose smallest support has size at least $\Omega(f(n))$.

A structure $\GG^S_n$ is $\Cc^{\tw_n}$-homogeneous if whenever two tuples $\bar{a}$ and $\bar{b}$ have the same $\Cc^{\tw_n}$-type in $\GG^S_n$, then there is an automorphism of $\GG^S_n$ that maps $\bar{a}$ to $\bar{b}$. The $\Cc^{\tw_n}$-type of a tuple $\bar{a}$ in $\GG^S_n$ is the collection of all $\Cc^{\tw_n}$-formulas that are true in $(\GG^S_n,\bar{a})$. By closer inspection of the entire proof in <cit.>, one can see that homogeneity is actually only required in the weaker sense that for all tuples of some bounded length, the $\Cc^{\tw_n}$-type partition coincides with the orbit partition – hence the explicit restriction in the above theorem.

The homogeneity condition is satisfied by certain ordered CFI-graphs, as stated in <cit.> and proved in <cit.>, and as we will show, the unordered CFI-graphs over hypercubes, which we use for the lower bound in Theorem <ref>, satisfy it as well. Therefore, the homogeneity condition is not really a restriction in the cases that are of interest for us, which is why we omitted it in Theorem <ref>. What we also omitted is the fact that we have to relate two different notions of support. Theorem <ref> refers to the minimum CFI-support of the h.f. sets, whereas the support lower bound above refers to the minimum $\Aut(\GG^S)$-support. Therefore, in order to formulate Theorem <ref> correctly with all details, we have to speak about the ratio between these two supports.

Let $G = (V,E)$ be a base graph and $\GG^S$ a CFI-graph over it. Let $\mu \in \HF(\widehat{E})$. Denote by $s(\mu)$ the size of the smallest $\Aut(\GG^S)$-support of $\mu$ (while $\sup_{\CFI}(\mu)$ still denotes the smallest CFI-support).

Then we call the ratio

\[
\alpha(\mu) = \frac{s(\mu)}{|\sup_{\CFI}(\mu)|}
\]

the CFI-support gap of $\mu$ (with respect to $\GG^S$).

Then the detailed version of Theorem <ref> reads as follows:

Let $(G_n = (V_n,E_n))_{n \in \bbN}$ be a sequence of base graphs. Let $\GG^S_n$ be a CFI-graph over $G_n$, let $\tw_n$ denote the treewidth of $G_n$. Let $f(n) \in \Oo(\tw_n)$ be a function such that every $\GG^S_n$ is $\Cc^{\tw_n}$-homogeneous, for all tuples of length $\leq 2f(n)$.
Let $g(n)$ be a function such that the CFI-support-gap for every $\mu \in \HF(\widehat{E}_n)$ with minimum support $s(\mu) \in \Omega(f(n))$ is bounded by $g(n)$.

If there exists a CFI-symmetric $\CPT$-program $\Pi$ that decides the CFI-query on all $\GG_n^S$, then for every $G_n = (V_n,E_n)$, there exists an XOR-circuit $C_n$ over $G_n$ that satisfies the following “instantiated properties” from Theorem <ref>:

* The number of gates in $C_n$ is polynomial in $|\GG^S_n|$.

* The orbit-size $|\Orb_{G_n}(C_n)|$ of the circuit is polynomial in $|\GG^S_n|$.

* $C_n$ is sensitive to $\Omega(f(n)/g(n))$ many edges in $E_n$.

* The fan-in dimension of $C_n$, restricted to the space $\Aut_{\CFI}(\GG_n^S)$, is $\Oo(\log |\GG_n^S|)$.

* If the program $\Pi$ is super-symmetric in addition to being CFI-symmetric, or if the base graph $G_n$ decomposes into at most $\Oo(\sqrt{\log |\GG^S|})$ many components when any $f(n)/g(n)$ many edges are removed, then also the (unrestricted) fan-in dimension of $C_n$ is $\Oo(\log |\GG_n^S|)$.

Assume such a CPT-program $\Pi$ exists. Let $\mu_n \in \HF(\widehat{E}_n)$ denote the CFI-symmetric h.f. set with large support that $\Pi$ activates on input $\GG^S_n$. Then by Theorem <ref>, the smallest $\Aut(\GG^S_n)$-support of the object $\mu_n$ has size $\Omega(f(n))$. Since the CFI-support gap of $\mu_n$ in $\GG^S_n$ is at most $g(n)$, the size of the smallest CFI-support of $\mu_n$ is at least: $\sup_{\CFI}(\mu_n) \in \Omega(f(n)/g(n))$. Theorem <ref> applied to $\mu_n$ yields the XOR-circuit $C_n$. Property 3 from Theorem <ref> in combination with the bound $\sup_{\CFI}(\mu_n) \in \Omega(f(n)/g(n))$ means that $C_n$ is sensitive to $\Omega(f(n)/g(n))$ many edges in $E_n$.
Property 4 from Theorem <ref> bounds the fan-in dimension and the restricted fan-in dimension in terms of $\log(\maxOrb_E(\mu_n))$ and $\log(\maxOrb_\CFI((\mu_n))$, respectively. Lemma <ref> states that $\maxOrb_E(\mu_n) \leq |\Orb_E(\mu_n)| \cdot | \tc(\mu_n)|$ and $\maxOrb_\CFI(\mu_n) \leq |\Orb_\CFI(\mu_n)| \cdot | \tc(\mu_n)|$. Because $\mu_n$ is defined by the CPT-program $\Pi$ on input $\GG^S_n$, both $|\tc(\mu_n)|$ and $|\Orb_{\CFI}(\mu_n)|$ are polynomially bounded in $|\GG_n^S|$ (the orbit is bounded because $\Aut_{\CFI}(\GG^S)$ is a subgroup of $\Aut(\GG^S_n)$). This yields a polynomial bound on $\maxOrb_\CFI(\mu_n)$. Together with the $\log(\maxOrb_\CFI((\mu_n))$-bound on the restricted fan-in dimension, this gives us Property 4 from this theorem.

Property 5 follows then with Lemma <ref> if $\Pi$ is super-symmetric, and with Corollary <ref> in case that the base graph $G_n$ splits into a bounded number of components when $\sup_{\CFI}(\mu_n)$ is removed from it.

§ XOR-CIRCUITS FOR MORE GENERAL HEREDITARILY FINITE SETS

So far, we have shown that CFI-symmetric h.f. sets over CFI-structures $\GG^S$ can be quite easily transformed into XOR-circuits by factoring out the orbits under the edge-flip-group $\Aut_{\CFI}(\GG)$. Importantly, this construction automatically translates the relevant properties of the h.f. set, such as support size and symmetry, into more or less natural circuit-properties. As a consequence, we can – in principle – limit the power of CFI-symmetric algorithms for the CFI-query by proving appropriate lower bounds for certain families of polynomial size symmetric XOR-circuits. Even though all currently known choiceless algorithms for the CFI-query are CFI-symmetric, and it is not clear that non-CFI-symmetric algorithms are really more powerful, it would be much nicer if the circuit-translation were so general that it could be used to separate all of CPT from P, and not only the CFI-symmetric algorithms. In this subsection we explore to what extent the circuit construction can be generalised in that direction. We will present a modification of the construction above, that uses additional gadgets, works without the restriction to CFI-symmetric sets, and has almost all properties from Theorem <ref>. By “almost all” we mean that the additional gadgets we have to introduce in the circuit are of unknown size. Hence, we cannot be sure that the constructed circuit is always of polynomial size. However, we can formulate a condition on the h.f. sets, which generalises that of CFI-symmetry and guarantees polynomial size of the circuit. This condition concerns Boolean vector spaces with a permutation group acting on the index set. If certain subspaces of $\bbF_2^E$, which appear as stabiliser groups of the connected components of the sets in $\mu$ possess a basis that is (almost) invariant under the permutation group (which will be a subgroup of $\Aut(G)$), then the circuit constructed from $\mu$ has polynomial size. Here is the result of this section:

Fix a family $(G_n)_{n \in \bbN}$ of base graphs.
For every $n \in \bbN$, let $\GG_n^S$ be a CFI-graph over $G_n = (V_n,E_n)$ and let $\mu_n \in \HF(\widehat{E}_n)$ be a h.f. set that is $\CPT$-definable on input $\GG^S_n$ (by the same $\CPT$-program for the whole family of graphs). Then for every $n \in \bbN$ there exists an XOR-circuit $\widehat{C}(\mu_n) = (V_C, E_C)$ over the edges of $G_n$ which satisfies:

* The orbit-size $|\Orb_G(\widehat{C}(\mu_n))|$ of the circuit is polynomial in $|\GG^S_n|$.

* $\widehat{C}(\mu_n)$ is sensitive to at least $\frac{|\sup_{\CFI}(\mu)|}{\log(\maxOrb_E(\mu))}$ many edges in $E$.

* The fan-in dimension of $\widehat{C}(\mu)$ is $\Oo(\log(\maxOrb_E(\mu)))$.

* If for every $x,y \in \tc(\mu)$ such that $[y] \cap x \neq \emptyset$, the space $\Stab_E([y] \cap x)$ has a symmetric basis (see Definition <ref>), then the size $|V_C|$ is polynomial in $|\GG^S|$.

This theorem differs from Theorem <ref> for CFI-symmetric objects in two aspects. Firstly, the circuit $\widehat{C}(\mu)$ is not necessarily sensitive to all edges in $\sup_{\CFI}(\mu)$ but only to a logarithmic fraction of them. Secondly, we have no guarantees for the size of the circuit unless all spaces $\Stab_E([y] \cap x)$ admit a symmetric basis; we will introduce this concept formally in Section <ref>. It should be noted that this fourth property mentioned in the theorem is – as far as we know – not an “if and only if”. It may be that $\widehat{C}(\mu)$ has polynomial size even when the symmetric basis condition is not satisfied for $\mu$.

As a consequence, we have the following version of Theorem <ref> for non-CFI-symmetric CPT-programs that decide the CFI-query. The condition that the h.f. set with large support which is used to decide the CFI-query is CFI-symmetric is weakened to the symmetric-basis condition.
As we show later, in Lemma <ref>, every CFI-symmetric set also has a symmetric basis, and there are as well simple examples of non-CFI-symmetric sets with a symmetric basis (see Example <ref>). Thus, the symmetric basis condition is indeed a strict generalisation of CFI-symmetry.

Let $(G_n = (V_n,E_n))_{n \in \bbN}$ be a sequence of base graphs. Let $\GG^S_n$ be a CFI-graph over $G_n$, let $\tw_n$ denote the treewidth of $G_n$, and let $f(n) \leq \tw_n$ be a function such that $\GG^S_n$ is $\Cc^{\tw_n}$-homogeneous for all tuples of length $\leq 2f(n)$.

Let $g(n)$ be a function such that the CFI-support-gap for every $\mu \in \HF(\widehat{E}_n)$ with minimum support $s(\mu) \in \Omega(f(n))$ is bounded by $g(n)$.

Let $\Pi$ be a $\CPT$-program that decides the CFI-query on all $\GG_n^S$ using a h.f. set $\mu_n \in \GG_n^S$ with sufficient support such that $\Stab_E([y] \cap x)$ has a symmetric basis according to Definition <ref>, for all $x,y \in \tc(\mu_n)$ with $[y] \cap x \neq \emptyset$.

Assume additionally that $\Pi$ is super-symmetric or that the base graph $G_n$ decomposes into at most $\Oo(\sqrt{\log |\GG^S|})$ many components when any $f(n)/g(n)$ many edges are removed.

Then for every $n \in \bbN$ there exists an XOR-circuit $C_n$ over $G_n$ that satisfies the following “instantiated properties” from Theorem <ref>:

* The number of gates in $C_n$ is polynomial in $|\GG^S_n|$.

* The orbit-size $|\Orb_{G_n}(C_n)|$ of the circuit is polynomial in $|\GG^S_n|$.

* $C_n$ is sensitive to $\Omega(f(n)/(g(n) \cdot \log | \GG_n^S|))$ many edges in $E_n$.

* The fan-in dimension of $C_n$ is $\Oo(\log |\GG_n^S|)$.

We omit the proof of this theorem because it follows from Theorem <ref> in the same way as Theorem <ref> follows from Theorem <ref>.

Now let us start with the proof of Theorem <ref>, which spans the rest of the section. It should be noted that Theorem <ref> is actually a special case of this, so we could have omitted the circuit construction for CFI-symmetric objects; however, the more general construction that we present now is not as natural as the one for CFI-symmetric objects and much harder to describe.

Fix again a base graph $G = (V,E)$, a CFI-graph $\GG^S$ over it, and an object $\mu \in \HF(\widehat{E})$. This time, $\mu$ need not be CFI-symmetric. In the previous subsection, we wrote $C(\mu)$ for the circuit obtained by factoring out the $\sim_E$ classes in $\tc(\mu)$. Now, we denote the constructed circuit by $\widehat{C}(\mu)$. Before we explain the construction, let us look at why $C(\mu)$ is not “the circuit we want” if $\mu$ is not CFI-symmetric. The only place where CFI-symmetry was required in the previous subsection is in the proof of Lemma <ref>, which relates the kernels of the gate matrices with the vector spaces $\Stab_E(x)$. This relationship is crucial because it leads to the connection between $\sup_{\CFI}(\mu)$ and the sensitivity of $C(\mu)$ to its input bits, and is also necessary to get a bound on the fan-in dimension of $C(\mu)$. Without such a bound, the construction would not be interesting because without fan-in restrictions, there always exist small symmetric XOR-circuits. Hence, we would like to ensure that the statement of Lemma <ref> still holds for $\widehat{C}(\mu)$, even if $\mu$ is not CFI-symmetric. Now take a look at the inductive proof of Lemma <ref> again. The key in this induction is that for any gate matrix $M[x]$ and any child $[y]$ of $[x]$, the row $M[x]_{[y]-}$ can be written as the product of another matrix and the child-gate-matrix $M[y]$: $M[x]_{[y]-} = (1 \ 1 \ ... \ 1) \cdot M[y]$. This equation holds because of the CFI-symmetry of $\mu$. Now in the general case, a similar equation will hold, namely: $M[x]_{[y]-} = N \cdot M[y]$, for some matrix $N$ that has to be chosen depending on $\Stab_E([y] \cap x)$. So our plan for this section is as follows: We will first of all define these $N$-matrices, that essentially “repair” the proof of Lemma <ref> in the non-CFI-symmetric case. Based on these matrices and on $C(\mu)$, we will construct $\widehat{C}(\mu)$ by introducing gadgets that simulate the effect of the chosen $N$-matrices. Then this circuit will be exactly such that the proof of Lemma <ref> goes through again, even if $\mu$ is not CFI-symmetric. In a sense, we can view the gadgets as corrections for local violations of CFI-symmetry.

§.§ Definition of the matrices

Actually, we will not only define the said $N$-matrices, but also, for every $[x] \in \{ [x] \mid x \in \tc(\mu)\}$, a Boolean matrix $M[x]$. We keep the notation $M[x]$ from the previous subsection, even though, strictly speaking, $M[x]$ will not be the gate matrix of any gate in $\widehat{C}(\mu)$; rather, it will be a matrix that satisfies $\Ker(M[x]) = \Stab_E(x)$, and it will serve as a kind of construction specification for a gadget in $\widehat{C}(\mu)$. The $M[x]$-matrices that we are going to define depend on the $M$- and $N$-matrices of the connected components of $x$ in the object $\mu$. Therefore, the construction of these matrices proceeds inductively from the atoms of $\mu$ to the more deeply nested sets. At this point, our main objective is to build the matrices in such a way that their kernels correspond to the stabiliser spaces of the sets they belong to. Furthermore, the matrices should satisfy certain symmetry requirements with respect to the action of $\Stab_G(\mu) \leq \Aut(G)$. Only after the construction of the matrices, we will use them to construct the circuit $\widehat{C}(\mu)$ in such a way that the gate matrices of $\widehat{C}(\mu)$ are as desired. So the procedure in this subsection is the other way round as in the previous one, where the circuit came first, and we then analysed its gate matrices. Now we are specifying the matrices first, and then build the circuit so that the statement of Lemma <ref> holds for $\widehat{C}(\mu)$ by construction.
Along with the matrices, we will provide certain group homomorphisms that ensure symmetry.
To speak about symmetry of matrices, we introduce notation to express the effect of row- and column-permutations:

Let $M \in \bbF_2^{I \times J}$ be any Boolean matrix, and $\sigma : I \lra I', \pi : J \lra J'$ be bijections. Then $(\sigma,\pi)(M) \in \bbF_2^{I' \times J'}$ is the matrix with $(\sigma,\pi)(M)_{\sigma i, \pi j} = M_{i,j}$ for each $(i,j) \in I \times J$. In particular, if $\sigma \in \Sym(I), \pi \in \Sym(J)$, then $(\sigma,\pi)(M)$ is the matrix that arises from $M$ when the respective row- and column-permutations are applied.

Let $\mathbf{v}, \mathbf{w} \in \bbF_2^I$ be two Boolean vectors and $\pi \in \Sym(I)$ a permutation of its entries. Then

\[
\mathbf{v}^T \cdot \mathbf{w} = \pi(\mathbf{v}^T) \cdot \pi(\mathbf{w}).
\]

Therefore, if $M \in \bbF_2^{I \times J}$ is a matrix and $\mathbf{w} \in \bbF_2^J$ is a vector, then

\[
\sigma(M \cdot \mathbf{w}) = (\sigma, \pi)M \cdot \pi(\mathbf{w}),
\]

for every $\sigma \in \Sym(I), \pi \in \Sym(J)$.

This proposition follows immediately from the definition of the scalar product of vectors because $\mathbf{v}^T \cdot \mathbf{w}$ and $\pi(\mathbf{v}^T) \cdot \pi(\mathbf{w})$ are the same sum of products, just summed in a different order. The statement about matrix-vector-multiplication then follows because this is just the scalar product of every row vector with $\mathbf{w}$. The proposition will sometimes be used without explicit reference in this section.

In the rest of this section, we will often speak about the following orbits and stabilisers. They differ from the ones from the previous section in so far as they concern the subgroup $\Stab_G(\mu) \leq \Aut(G)$, instead of $\Aut(G)$ itself. Thus, we override the notation from the previous section. Let $x \in \tc(\mu)$.

\begin{align*}
\Orb_G([x]) &:= \{ \pi([x]) \mid \pi \in \Stab_G(\mu) \leq \Aut(G) \}.\\
\Stab_G([x]) &:= \{ \pi \in \Stab_G(\mu) \mid \pi([x]) = [x]   \}.
\end{align*}

Similarly, for $x,y \in \tc(\mu)$, $\Stab_G([y] \cap x)$ refers to the stabiliser of the set $[y] \cap x$ in the group $\Stab_G(\mu)$.

Any orbit of a $\sim$-class is a set of $\sim$-equivalence classes:

For any $\sim_E$-class $[x] \subseteq \tc(\mu)$, and any $\pi \in \Stab_G(\mu)$, $\pi([x])$ is also a $\sim_E$-class of $\tc(\mu)$.

It is not hard to check that for any $\pi \in \Aut(G)$, and any $\rho_F \in \Aut_{\CFI}(\GG)$ it holds $\rho_{\pi F} = \pi \circ \rho_F \circ \pi^{-1}$.
Let $x',x'' \in [x]$ and let $\rho_F \in \Aut_{\CFI}(\GG)$ be such that $\rho_F(x') = x''$.  Then $\rho_{\pi F}(\pi x') = \pi x''$ by the above equation. Thus, $\pi(x') \sim_E \pi(x'')$. Similarly one can show that if $x' \not\sim_E x''$, then $\pi(x') \not\sim_E \pi(x'')$. Therefore, $\pi([x])$ is again a $\sim_E$-class. The fact that $\pi([x]) \subseteq \tc(\mu)$ follows because $\pi$ extends to an automorphism of the h.f. set $\mu$.

Let $x,y \in \tc(\mu)$ such that $[y] \cap x \neq \emptyset$. Then

\[
\Stab_G([y] \cap x) \leq \Stab_G([y]).
\]

The group $\Stab_G([y] \cap x)$ maps the set $[y] \cap x \subseteq [y]$ to itself, so it does not move this subset of the $\sim$-class $[y]$ into another $\sim$-class. Then by Lemma <ref>, it must map the whole class $[y]$ to itself because the image of $[y]$ must again be a $\sim$-class.

For any $x,x',y \in \tc(\mu)$ such that $x \sim_E x'$ and $[y] \cap x \neq \emptyset$, it holds

\[
\Stab_E([y] \cap x) = \Stab_E([y] \cap x').
\]

The sets $[y] \cap x$ and $[y] \cap x'$ are related via an automorphism in $\Aut_{\CFI}(\GG)$. Therefore,
Lemma <ref> applied to the set $[y] \cap x$ yields the desired statement.

Now we come to the inductive definition of the aforementioned $M$- and $N$-matrices. Here is the precise list of objects that we are going to define:

* For every $[x] \in \{[x] \mid x \in \tc(\mu) \}$:

* An index-set $I_{[x]}$.

* A matrix $M[x] \in \bbF_2^{I_{[x]} \times E}$ with the property that $\Ker(M[x]) = \Stab_E(x)$ (note that $\Stab_E(x) = \Stab_E(x')$ for every $x' \in [x]$ by Lemma <ref>).

Let $\Cc[x] := \{ [y] \mid [y] \cap x \neq \emptyset \}$ (note that this does not depend on the representative of $[x]$ – see Lemma <ref>) denote the $\sim$-classes of the connected components of $x$.

* For every $[x] \in \{[x] \mid x \in \tc(\mu) \}$, where $x$ is a set,
and every $[y] \in \Cc[x]$:

* An index-set $J_{[x][y]}$.

* A matrix $N[x][y] \in \bbF_2^{J_{[x][y]} \times I_{[y]}}$ with the property that $\Ker(N[x][y] \cdot M[y]) = \Stab_E([y] \cap x)$ (by Lemma <ref>, $\Stab_E([y] \cap x)$ is independent of the choice of representative of $[x]$).

* For every orbit $\Omega_{[x]} := \Orb_G([x])$, let $I_{\Omega_{[x]}} := \biguplus_{[x'] \in \Omega_{[x]}} I_{[x']}$. For every $\Omega_{[x]}$, we provide a group homomorphism $g_{[x]} : \Stab_G(\mu) \lra \Sym(I_{\Omega_{[x]}})$ such that for each $[x'] \in \Omega_{[x]}$ and each $\pi \in \Stab_G(\mu)$, it holds $g_{[x]}(\pi)(I_{[x']}) = I_{\pi[x']}$. $M\pi[x'] = (g_{[x]},\pi)M[x']$ for each $[x'] \in \Omega_{[x]}$ and $\pi \in \Stab_G(\mu)$.

* For every orbit $\Omega_{[x]}$, let

\[
J_{\Omega_{[x]}} := \biguplus_{\stackrel{[x'] \in \Omega_{[x]}}{[y'] \in \Cc[x']}} J_{[x'][y']}.
\]

For every $\Omega_{[x]}$, we provide a group homomorphism $h_{[x]} : \Stab_G(\mu) \lra \Sym(J_{\Omega_{[x]}})$ such that for each $[x'] \in \Omega_{[x]}$ and each $[y'] \in \Cc[x']$, it holds $h_{[x]}(\pi)(J_{[x'][y']}) = J_{\pi[x']\pi[y']}$. Furthermore, $N\pi[x']\pi[y']= (h_{[x]}(\pi),g_{[x]}(\pi))N[x'][y']$ for each $[x'] \in \Omega_{[x]}$, $[y'] \in \Cc[x']$, and $\pi \in \Stab_G(\mu)$.

The role of the group homomorphisms is to ensure – when we build the circuit from these matrices – that every $\pi \in \Stab_G(\mu)$ that acts on the input gates indeed extends to an automorphism of $\widehat{C}(\mu)$. Before we actually construct anything, we have to verify that it is indeed possible to satisfy the symmetry conditions witnessed by the group homomorphisms and the conditions on the kernels of the matrices simultaneously. In other words, we have to show that the stabiliser spaces, which are supposed to be equal to the respective kernels, are mapped to each other by the permutations in $\Stab_G(\mu)$:

Let $x \in \tc(\mu)$ and $\pi \in \Stab_G(\mu)$. Then

\[
\Stab_E(\pi x) = \pi(\Stab_E(x)) = \{  \pi \mathbf{v} \mid \mathbf{v} \in \Stab_E(x)  \},
\]

where $\pi \in \Sym(E)$ acts on vectors in $\bbF_2^E$ by permuting their entries. Furthermore, for every $[y] \in \Cc[x]$, we have

\[
\Stab_E(\pi[y] \cap \pi x) = \pi(\Stab_E([y] \cap x)).
\]

For any $\pi \in \Aut(G)$, and any $\rho_F \in \Aut_{\CFI}(\GG)$, it holds $\rho_{\pi F} = \pi \circ \rho_F \circ \pi^{-1}$. Thus, $\rho_{\pi F} \in \Stab_E(\pi x)$ if and only if $(\pi \circ \rho_F \circ \pi^{-1})(\pi x) = \pi x$. This holds if and only if $(\pi \circ \rho_F)(x) = \pi x$, which is the case iff $\rho_F(x) = x$. This proves the first part of the lemma since $\chi(\pi F) = \pi(\chi(F))$. The second part can be shown in the same way because $\pi[y] \cap \pi x = \pi([y] \cap x)$. This last equation holds since the action of $\pi$ on $\HF(\widehat{E})$ is a bijection from $\HF(\widehat{E})$ to itself, so $\pi[y] \cap \pi x \subseteq \pi([y] \cap x)$ (this would not necessarily be true if $\pi$ were not injective on $\HF(\widehat{E})$).

§.§ Inductive construction

Base case:

Let $x = e_i$, for $e \in E$ and $i \in \{0,1\}$, be an atom in $\tc(\mu)$. Then we set

\[
M[x] := \chi(e)^T.
\]

Formally, we define the row index set as $I_{[x]} := \{[x]\}$, but any singleton set that is distinct from all other index sets will do.

Now for every orbit $\Omega_{[x]}$, where $x$ is an atom in $\tc(\mu)$, we define the homomorphism $g_{[x]} : \Stab_G(\mu) \lra \Sym(I_{\Omega_{[x]}})$ by letting $g_{[x]}(\pi)([x']) := [\pi x']$ for every $\pi \in \Stab_G(\mu)$, $[x'] \in I_{\Omega_{[x]}}$ (note that by definition of the index-sets $I_{[x]}$, $I_{\Omega_{[x]}}$ is equal to the orbit $\Omega_{[x]}$).

Inductive step:

We deal with the items from the above list in the order (b), (d), (a), (c).
Let $x \in \tc(\mu)$ be a non-atomic object, that is, a set. Assume that for every $[y] \in \Cc[x]$ and every $[y] \in \Cc[x']$, for every $[x'] \in \Omega_{[x]}$, the respective matrix $M[y]$ with index set $I_{[y]}$ has been constructed. Thus we also assume that for any such $[y]$, the homomorphism $g_{[y]}$ corresponding to $\Omega_{[y]}$ has been defined. We fix a $y$ such that $[y] \in \Cc[x]$. For this fixed pair $[x], [y]$ we will now construct the matrix $N[x][y]$. Then we will close it under the action of $\Stab_G(\mu)$. That is, given this matrix $N[x][y]$, we will symmetrically define $N[x'][y']$ for all $[y'] \in \Omega_{[y]}$, and all $[x'] \in \Omega_{[x]}$ such that $[y'] \in \Cc[x']$.

After this, there may still exist some components $[y'] \in \Cc[x]$ for which $N[x][y']$ has not been defined. In that case, we fix such a $[y'] \in \Cc[x]$, define the corresponding matrix $N[x][y']$ explicitly, and define the matrices for all $\Stab_G(\mu)$-images of $[x]$ and $[y']$ symmetrically, and so on. Hence, we first have to describe how to define the respective initial matrix from which we obtain the other ones by symmetry.

*Definition of the N-matrices
Let $y \in \tc(\mu)$ be such that $[y] \in \Cc[x]$.
We assume that $M[y]$, $I_{[y]}$ and $g_{[y]}$ have been constructed.
The matrix $N[x][y]$ is defined as the smallest Boolean matrix that satisfies the following two conditions:

* $
\Ker(N[x][y]) \cap \Im(M[y]) = M[y] \cdot \Stab_E([y] \cap x) = \{ (M[y] \cdot \mathbf{v}) \mid \mathbf{v} \in \Stab_E([y] \cap x)  \}.

(For a matrix $M \in \bbF_2^{I \times J}$, $\Im(M)$ denotes the space that is the image of $\bbF_2^J$ under $M$).

* There exists a homomorphism $h$ from $g_{[y]}(\Stab_G([y] \cap x)) \leq \Sym(I_{[y]})$ into the symmetric group on the row index set of $N[x][y]$ such that for every $\sigma \in g_{[y]}(\Stab_G([y] \cap x))$, it holds $(h(\sigma), \sigma)(N[x][y]) = N[x][y]$.

In the second property, we abused notation and wrote $g_{[y]}(\Stab_G([y] \cap x))$ for a subgroup of $\Sym(I_{[y]})$, even though $g_{[y]}(\Stab_G([y] \cap x))$ is formally a subgroup of $\Sym(I_{\Omega_{[y]}})$. However, we know from Corollary <ref> that $\Stab_G([y] \cap x) \leq \Stab_G([y])$, so $g_{[y]}(\Stab_G([y] \cap x))$ indeed maps the row index set of $M[y]$, that is, $I_{[y]}$, to itself (see property (c) of $g_{[y]}$ that holds by the induction hypothesis).

By “smallest” matrix we mean one that satisfies (i) and (ii) and has the least number of rows. If there are multiple such matrices with the same minimal number of rows, we choose an arbitrary one of them for $N[x][y]$.

Let $m$ be the number of rows of $N[x][y]$. We define the row index set $J_{[x][y]}$ of $N[x][y]$ as an $m$-element set that is disjoint from all other index sets constructed so far. Formally, this can be achieved by letting $J_{[x][y]} := \{ (i,[x],[y]) \mid i \in [m]  \}$.

We have to show that there always exists a matrix that satisfies (a) and (b). A matrix satisfying (a) can be found with methods from linear algebra:

Let $\Gamma \leq \Delta \leq \bbF_2^I$ be Boolean vector spaces. Let $d$ be the dimension of $\Gamma$ and $k = \dim \Delta - d$ be the codimension of $\Gamma$ in $\Delta$. There exists a matrix $N \in \bbF_2^{[k] \times I}$ such that $\Ker(N) \cap \Delta = \Gamma$.

Each of the $k$ rows of $N$ can be obtained as the solution to a linear equation system. For $i \in [k]$, $j \in I$, let $n_{ij} := N_{ij}$ denote the sought entry in row $i$ and column $j$. Fix a basis $\Bb_{\Gamma}$ of $\Gamma$, and an extension of that basis $\Bb \supseteq \Bb_{\Gamma}$ such that $\Bb = \Bb_{\Gamma} \uplus \{ \mathbf{w}_1,...,\mathbf{w}_k \}$ is a basis of $\Delta$. For each $i \in [k]$, we define an equation system $A_i \cdot \mathbf{x} = \mathbf{b}_i$ whose unique solution vector is the desired row $(n_{i1}, n_{i2},...,n_{i|I|})$ of $N$. The system has $\dim \Delta$ many equations, where each equation is associated with a basis vector in $\Bb$. For every basis vector $\mathbf{v} \in \Bb \setminus \{ \mathbf{w}_i\}$, we have the equation

\[
\sum_{j \in I}\mathbf{v}(j)\cdot \mathbf{x}(j) = 0
\]

in the system $A_i \cdot \mathbf{x} = \mathbf{b}_i$. For the basis vector $\mathbf{w}_i \in \Bb$, we have the equation

\[
\sum_{j \in I}\mathbf{w}_i(j)\cdot \mathbf{x}(j) = 1
\]

in $A_i \cdot \mathbf{x} = \mathbf{b}_i$. In this way, we define $k$ equation systems, one for each $i \in [k]$. In fact, the coefficient matrix $A_i$ is the same for all of them. Its rows are the vectors in $\Bb$ (transposed). The vector $\mathbf{b}_i$ has a $1$-entry in the row containing $\mathbf{w}_i$, and is zero otherwise. The rank and the number of rows of every $A_i$ is $\dim \Delta$ because $\Bb$ is a basis of $\Delta$. Hence, each of the equation systems has a unique solution. If we define each entry $n_{ij}$ of $N$ to be the $j$-th entry of the solution vector to $A_i \cdot \mathbf{x} = \mathbf{b}_i$, then indeed, $\Ker(N) \cap \Delta = \Gamma$, by definition of the equation systems.

This shows that a matrix satisfying condition (a) always exists. The matrix can be closed under the action of $g_{[y]}(\Stab_G([y] \cap x))$ so that it also satisfies condition (b). This requires that the vector space that we want as the kernel of $N[x][y]$ is invariant under that permutation group:

The space $M[y] \cdot \Stab_E([y] \cap x) \leq \bbF_2^{I_{[y]}}$ is invariant under the action of the permutation group $g_{[y]}(\Stab_G([y] \cap x)) \leq \Sym(I_{[y]})$ on the entries of its vectors. That is, for every $\mathbf{v} \in M[y] \cdot \Stab_E([y] \cap x)$ and $\pi \in g_{[y]}(\Stab_G([y] \cap x))$, it holds $\pi(\mathbf{v}) \in M[y] \cdot \Stab_E([y] \cap x)$.

Let $\mathbf{v} \in M[y] \cdot \Stab_E([y] \cap x)$ and $\pi \in g_{[y]}(\Stab_G([y] \cap x))$. We can write $\mathbf{v} = M[y] \cdot \mathbf{w}$ for some $\mathbf{w} \in \Stab_E([y] \cap x)$. Fix a $\sigma \in g^{-1}_{[y]}(\pi)$, i.e. $\sigma \in \Stab_G([y] \cap x)$. By Proposition <ref> it holds:

\[
(\pi, \sigma)(M[y]) \cdot \sigma(\mathbf{w}) = \pi(\mathbf{v}).
\]

From the inductive hypothesis we have that $(\pi, \sigma)(M[y]) = M[y]$ since $\sigma \in \Stab_G([y] \cap x) \leq \Stab_G([y])$ (see item (c) in the enumeration above). The fact that $\Stab_G([y] \cap x) \leq \Stab_G([y])$ is shown in Corollary <ref>. We conclude: $M[y] \cdot \sigma(\mathbf{w}) = \pi(\mathbf{v})$. If $\sigma(\mathbf{w}) \in \Stab_E([y] \cap x)$, then we are done and have that $\pi(\mathbf{v}) \in M[y] \cdot \Stab_E([y] \cap x)$, as desired. To show that $\sigma(\mathbf{w}) \in \Stab_E([y] \cap x)$, we apply Lemma <ref>: Since $\mathbf{w} \in \Stab_E([y] \cap x)$, we have $\sigma \mathbf{w} \in \sigma (\Stab_E([y] \cap x) )= \Stab_E(\sigma[y] \cap \sigma x)$. Finally, as mentioned in the proof of Lemma <ref>, we have $\sigma[y] \cap \sigma x = \sigma([y] \cap x)$, and it holds $\sigma([y] \cap x) = [y] \cap x$, because $\sigma \in \Stab_G([y] \cap x)$.

Knowing this, we can see that it is indeed possible to satisfy both conditions (i) and (ii) at the same time.

Let $[y] \in \Cc[x]$. There exists a Boolean matrix $N$ that satisfies conditions (i) and (ii) mentioned above, i.e.:

* $
\Ker(N) \cap \Im(M[y]) = M[y] \cdot \Stab_E([y] \cap x).

* There exists a homomorphism $h$ from $g_{[y]}(\Stab_G([y] \cap x)) \leq \Sym(I_{[y]})$ into the symmetric group on the row index set of $N$ such that for every $\sigma \in g_{[y]}(\Stab_G([y] \cap x))$, it holds $(h(\sigma), \sigma)(N) = N$.

Lemma <ref> applied to $\Delta = \Im(M[y])$ and $\Gamma =  M[y] \cdot \Stab_E([y] \cap x)$ gives us a matrix $N' \in \bbF_2^{[k] \times I_{[y]}}$ that satisfies condition (i); here, $k = \dim (\Im \ M[y]) - \dim( M[y] \cdot \Stab_E([y] \cap x) )$. We can close $N'$ under the action of $g_{[y]}(\Stab_G([y] \cap x)) \leq \Sym(I_{[y]})$ so that condition (ii) is also satisfied: For each row $N'_{i-}$ of $N'$, let $\Orb(N'_{i-}) := \{ \pi(N'_{i-}) \mid \pi \in g_{[y]}(\Stab_G([y] \cap x)) \}$. Here, $\pi \in \Sym(I_{[y]}) $ permutes the columns, i.e. the entries of the respective row $N'_{i-}$. Now let $N$ be the Boolean matrix whose set of rows is the disjoint union $\biguplus_{i \in [k]} \Orb(N'_{i-})$. Clearly, there is a homomorphism $h$ from $g_{[y]}(\Stab_G([y] \cap x))$ into the symmetric group on the rows of $N$ (more precisely into $\Pi_{i \in [k]} \Sym(\Orb(N'_{i-}))$). This homomorphism is just the group action of $g_{[y]}(\Stab_G([y] \cap x))$ on the rows of $N$ (separately on the orbits $\Orb(N'_{i-})$).

It remains to show that this symmetry-closed matrix $N$ still satisfies condition (i), i.e. that $\Ker(N) \cap \Im(M[y]) = M[y] \cdot \Stab_E([y] \cap x)$. We have $\Ker(N) \cap \Im(M[y]) \subseteq M[y] \cdot \Stab_E([y] \cap x)$ because for any vector $\mathbf{v} \notin M[y] \cdot \Stab_E([y] \cap x)$, either $\mathbf{v} \notin \Im(M[y])$, or if $\mathbf{v} \in \Im(M[y])$, then $N' \cdot \mathbf{v} \neq \mathbf{0}$ because $\Ker(N') \cap \Im(M[y]) = M[y] \cdot \Stab_E([y] \cap x)$. Since $N'$ is a submatrix of $N$, we also have $N \cdot \mathbf{v} \neq \mathbf{0}$, so $\mathbf{v} \notin \Ker(N)$. Therefore, $\Ker(N) \cap \Im(M[y]) \subseteq M[y] \cdot \Stab_E([y] \cap x)$. It remains to show: $M[y] \cdot \Stab_E([y] \cap x) \subseteq \Ker(N) \cap \Im(M[y])$. So let $\mathbf{v} \in M[y] \cdot \Stab_E([y] \cap x)$. Then $N' \cdot \mathbf{v} = \mathbf{0}$. We have to prove that for every row $N'_{i-}$ and every $\pi \in g_{[y]}(\Stab_G([y] \cap x))$, we have $\pi(N'_{i-}) \cdot \mathbf{v} = 0$. It holds (see Proposition <ref>):

\[
\pi(N'_{i-}) \cdot \mathbf{v} = \pi^{-1}(\pi(N'_{i-})) \cdot \pi^{-1}\mathbf{v} = N'_{i-} \cdot \pi^{-1}\mathbf{v} = 0.
\]

The final equality holds because $\Ker(N') = M[y] \cdot \Stab_E([y] \cap x)$, and $\pi^{-1}\mathbf{v} \in M[y] \cdot \Stab_E([y] \cap x)$ by Lemma <ref>. Since each row of $N$ is of the form $\pi(N'_{i-})$ for some row $i$ of $N'$ and $\pi \in g_{[y]}(\Stab_G([y] \cap x))$, we have shown that $M[y] \cdot \Stab_E([y] \cap x) \subseteq \Ker(N) \cap \Im(M[y])$.

This lemma shows that there exists a Boolean matrix satisfying conditions (i) and (ii), so it is indeed possible to pick a smallest one for $N[x][y]$. The trouble is that we do not know a priori how small it is. Therefore, the construction of $\widehat{C}(\mu)$ that we are describing does not come with a guaranteed size bound. Later on in Section <ref> we will get back to the choice of $N[x][y]$ and show how we can bound its size in case that $\Stab_E([y] \cap x)$ has a symmetric basis. The idea will be that the size of the closure of $N'$ under the action of $g_{[y]}(\Stab_G([y] \cap x))$ can be bounded then, because the symmetries of the basis of $\Stab_E([y] \cap x)$ “propagate” through the equation systems $A_i \cdot \mathbf{x} = \mathbf{b}_i$ that are used to define the rows of $N'$.

Since at least one matrix satisfying (i) and (ii) exists, $N[x][y]$ can indeed be defined as the smallest one. Remember that this definition was for a fixed $[y] \in \Cc[x]$. Now let $[y'] \in \Omega_{[y]}$, and $[x'] \in \Omega_{[x]}$ such that $[y'] \in \Cc[x']$ and such that there is a $\pi \in \Stab_G(\mu)$ with $\pi([y] \cap x) = [y'] \cap x'$ (it may be that $[x'] = [x]$). Set $\pi_{[x'][y']} := \pi$, so we can refer back to this particular permutation in the future.
We set $J_{[x'][y']} :=  \{ (i,[x'],[y']) \mid i \in [m]  \}$. Here, $m$ still denotes the number of rows of the previously defined $N[x][y]$.
Let $N[x'][y']$ be the Boolean matrix in $\bbF_2^{J_{[x'][y']} \times I_{[y']}}$ such that $(N[x'][y'])_{(k,[x'],[y']),g_{[y]}(\pi_{[x'][y']})(i)} = (N[x][y])_{(k,[x],[y]),i}$ for every $i \in I_{[y]}$ and $k \in [m]$. We will usually write $N([x'][y'])_{k,-}$ instead of $(N[x'][y'])_{(k,[x'],[y']),-}$ to denote the $k$-th row of the matrix.
In this way, we define the matrices $N[x'][y']$ for all $[y'] \in \Omega_{[y]}$. We will call the $\sim$-class $[y] \in \Cc[x]$, that we arbitrarily chose as the first one in its orbit to define $N[x][y]$ with Lemma <ref>, the primer of the orbit $\Omega_{[y]}$. We proceed to pick a new primer $[y] \in \Cc[x]$ for which $N[x][y]$ has not been defined so far, and repeat the construction for $[y]$ and its orbit $\Omega_{[y]}$. This is done until $N[x][y]$ is defined for every $[y] \in \Cc[x]$ and for every $[y'] \in \Cc[x']$, for every $[x'] \in \Omega_{[x]}$.

We show that the defined matrices have the desired properties:

Let $[x'] \in \Omega_{[x]}$ and $[y'] \in \Cc[x']$. Then

\[
\Ker(N[x'][y'] \cdot M[y']) = \Stab_E([y'] \cap x').
\]

Let $[y] \in \Cc[x]$ be the primer of the orbit $\Omega_{[y']}$ that was used in the matrix construction. Then $[y'] = \pi_{[x'][y']} [y]$ and $[x'] = \pi_{[x'][y']} [x]$. If $[y'] = [y]$, then $\pi_{[x'][y']}$ is the identity permutation in $\Sym(V)$. For ease of notation, we write $\pi :=  \pi_{[x'][y']}$ in the following. By Lemma <ref>, we have

\[
\Stab_E([y'] \cap x') =  \Stab_E(\pi[y] \cap \pi x) = \pi(\Stab_E([y] \cap x)).
\]

By definition of $N[x][y]$, and because $\Ker(M[y]) = \Stab_E(y) \leq \Stab_E([y] \cap x)$, we have $\Ker(N[x][y] \cdot M[y]) = \Stab_E([y] \cap x)$. It holds $M[y'] = (g_{[y]}(\pi),\pi)M[y]$ (item (c) of the inductive hypothesis). So for any vector $\mathbf{v} \in \bbF_2^E$, we have $M[y'] \cdot \pi(\mathbf{v}) = g_{[y]}(\pi)( M[y] \cdot \mathbf{v})$. Here, $g_{[y]}(\pi)$ acts on a vector $\mathbf{w} \in \bbF_2^{I_{[y]}}$ by mapping it to a vector $\mathbf{w}' \in \bbF_2^{I_{[y']}}$ with $\mathbf{w}'(g_{[y]}(\pi)(i)) = \mathbf{w}(i)$ for every $i \in I_{[y]}$. By definition, we have for the $k$-th row of $N[x'][y']$: $N([x'][y'])_{k,-} = g_{[y]}(\pi)(N([x][y])_{k,-} )$. In total, this means that for every $\mathbf{v} \in \bbF_2^E$, it holds:

\[
N([x'][y'])_{k,-} \cdot M[y'] \cdot \pi(\mathbf{v}) = N([x][y])_{k,-} \cdot M[y] \cdot \mathbf{v}.
\]

Therefore, $\Ker(N[x'][y'] \cdot M[y']) = \pi(\Ker(N[x][y] \cdot M[y])) = \pi(\Stab_E([y] \cap x)) = \Stab_E([y'] \cap x')$.

The proofs of the next lemmas are given in the appendix. They concern the symmetries of the constructed $N$-matrices, and essentially follow directly from the construction of the first $N$-matrix and the fact that the other $N$-matrices are symmetric to it. The formal proofs involve tedious calculations, though.

Let $[x'] \in \Omega_{[x]}$ and $[y'] \in \Cc[x']$. There exists a homomorphism $h'$ from $g_{[y']}(\Stab_G([y'] \cap x')) \leq \Sym(I_{[y']})$ into the symmetric group on the row index set of $N[x'][y']$ such that for every $\sigma \in g_{[y']}(\Stab_G([y'] \cap x'))$, it holds $(h'(\sigma), \sigma)(N[x'][y']) = N[x'][y']$.

Proof sketch.
Let $[y] \in \Cc[x]$ be the primer of $\Omega_{[y']}$. Then for $N[x][y]$, the lemma holds by construction because we explicitly closed the rows of $N[x][y]$ under these symmetries. For $N[x'][y']$, the result follows by symmetry of the construction.

TODO: This proof is not yet rewritten!!! Take the one from the thesis for the appendix!!
Let $[y] \in \Cc[x]$ be the primer of $\Omega_{[y']}$. Let $\pi_{[x'][y']} \in \Stab_G(\mu)$ be the permutation that was used to define $N[x'][y']$ from $N[x][y]$. For the matrix $N[x][y]$, there exists such a homomorphism $h : g_{[y]}(\Stab_G([y] \cap x)) \lra \Sym(J_{[x][y]})$ by definition of the matrix. We define the desired homomorphism $h': g_{[y']}(\Stab_G([y'] \cap x')) \lra \Sym(J_{[x'][y']})$ as follows. For every $\pi \in \Stab_G([y'] \cap x')$ and every $(i,[x'],[y']) \in J_{[x'][y']}$, let

\[
h'(g_{[y']}(\pi))(i,[x'],[y']) := (j,[x'],[y']),
\]

where $j$ is the number such that

\[
h(g_{[y]}(\pi^{-1}_{[x'][y']} \circ \pi \circ \pi_{[x'][y']}))(i,[x],[y]) = (j,[x],[y]).
\]

For every $\pi \in \Stab_G([y'] \cap x')$, $h(g_{[y']}(\pi))$ is indeed a permutation in $\Sym(J_{[x'][y']})$, because $N[x][y]$ and $N[x'][y']$ have the same number of rows (and the index sets $J_{[x][y]}$ and $J_{[x'][y']}$ differ only with respect to the second and third entry of the index triples), and $(\pi^{-1}_{[x'][y']} \circ \pi \circ \pi_{[x'][y']}) \in \Stab_G([y] \cap x)$, so $h(g_{[y]}(\pi^{-1}_{[x'][y']} \circ \pi \circ \pi_{[x'][y']}))$ is a permutation on the rows of $N[x][y]$.

The fact that $h'$ is a group homomorphism follows directly from the fact that $h$ is one.
Finally, we have to show that for every $\sigma \in g_{[y']}(\Stab_G([y'] \cap x'))$, it holds $(h(\sigma), \sigma)(N[x'][y']) = N[x'][y']$. To prove this, we show that $N[x'][y']_{h(\sigma)(j,[x'],[y']),\sigma(i)} = N[x'][y']_{(j,[x'],[y']),i}$ for every $(j,[x'],[y']) \in J_{[x'][y']}$ and $i \in I_{[y']}$. In the following, we will use that by definition of $N[x'][y']$, we have: $N[x'][y'] = (\text{id},g_{[y]}(\pi_{[x'][y']}))(N[x][y])$. Let $\sigma = g_{[y']}(\pi) = g_{[y]}(\pi)$ for a $\pi \in \Stab_G([y'] \cap x')$. Then for any $(j,[x'],[y']) \in J_{[x'][y']}, i \in I_{[y']}$, we obtain:

\begin{align*}
N[x'][y']_{h(\sigma)(j,[x'],[y']),\sigma(i)} &= (N[x][y])_{h'(g_{[y]}(\pi^{-1}_{[x'][y']} \circ \pi \circ \pi_{[x'][y']}))(j,[x],[y]),(g_{[y]}(\pi_{[x'][y']})^{-1} \circ \sigma)(i)}\\
&= (N[x][y])_{h'(g_{[y]}(\pi^{-1}_{[x'][y']} \circ \pi \circ \pi_{[x'][y']}))(j,[x],[y]),g_{[y]}(\pi_{[x'][y']}^{-1} \circ \pi \circ \pi_{[x'][y']})(i')}\\
&=  (N[x][y])_{(j,[x],[y]),i'}.
\end{align*}

In the second step, we used that $\sigma(i) = g_{[y']}(\pi)(i)$, and we replaced $i \in I_{[y']}$ with $g_{[y]}(\pi_{[x'][y']})(i')$ for some $i' \in I_{[y]}$ (which can be done because of item (c) of the induction hypothesis for $I_{[y]}$ and $I_{[y']} = I_{\pi_{[x'][y']}[y]}$). We also used that $g_{[y]}$ is a group homomorphism. The last step holds because we already know that $h'$ satisfies the property that we are trying to prove for $h$, i.e. $(h'(\sigma'),\sigma')N[x][y] = N[x][y]$ for any $\sigma' \in g_{[y]}(\Stab_G([y] \cap x))$. We can continue the equation, using the definition of $N[x'][y']$ again:

\begin{align*}
(N[x][y])_{(j,[x],[y]),i'} &= (N[x'][y'])_{(j,[x'],[y']),g_{[y]}(\pi_{[x'][y']})(i')}\\
&= (N[x'][y'])_{(j,[x'],[y']),i}.
\end{align*}

This proves that $((h(\sigma), \sigma)(N[x'][y'])) = N[x'][y']$, as desired.

Lemmas <ref> and <ref> assert that all the constructed matrices $N[x'][y']$ satisfy the properties (i) and (ii) that $N[x][y]$ has by construction.

Now let

\[
J_{\Omega_{[x]}} := \bigcup_{\stackrel{[x'] \in \Omega_{[x]}}{[y'] \in \Cc[x']}} J_{[x'][y']}.
\]

We provide a group homomorphism $h_{[x]} : \Stab_G(\mu) \lra \Sym(J_{\Omega_{[x]}})$ such that for each $[x'] \in \Omega_{[x]}$ and each $[y'] \in \Cc[x']$, it holds $h_{[x]}(\pi)(J_{[x'][y']}) = J_{\pi[x']\pi[y']}$. Furthermore, we want that $(N\pi[x']\pi[y']) = (h_{[x]}(\pi),g_{[x]}(\pi))N[x'][y']$ for each $[x'] \in \Omega_{[x]}$, $[y'] \in \Cc[x']$, and $\pi \in \Stab_G(\mu)$.
For each triple $(k,[x'],[y']) \in J_{\Omega_{[x]}}$, we set:

\[
h_{[x]}(\pi)(k,[x'],[y']) := (\ell, \pi[x'],\pi[y']),
\]

where $\ell$ is defined as follows: Let

\[
t := |\{ i \in \{1,2,...,k-1 \} \mid (N[x'][y'])_{i,-} = (N[x'][y'])_{k,-}  \}|.
\]

That is, for the $k$-th row of $N[x'][y']$, there are $t$ rows identical to it with a smaller index. Then $\ell$ is defined such that

\[
|\{ i \in \{1,2,...,\ell-1 \} \mid (N\pi[x']\pi[y'])_{i,-} = g_{[y']}(\pi)((N[x'][y'])_{k,-})  \}| = t,
\]

and such that $(N\pi[x']\pi[y'])_{\ell,-} = g_{[y']}(\pi)((N[x'][y'])_{k,-})$. In other words, $\ell$ is the $(t+1)$st row of $N\pi[x']\pi[y']$ which is equal to the $k$-th row of $N[x][y]$, up to a permutation of the columns given by $g_{[y']}(\pi)$.

We have to argue that $h_{[x]}(\pi)(k,[x'],[y'])$ is indeed well-defined:

Let $[x'] \in \Omega_{[x]}, [y'] \in \Cc[x']$. Let $\pi \in \Stab_G(\mu)$. Then for every $(k,[x'],[y']) \in J_{[x'][y']}$, the number of rows of $N[x'][y']$ which are equal to the $k$-th row is the same as the number of rows of $N\pi[x']\pi[y']$ that are equal to the $k$-th row of $N[x'][y']$, up to application of $g_{[y']}$ to the columns. Formally:

\begin{align*}
&|\{ (i,[x'],[y']) \in J_{[x'][y']} \mid (N[x'][y'])_{(i,[x'],[y']),-} = (N[x'][y'])_{k,-} \}| \\
= &| \{ (i,\pi[x'],\pi[y']) \in J_{\pi[x']\pi[y']} \mid (N\pi[x']\pi[y'])_{(i,\pi[x'],\pi[y']),-} = g_{[y']}((N[x'][y'])_{k,-}) \}   |
\end{align*}

Proof sketch. Follows again from the fact that $N[x'][y']$ and $N\pi[x']\pi[y']$ are by construction symmetric to each other.

Let $[y] \in \Cc[x]$ be the primer of $\Omega_{[y']}$, and write $\sigma := \pi_{[x'][y']}, \sigma' := \pi_{\pi[x']\pi[y']}$. So these are the two permutations in $\Stab_G(\mu)$ that were used to construct $N[x'][y']$ and $N\pi[x']\pi[y']$ from $N[x][y]$. By construction of these matrices, it holds $N[x'][y'] = (\text{id},g_{[y]}(\sigma))(N[x][y])$ and $N[x'][y'] = (\text{id},g_{[y]}(\sigma'))(N[x][y])$. Thus, $(N\pi[x']\pi[y'])_{k,-} = (g_{[y]}(\sigma') \circ g_{[y]}(\sigma)^{-1})((N[x'][y'])_{k,-})$. Since $g_{[y]}$ is a group homomorphism, we can also write this as:

\[
(N\pi[x']\pi[y'])_{k,-} = g_{[y]}(\sigma' \circ \sigma^{-1})((N[x'][y'])_{k,-}) \tag{$\star$}
\]

If $\sigma' \circ \sigma^{-1}$ were equal to $\pi$, then this would suffice to prove the lemma. However, we only know that $(\sigma' \circ \sigma^{-1})([y'] \cap x') = \pi([y'] \cap x')$. We use this to show the following

Claim: Let $m$ be the number of rows of $N[x'][y']$ and $N\pi[x']\pi[y']$. There exists a permutation $\theta \in \Sym_m$ such that $(N\pi[x']\pi[y'])_{\theta(k),-} = g_{[y]}(\pi)((N[x'][y'])_{k,-})$, for every $k \in [m]$.

Proof. It holds that $(\pi \circ \sigma \circ (\sigma')^{-1}) \in \Stab_G(\pi[y'] \cap \pi x')$. By Lemma <ref>, there exists a $\theta \in \Sym_m$ such that $(\theta, g_{[y]}(\pi \circ \sigma \circ (\sigma')^{-1})))(N\pi[x']\pi[y']) = N\pi[x']\pi[y']$. It holds $\sigma \circ (\sigma')^{-1} = (\sigma' \circ \sigma^{-1})^{-1}$. Thus, by $(\star)$ we have: $(N[x'][y'])_{k,-} = g_{[y]}(\sigma \circ (\sigma')^{-1})((N\pi[x']\pi[y'])_{k,-})$. It follows that $(N\pi[x']\pi[y'])_{\theta(k),-} = g_{[y]}(\pi)(N[x'][y'])_{k,-}$ for every $k \in [m]$. This proves the claim.

The claim entails the lemma because $g_{[y']} = g_{[y]}$ (as $\Omega_{[y]} = \Omega_{[y']})$, and so we know that the rows of $N\pi[x']\pi[y']$ are the rows of $N[x'][y']$, with an application of $g_{[y']}(\pi)$ to the columns, and a potential reordering of the rows.

This lemma shows that we can indeed define $h_{[x]}$ as we did. Now one can verify that $h_{[x]}$ is a group homomorphism with the desired properties. Again, we prove this in the appendix; it follows from the definition of $h_{[x]}$ and Lemma <ref>.

The mapping $h_{[x]} : \Stab_G(\mu) \lra \Sym(J_{\Omega_{[x]}})$ is a group homomorphism.
For every $[x'] \in \Omega_{[x]}$, $[y'] \in \Cc[x']$ and each $\pi \in \Stab_G(\mu)$, it holds $h_{[x]}(\pi)(J_{[x'][y']}) = J_{\pi[x']\pi[y']}$. Furthermore, $N\pi[x']\pi[y']= (h_{[x]}(\pi),g_{[y']}(\pi))N[x'][y']$ for each $[x'] \in \Omega_{[x]}$, $[y'] \in \Cc[x']$, and $\pi \in \Stab_G(\mu)$.

First, we show that $h_{[x]}$ is a group homomorphism. It can be seen directly from the definition that the identity permutation in $\Stab_G(\mu)$ is mapped to the identity permutation in $\Sym(J_{\Omega_{[x]}})$. Now let $\pi, \pi' \in \Stab_G(\mu)$. Let $(k,[x'],[y']) \in J_{\Omega_{[x]}}$. Then $h_{[x]}(\pi' \circ \pi)(k,[x'],[y']) = (\ell, (\pi' \circ \pi)[x'], (\pi' \circ \pi)[y'])$, where $\ell$ is such that

\[
(N(\pi' \circ \pi)[x'](\pi' \circ \pi)[y'])_{\ell,-} = g_{[y]}(\pi' \circ \pi)(N[x'][y']_{k,-}),
\]

and there are exactly $t$ rows identical to it with an index $< \ell$ in $N(\pi' \circ \pi)[x'](\pi' \circ \pi)[y']$. As in the definition, $t$ denotes the number of rows in $N[x'][y']$ with an index $< k$ that are identical to $(N[x'][y'])_{k,-}$. Now we want to argue that $(h_{[x]}(\pi') \circ h_{[x]}(\pi))(k,[x'],[y']) = (\ell, (\pi' \circ \pi)[x'], (\pi' \circ \pi)[y']) = h_{[x]}(\pi' \circ \pi)(k,[x'],[y'])$.

We have $h_{[x]}(\pi)(k,[x'],[y']) = (\ell_1, \pi[x], \pi[y])$, where $\ell_1$ is the row index in $N\pi[x']\pi[y']$ such that

\[
(N\pi[x']\pi[y'])_{\ell_1,-} = g_{[y]}(\pi)(N[x'][y']_{k,-}),
\]

and there are again exactly $t$ identical rows with index $< \ell_1$ in $N\pi[x']\pi[y']$. Thus we have $h_{[x]}(\pi')(\ell_1,\pi[x'],\pi[y']) = (\ell_2,(\pi' \circ \pi)[x'],(\pi' \circ \pi)[y'])$, where $\ell_2$ is the row index in $N(\pi' \circ \pi)[x'](\pi' \circ \pi)[y']$ such that

\[
(N(\pi' \circ \pi)[x'](\pi' \circ \pi)[y'])_{\ell_2,-} = g_{[y]}(\pi' \circ \pi)(N[x'][y']_{k,-}),
\]