Reasoning Shortcuts and Value Symmetries: What Symmetry Permits, Architecture Realizes, and Optimization Selects

# What Symmetry Permits, Architecture Realizes, and Optimization Selects
Source: [https://arxiv.org/html/2608.10420](https://arxiv.org/html/2608.10420)
## Reasoning Shortcuts and Value Symmetries: What Symmetry Permits, Architecture Realizes, and Optimization Selects

###### Abstract

Reasoning shortcuts are solutions of a neurosymbolic system’s rules that produce correct predictions through unintended concepts\. A recent framework of Takemura, Inoue and Nishino analyzes them through an automorphism group of value relabelings, and asks, as its central open question, when rules pin concepts down\. We first show that the framework’s key definition, one shared permutation applied at every position, does not apply as stated to any of the four heterogeneous benchmarks it was evaluated on: using it at all requires an embedding step the framework does not specify, and the most direct embedding, padding domains to a common size, produces confident false pathology:90\.91%90\.91\\%of solution pairs reported unexplained on CLE4EVR’s real rule, where the componentwise generalization we introduce reports0%0\\%, with the padded verdict’s content determined by configuration\-file ordering rather than rule structure\. Re\-measuring with the corrected instrument across eleven rule families, under fifteen predictions recorded before measurement \(thirteen confirmed\), we find unexplained\-pair rates spanning0%0\\%to99\.9999%99\.9999\\%that track checkable structure, which we then prove: six theorems give sufficient conditions for transitivity and its failure, including a Free Slot Lemma certifying Kandinsky’s pathology from syntax alone\. For rules given as circuits, deciding whether a designated coordinate is symmetry\-inert is coNP\-complete; deciding whether any nontrivial automorphism exists is coNP\-hard under randomized reductions, lies inΣ2𝗉\\Sigma\_\{2\}^\{\\mathsf\{p\}\}, is notΣ2𝗉\\Sigma\_\{2\}^\{\\mathsf\{p\}\}\-complete unless the polynomial hierarchy collapses, and on monotone circuits is coNP\-complete outright\. In the Boolean case transitivity is fully classified: the automorphisms explain everything exactly when the solution set is an affine coset\. Finally, weakly supervised models trained on rsbench arithmetic tasks place all9494observed concept\-level shortcuts at exactly the one level the componentwise theory flags as pathological and none at the4848it certifies transitive, with automorphism orbits explaining70%70\\%of them; twelve further levels flagged as ambiguous by the typed reading produce none, separating what symmetry permits from what optimization selects, and a dual\-head control whose independent perception networks realize the full componentwise group replicates the entire geography\. Every reported number traces to released, executable verification artifacts\.

## 1Introduction

A neurosymbolic system couples a learned perception component with a fixed body of symbolic knowledge\. The perception component maps raw inputs to symbolic concepts\. The knowledge maps concepts to predictions\. When the system reaches the right predictions through the wrong concepts, it has learned a*reasoning shortcut*: every rule is satisfied at training time, yet the learned concept mapping is not the intended one, and the error surfaces only later, on downstream tasks that reuse the concepts\[[15](https://arxiv.org/html/2608.10420#bib.bib15),[7](https://arxiv.org/html/2608.10420#bib.bib7)\]\. A self\-driving benchmark makes the stakes concrete\. A model can learn to predict*stop*correctly while confusing pedestrians with red lights, because both concepts imply stopping\[[7](https://arxiv.org/html/2608.10420#bib.bib7)\]\. The prediction is right\. The concept is wrong\. Everything downstream of the concept is compromised\.

Takemura, Inoue and Nishino\[[26](https://arxiv.org/html/2608.10420#bib.bib26)\]recently gave this problem an algebraic form\. Model the rules as a constraint satisfaction problem, collect the concept mappings that satisfy every rule into a solution set, and ask what structure the set of alternative solutions carries\. Their central tool is an automorphism group: a set of value relabelings that map solutions to solutions\. If two shortcuts differ only by an automorphism, they are the same failure wearing two labels, and symmetry\-aware training or evaluation can treat them as one\. Their paper closes by naming its most pressing open question: characterize when the rules pin the concepts down, beyond the case where the automorphism group is trivial\.

This paper starts from a fact about that framework which, to our knowledge, has not been reported\. The framework’s central definition does not apply to the benchmarks it was evaluated on\. Takemura et al\.’s automorphism group applies one shared permutation of one shared value set at every position\. The four rsbench benchmarks in their own evaluation all have heterogeneous attribute domains: colors, shapes and materials of different sizes, or twenty binary detectors with no shared label space\. On such instances the definition does not apply as stated: its hypotheses fail, and every use requires an embedding of typed attribute domains into one shared value set that the framework itself does not supply\. The most direct such embedding, padding every domain to a common size, does not fail conservatively\. On CLE4EVR’s real rule it reports that90\.91%90\.91\\%of solution pairs are unexplained pathology, where every well\-defined member of the value\-symmetry hierarchy reports0%0\\%on the same instance\. The reported pathology decomposes entirely into bookkeeping: which values the padded group identifies as interchangeable is decided by the order in which attributes happen to be listed in a configuration file, and permuting that order permutes the answer\. A practitioner who reaches for the published definition on a real, heterogeneous benchmark gets a confident, wrong, and unstable number\.

We therefore generalize the definition rather than the benchmarks\.*Componentwise value symmetry*lets every position carry its own value permutation over its own domain\. On homogeneous instances it contains the original group\. On heterogeneous instances it is the only one of the two definitions that is defined at all\. The rest of the paper asks, with this corrected instrument, the question the original framework raised: when do automorphisms account for the alternative solutions of real neurosymbolic rules, when do they not, what distinguishes the two cases, and how hard is it to decide?

The answers are specific enough to summarize\.

#### Contribution 1: a measured false positive \([Section2](https://arxiv.org/html/2608.10420#S2)\)\.

We show that porting the global definition to heterogeneous benchmarks by padding produces confident false pathology, quantify it on CLE4EVR’s public rule \(90\.91%90\.91\\%against0%0\\%, with the content of the reported pathology tracking configuration\-file order rather than rule structure\), and confirm on a5,4335\{,\}433\-instance synthetic sweep that the padded reading collapses to the trivial group on97%97\\%of heterogeneous instances\. The generalization is not an elegance\. It is the difference between a wrong answer and a right one\.

#### Contribution 2: structural determinants of pathology \([Section3](https://arxiv.org/html/2608.10420#S3)\)\.

Across three published benchmark families and eight further rule families, with fifteen structure\-to\-outcome predictions recorded before measurement \(thirteen confirmed\), the fraction of solution pairs that automorphisms fail to explain ranges from0%0\\%to99\.9999%99\.9999\\%, and the variation tracks checkable structural features of the rule\. Mild conjunctive structure is transitive: every solution pair is related by an automorphism\. Disjunctive structure is pathological or not depending on whether its branches are exchangeable by value permutations alone\. An absorbing element, a multiplicative zero, breaks an otherwise safe conjunction\. A counting bound forces pathology on all\-different constraints regardless of syntax\. The two predictions that failed are as informative as the thirteen that held: both failures isolated the precise condition, branch exchangeability by value permutation rather than syntactic disjunction, that the coarse prediction missed\.

#### Contribution 3: six theorems \([Section4](https://arxiv.org/html/2608.10420#S4)\)\.

We prove each empirical mechanism at least partially\. A single Forcing Lemma underlies sufficient conditions for transitivity \(matching decompositions, exchangeable branches\) and for its failure \(anchored inequality patterns, degree invariants, an orbit\-stabilizer counting bound, and a Free Slot Lemma that certifies Kandinsky’s81\.99%81\.99\\%pathology directly from its rule syntax, without enumerating the group\)\. A byproduct settles a natural conjecture negatively: conjunctive structure alone does not imply transitivity, by an explicit two\-constraint counterexample found in a randomized search of4,0004\{,\}000instances and then proved as a theorem\.

#### Contribution 4: the complexity of deciding \([Section5](https://arxiv.org/html/2608.10420#S5)\)\.

For rules given as compact circuits, deciding whether a designated coordinate is symmetry\-inert \(Dead\-Var\) is coNP\-complete, a known result we state here for completeness\[[4](https://arxiv.org/html/2608.10420#bib.bib4)\]\. Deciding whether any nontrivial automorphism exists \(Nontriv\-Aut\) is coNP\-hard under randomized reductions and lies inΣ2𝗉\\Sigma\_\{2\}^\{\\mathsf\{p\}\}\. The main complexity result is that it is notΣ2𝗉\\Sigma\_\{2\}^\{\\mathsf\{p\}\}\-complete unless the polynomial hierarchy collapses toΣ3𝗉\\Sigma\_\{3\}^\{\\mathsf\{p\}\}\. The collapse theorem adapts Agrawal and Thierauf’s argument for Boolean isomorphism\[[1](https://arxiv.org/html/2608.10420#bib.bib1)\]to a group that permutes values rather than named positions, a transplant that fails for their own labeling technique and succeeds through a laundering protocol that never names objects at all\. In the Boolean case we give the group an exact structure theory: it is always an𝔽2\\mathbb\{F\}\_\{2\}\-linear subspace, equal to the orthogonal complement of the Fourier support, which explains a constant the empirical chapter measures eight times over\. Two further results settle parts of the landscape outright rather than bounding them\. In the Boolean case, transitivity admits a complete classification, not merely sufficient conditions: the group acts freely, soAut​\(ΦC\)\\mathrm\{Aut\}\(\\Phi\_\{C\}\)explains all shortcuts exactly whenΦC\\Phi\_\{C\}is an affine coset, and an exact orbit law reproduces every BDD\-OIA percentage of[Section3](https://arxiv.org/html/2608.10420#S3)to the last digit\. And on monotone circuits the existence question is coNP\-complete under deterministic reductions, because monotone functions provably cannot carry the camouflage symmetries that force the general reduction to randomize\. An appendix charts the obstruction landscape between randomized coNP\-hardness and the collapse bound in the general case, distilling a systematic sweep of the standard toolkits into three structural facts any future attack must clear\.

#### Contribution 5: the shortcut geography of trained models \([Section6](https://arxiv.org/html/2608.10420#S6)\)\.

We train standard weakly supervised neurosymbolic models on rsbench’s MNIST arithmetic tasks, ten seeds per task\. All9494observed concept\-level shortcuts occur at exactly the one target level the componentwise theory identifies as pathological, and none at the4848levels it certifies as transitive \(34,80034\{,\}800of the experiment’s40,00040\{,\}000model\-instance evaluations\)\. The typed reading then sharpens the result into this paper’s cleanest experiment: it flags twelve further levels as architecture\-realizable ambiguities, and not one of them produces a single shortcut, isolating gradient starvation at the multiplicative zero, predicted in advance by the loss algebra, as the mechanism that selects which ambiguity materializes\. A dual\-head control, rerunning everything with independently weighted perception networks so that the full componentwise group becomes architecture\-realizable, replicates the geography under pre\-specified predictions: all 101 of itsproductshortcuts land on the same single level, the twelve typed\-ambiguous levels stay empty, and the same\-orbit share moves only from70\.2%70\.2\\%to71\.3%71\.3\\%\. Automorphism orbits explain70%70\\%of the observed shortcuts, and the correspondence between symbolic prediction and learned failure separates three things a single number usually conflates: what symmetry permits, what architecture realizes, and what optimization selects\.

#### Instrument and evidence discipline\.

Componentwise value symmetry is positioned, not presumed\. It is the finest member of a hierarchy of well\-defined value\-symmetry readings \(global, typed, componentwise;[Section2](https://arxiv.org/html/2608.10420#S2)\); the members agree exactly on the headline instances, and where they genuinely part, on unconstrained slots and on equality patterns,[Section6](https://arxiv.org/html/2608.10420#S6)measures the divergence and turns it into the paper’s sharpest experiment\. No member of the hierarchy supports the padded verdict\. The theory arrives in two matched halves, orbit combinatorics for general domains and linear algebra for Boolean ones, and each half carries a real benchmark that needs it: Kandinsky’s certificate comes from the Free Slot Lemma, BDD\-OIA’s from the subspace structure\. Every number in the paper traces, through a comment in the source, to a machine\-computed artifact in the released verification data\.

[Section2](https://arxiv.org/html/2608.10420#S2)develops the framework and the false positive\.[Section3](https://arxiv.org/html/2608.10420#S3)reports the measurements\.[Section4](https://arxiv.org/html/2608.10420#S4)proves the six theorems\.[Section5](https://arxiv.org/html/2608.10420#S5)maps the decision problems\.[Section6](https://arxiv.org/html/2608.10420#S6)closes the loop on trained models, and[Sections7](https://arxiv.org/html/2608.10420#S7)and[8](https://arxiv.org/html/2608.10420#S8)situate and conclude\.

## 2Background: Global Value Symmetry on Heterogeneous Domains

This section builds the formal apparatus the rest of the paper uses\. Section[2\.1](https://arxiv.org/html/2608.10420#S2.SS1)recalls constraint satisfaction \(CSP\) notation and the automorphism\-based account of reasoning shortcuts due to Takemura, Inoue and Nishino\[[26](https://arxiv.org/html/2608.10420#bib.bib26)\]\. It then shows that their central definition, a single global permutation of one shared value set, does not literally apply to any of the four real neurosymbolic benchmarks it was evaluated on\. Section[2\.2](https://arxiv.org/html/2608.10420#S2.SS2)introduces the generalization this paper studies, componentwise value symmetryAut​\(ΦC\)\\mathrm\{Aut\}\(\\Phi\_\{C\}\), in which every position chooses its own value permutation\. Section[2\.3](https://arxiv.org/html/2608.10420#S2.SS3)shows why this generalization is not optional\. Forcing Takemura et al\.’s original definition onto a heterogeneous benchmark by padding its domains to a common size reports a90\.91%90\.91\\%pathology rate on CLE4EVR’s real rule where the componentwise definition finds none\. The naive port is not merely less general\. It is wrong\.

### 2\.1Reasoning shortcuts and the automorphism framework

A neurosymbolic system learns to map raw inputs to symbolic concepts, then reasons over those concepts with a fixed set of logical or arithmetic rules\. A reasoning shortcut occurs when the system satisfies every rule at training time without recovering the intended concept mapping\. The network learns some mapping consistent with the rules, but not necessarily the one a human would call correct\. Takemura, Inoue and Nishino\[[26](https://arxiv.org/html/2608.10420#bib.bib26)\]formalize this as a constraint satisfaction problem and ask when the rules alone pin the mapping down to a single, intended solution\.

###### Definition 2\.1\(Constraint satisfaction instance\)\.

Fix a finite index set of positionsN=\{1,…,n\}N=\\\{1,\\dots,n\\\}\. Each positioni∈Ni\\in Nhas a finite, nonempty local domainSiS\_\{i\}\. The domains need not coincide, so\|Si\|\|S\_\{i\}\|can differ across positions\. A constraint setCCis a finite set of relations, each over some subset of positions\. A mappingϕ∈∏i∈NSi\\phi\\in\\prod\_\{i\\in N\}S\_\{i\}satisfiesCCif it satisfies every relation inCC\. The solution set is

ΦC=\{ϕ∈∏i∈NSi:ϕ​satisfies every constraint in​C\}\.\\Phi\_\{C\}\\;=\\;\\Big\\\{\\,\\phi\\in\\textstyle\\prod\_\{i\\in N\}S\_\{i\}\\;:\\;\\phi\\text\{ satisfies every constraint in \}C\\,\\Big\\\}\.A constraint\-based neurosymbolic learning problem additionally fixes an intended mappingϕ∗∈ΦC\\phi^\{\*\}\\in\\Phi\_\{C\}and a datasetDD\. A mappingϕ∈ΦC\\phi\\in\\Phi\_\{C\}is a*reasoning shortcut*ifϕ≠ϕ∗\\phi\\neq\\phi^\{\*\}\. The problem is*shortcut\-free*ifΦC=\{ϕ∗\}\\Phi\_\{C\}=\\\{\\phi^\{\*\}\\\}, and the shortcut multiplicity isSM​\(C\):=\|ΦC\|−1\\mathrm\{SM\}\(C\):=\|\\Phi\_\{C\}\|\-1\.

Takemura et al\.’s central definition targets the bijective case directly\. It requiresSi≡SS\_\{i\}\\equiv Sfor every position, so thatΦCbij\\Phi\_\{C\}^\{\\mathrm\{bij\}\}is well defined, and it requires\|N\|=\|S\|\|N\|=\|S\|, since a bijectionN→SN\\to Scan only exist when the two sets have the same size\.

###### Definition 2\.3\(Global value symmetry; Takemura et al\.\[[26](https://arxiv.org/html/2608.10420#bib.bib26)\], Definition 7\)\.

SupposeSi≡SS\_\{i\}\\equiv Sfor alli∈Ni\\in Nand\|N\|=\|S\|\|N\|=\|S\|\. Each permutationσ∈Sym​\(S\)\\sigma\\in\\mathrm\{Sym\}\(S\)acts on mappings by post\-composition,\(σ∘ϕ\)​\(i\)=σ​\(ϕ​\(i\)\)\(\\sigma\\circ\\phi\)\(i\)=\\sigma\(\\phi\(i\)\)\. The automorphism group ofX=\(N,S,C\)X=\(N,S,C\)is

Aut​\(X\):=\{σ∈Sym​\(S\):σ∘ϕ∈ΦCbij​for all​ϕ∈ΦCbij\}\.\\mathrm\{Aut\}\(X\)\\;:=\\;\\big\\\{\\,\\sigma\\in\\mathrm\{Sym\}\(S\)\\;:\\;\\sigma\\circ\\phi\\in\\Phi\_\{C\}^\{\\mathrm\{bij\}\}\\text\{ for all \}\\phi\\in\\Phi\_\{C\}^\{\\mathrm\{bij\}\}\\,\\big\\\}\.

A single global permutation is applied identically at every position\.Aut​\(X\)\\mathrm\{Aut\}\(X\)is the setwise stabilizer ofΦCbij\\Phi\_\{C\}^\{\\mathrm\{bij\}\}insideSym​\(S\)\\mathrm\{Sym\}\(S\), acting diagonally\.

###### Proposition 2\.4\(Value\-symmetry elimination; Takemura et al\.\[[26](https://arxiv.org/html/2608.10420#bib.bib26)\], Proposition 2\)\.

IfAut​\(X\)\\mathrm\{Aut\}\(X\)is trivial, that isAut​\(X\)=\{id\}\\mathrm\{Aut\}\(X\)=\\\{\\mathrm\{id\}\\\}, then no two distinct solutions inΦCbij\\Phi\_\{C\}^\{\\mathrm\{bij\}\}are related by a permutation inAut​\(X\)\\mathrm\{Aut\}\(X\)\.

The proof is immediate\. Ifϕ′=σ∘ϕ\\phi^\{\\prime\}=\\sigma\\circ\\phifor someσ∈Aut​\(X\)\\sigma\\in\\mathrm\{Aut\}\(X\), triviality forcesσ=id\\sigma=\\mathrm\{id\}, soϕ′=ϕ\\phi^\{\\prime\}=\\phi\. Proposition[2\.4](https://arxiv.org/html/2608.10420#S2.Thmtheorem4)rules out one specific mechanism for multiple solutions: a global relabeling drawn fromAut​\(X\)\\mathrm\{Aut\}\(X\)itself\. It does not imply\|ΦCbij\|=1\|\\Phi\_\{C\}^\{\\mathrm\{bij\}\}\|=1\. Two solutions can be related by a permutation outsideAut​\(X\)\\mathrm\{Aut\}\(X\), or by no permutation at all\. A complete characterization of sufficient conditions for uniqueness beyond trivial automorphism groups is, in Takemura et al\.’s own framing, the most pressing question their analysis leaves open\.

The CP literature distinguishes several notions of symmetry for a CSP instance\. Cohen, Jeavons, Jefferson, Petrie and Smith\[[10](https://arxiv.org/html/2608.10420#bib.bib10)\]separate*constraint symmetry*, a permutation of variable\-value pairs that preserves the constraint relations themselves, from*solution symmetry*, a permutation that merely preserves the solution set\. They prove every constraint symmetry is a solution symmetry \(their Theorem 1\), though the converse can fail badly\. They exhibit a CSP withnnvariables andddvalues each, with a unique solution, whose solution\-symmetry group nonetheless has ordern\!​\(n​\(d−1\)\)\!n\!\\,\(n\(d\-1\)\)\!\(their Example 3\): freely permuting thennvariable\-value pairs the one solution uses contributes then\!n\!factor, and freely permuting then​\(d−1\)n\(d\-1\)pairs it leaves unused contributes the rest, since acting within either of these two disjoint sets on its own cannot disturb the one solution\. Definition[2\.3](https://arxiv.org/html/2608.10420#S2.Thmtheorem3)is a solution symmetry of a narrow kind\. It never permutes positions\. It fixesNNpointwise and applies a single permutation of the shared value setSSidentically at every position\. We call it*global value symmetry*\. The generalization introduced in Section[2\.2](https://arxiv.org/html/2608.10420#S2.SS2), where each position chooses its own value permutation independently, sits strictly between global value symmetry and Cohen et al\.’s unrestricted solution symmetry\. We call it*componentwise*, or*per\-variable*,*value symmetry*\.

None of the four rsbench benchmarks used to evaluate Definition[2\.3](https://arxiv.org/html/2608.10420#S2.Thmtheorem3)satisfies its shared\-domain hypothesis\. Bortolotti et al\.’s rsbench\[[7](https://arxiv.org/html/2608.10420#bib.bib7)\]specifies CLE4EVR concretely\. Two rendered objects each carry four attributes, color, shape, material and size, with public default domain sizes 2, 3, 2 and 3 respectively\. The eight resulting positions do not share one value setSS\. They range over four semantically unrelated, differently sized sets\. Kandinsky’s three objects are more regular: shape and color domains both have size 3\. But shape values \(circle, square, triangle\) and color values \(red, yellow, blue\) remain two different sets, not one sharedSS\. BDD\-OIA and SDD\-OIA are the starkest case\. Takemura et al\.’s own Table 1 recordsN=21N=21for both\. The public rsbench decision logic is a function of “4 actions from 20 interrelated concepts”\[[7](https://arxiv.org/html/2608.10420#bib.bib7)\], and direct inspection of its arguments confirms it takes exactly 20 free binary inputs\. The 21st recorded field,road\_clear, is logically determined by four of the other twenty\. An exhaustive check over all2202^\{20\}assignments confirmsroad\_clear≡¬\(car∨person∨rider∨other\_obstacle\)\\texttt\{road\\\_clear\}\\equiv\\neg\(\\texttt\{car\}\\lor\\texttt\{person\}\\lor\\texttt\{rider\}\\lor\\texttt\{other\\\_obstacle\}\), so it carries no independent information\. Twenty positions, each with its own two\-valued domain\{0,1\}\\\{0,1\\\}, drive the four action labels, and there is no natural sense in which a red\-light detector and a left\-turn\-lane detector take values from one shared label setSS\. Definition[2\.3](https://arxiv.org/html/2608.10420#S2.Thmtheorem3)’s bijective restriction additionally requires\|N\|=\|S\|\|N\|=\|S\|\. For CLE4EVR \(\|N\|=8\|N\|=8split across four differently sized attribute types\) and for BDD\-OIA/SDD\-OIA \(\|N\|=20\|N\|=20free positions,\|Si\|=2\|S\_\{i\}\|=2at every position\) this equality has no natural reading\. Applying Definition[2\.3](https://arxiv.org/html/2608.10420#S2.Thmtheorem3)to these benchmarks requires an extra step the definition itself does not supply: some way of embedding heterogeneous attribute domains into one sharedSS\. Section[2\.3](https://arxiv.org/html/2608.10420#S2.SS3)shows this step is not innocuous\.

Takemura et al\.’s own published evaluation is consistent with this reading, not in tension with it\. Their formalization fixes a single shared domain from the start \(their Definition 1: variablesNN, one domainSS\), and their bijective results additionally force\|S\|=\|N\|\|S\|=\|N\|\. Their Table 1 reports5,7595\{,\}759bijective shortcuts for CLE4EVR atN=8N=8, which under their own definitions presupposes an88\-element shared value set, while the benchmark’s native typed structure carries ten values across four semantically distinct attribute types\. Some re\-encoding of typed attributes into one untyped domain was therefore necessarily applied on their side; every encoding printed in their paper declares a single sharedval\(0\.\.k\)domain \(their toy examples\), and the specific re\-encoding behind the benchmark rows is not given\. We make no claim that their published counts are incorrect under their own encoding\. The claim is about the step in between: the framework’s definition attaches to a typed benchmark only through a translation into one shared domain, the translation is not part of the framework, and Section[2\.3](https://arxiv.org/html/2608.10420#S2.SS3)shows the resulting verdict depends materially on which translation is chosen\.

### 2\.2The independent\-coordinate generalization

Section[2\.1](https://arxiv.org/html/2608.10420#S2.SS1)shows that Definition[2\.3](https://arxiv.org/html/2608.10420#S2.Thmtheorem3)needs a single shared value setSSthat none of the four benchmarks naturally provides\. We now generalize the definition itself, rather than the benchmarks, letting every position keep its own local domainSiS\_\{i\}and its own value permutation\.

###### Definition 2\.5\(Componentwise value symmetry\)\.

Forσ=\(σ1,…,σn\)∈∏i=1nSym​\(Si\)\\sigma=\(\\sigma\_\{1\},\\dots,\\sigma\_\{n\}\)\\in\\prod\_\{i=1\}^\{n\}\\mathrm\{Sym\}\(S\_\{i\}\)andϕ∈∏i∈NSi\\phi\\in\\prod\_\{i\\in N\}S\_\{i\}, writeσ⋅ϕ\\sigma\\cdot\\phifor the mapping with\(σ⋅ϕ\)​\(i\)=σi​\(ϕ​\(i\)\)\(\\sigma\\cdot\\phi\)\(i\)=\\sigma\_\{i\}\(\\phi\(i\)\)for everyi∈Ni\\in N\. The automorphism group ofΦC\\Phi\_\{C\}is the setwise stabilizer ofΦC\\Phi\_\{C\}under this action,

Aut​\(ΦC\)=\{σ∈∏i=1nSym​\(Si\):σ⋅ϕ∈ΦC​for all​ϕ∈ΦC\}\.\\mathrm\{Aut\}\(\\Phi\_\{C\}\)\\;=\\;\\big\\\{\\,\\sigma\\in\\prod\_\{i=1\}^\{n\}\\mathrm\{Sym\}\(S\_\{i\}\)\\;:\\;\\sigma\\cdot\\phi\\in\\Phi\_\{C\}\\text\{ for all \}\\phi\\in\\Phi\_\{C\}\\,\\big\\\}\.

Every position chooses its own value permutationσi∈Sym​\(Si\)\\sigma\_\{i\}\\in\\mathrm\{Sym\}\(S\_\{i\}\)independently\. Nothing requiresSi=SjS\_\{i\}=S\_\{j\}fori≠ji\\neq j, and nothing requiresσi=σj\\sigma\_\{i\}=\\sigma\_\{j\}\.

###### Observation 2\.6\(Componentwise symmetry contains global value symmetry, on any common solution set\)\.

SupposeSi≡SS\_\{i\}\\equiv Sfor alli∈Ni\\in N\. LetΔ=\{\(σ,…,σ\):σ∈Sym​\(S\)\}≤∏i=1nSym​\(Si\)\\Delta=\\\{\(\\sigma,\\dots,\\sigma\):\\sigma\\in\\mathrm\{Sym\}\(S\)\\\}\\leq\\prod\_\{i=1\}^\{n\}\\mathrm\{Sym\}\(S\_\{i\}\)be the diagonal subgroup; the mapσ↦\(σ,…,σ\)\\sigma\\mapsto\(\\sigma,\\dots,\\sigma\)is a group isomorphismSym​\(S\)→Δ\\mathrm\{Sym\}\(S\)\\to\\Delta, and\(σ,…,σ\)⋅ϕ=σ∘ϕ\(\\sigma,\\dots,\\sigma\)\\cdot\\phi=\\sigma\\circ\\phi\. Consequently, for*any*fixed solution setΨ\\Psi, the diagonal stabilizer ofΨ\\Psiis exactlyStab∏i=1nSym​\(Si\)​\(Ψ\)∩Δ\\mathrm\{Stab\}\_\{\\prod\_\{i=1\}^\{n\}\\mathrm\{Sym\}\(S\_\{i\}\)\}\(\\Psi\)\\cap\\Delta: read off one common solution set, componentwise symmetry contains global value symmetry as its diagonal part\. In particularAut​\(X\)\\mathrm\{Aut\}\(X\)from Definition[2\.3](https://arxiv.org/html/2608.10420#S2.Thmtheorem3)is isomorphic to the diagonal part of the componentwise stabilizer ofΦCbij\\Phi\_\{C\}^\{\\mathrm\{bij\}\}\.

The qualifier “on any common solution set” is load\-bearing\. The two definitions as published read their groups off*different*sets,ΦCbij\\Phi\_\{C\}^\{\\mathrm\{bij\}\}for Definition[2\.3](https://arxiv.org/html/2608.10420#S2.Thmtheorem3)and the generalΦC\\Phi\_\{C\}for Definition[2\.5](https://arxiv.org/html/2608.10420#S2.Thmtheorem5), and across that divide neither group need contain the other\. A three\-solution example settles it: withN=S=\{0,1\}N=S=\\\{0,1\\\}andΦC=\{\(0,0\),\(0,1\),\(1,0\)\}\\Phi\_\{C\}=\\\{\(0,0\),\(0,1\),\(1,0\)\\\}\(the rule¬\(x1∧x2\)\\neg\(x\_\{1\}\\wedge x\_\{2\}\)\), the value swap preservesΦCbij=\{\(0,1\),\(1,0\)\}\\Phi\_\{C\}^\{\\mathrm\{bij\}\}=\\\{\(0,1\),\(1,0\)\\\}, so it lies inAut​\(X\)\\mathrm\{Aut\}\(X\), yet it maps\(0,0\)\(0,0\)to\(1,1\)∉ΦC\(1,1\)\\notin\\Phi\_\{C\}, so its diagonal copy is not inAut​\(ΦC\)\\mathrm\{Aut\}\(\\Phi\_\{C\}\)\. The bijective restriction is not a cosmetic convention: it changes the group\. Computationally verified; see[AppendixB](https://arxiv.org/html/2608.10420#A2)\. Observation[2\.6](https://arxiv.org/html/2608.10420#S2.Thmtheorem6)only applies on homogeneous instances, whereSi≡SS\_\{i\}\\equiv Sfor every position\. On heterogeneous instances, no diagonal subgroup exists and Definition[2\.3](https://arxiv.org/html/2608.10420#S2.Thmtheorem3)simply has nothing to say\. CLE4EVR, Kandinsky, BDD\-OIA and SDD\-OIA are all heterogeneous in this sense \(Section[2\.1](https://arxiv.org/html/2608.10420#S2.SS1)\)\. Componentwise value symmetry is not a refinement of global value symmetry on the cases that matter here\. It is the only one of the two definitions that is even well defined on them\.

Componentwise is not the only well\-defined reading, however, and we do not claim it is uniquely correct\. Between one permutation for all positions and one permutation per position sits a natural intermediate\.

###### Definition 2\.7\(Typed value symmetry\)\.

Letτ:N→T\\tau:N\\to Tassign each position a semantic type, with a shared domainStS\_\{t\}for all positions of typett\(soSi=Sτ​\(i\)S\_\{i\}=S\_\{\\tau\(i\)\}\)\. The typed group isGτ:=∏t∈TSym​\(St\)G\_\{\\tau\}:=\\prod\_\{t\\in T\}\\mathrm\{Sym\}\(S\_\{t\}\), acting by\(σ⋅ϕ\)​\(i\):=στ​\(i\)​\(ϕ​\(i\)\)\(\\sigma\\cdot\\phi\)\(i\):=\\sigma\_\{\\tau\(i\)\}\(\\phi\(i\)\), and the typed automorphism groupAutτ​\(ΦC\)\\mathrm\{Aut\}\_\{\\tau\}\(\\Phi\_\{C\}\)is its setwise stabilizer ofΦC\\Phi\_\{C\}\.

Taking one type for all positions recovers Definition[2\.3](https://arxiv.org/html/2608.10420#S2.Thmtheorem3)\(when it is defined\); taking every position as its own type recovers Definition[2\.5](https://arxiv.org/html/2608.10420#S2.Thmtheorem5)\. Typed value symmetry is well defined on all four benchmarks, with types given by the attribute kinds \(CLE4EVR: color, shape, material, size, each shared by the two objects\)\. Which rung of this hierarchy counts two shortcuts as “the same failure” is a modeling choice with an architectural reading, to which we return in[Section6](https://arxiv.org/html/2608.10420#S6): a perception network shared across same\-type positions can realize exactly the typed relabelings, while independent per\-position heads realize componentwise ones\. What matters for this paper is knowing exactly where the choice changes the answer, and this paper measures it rather than assuming it\. On CLE4EVR’s six constrained dimensions the typed and componentwise groups coincide exactly, element for element, and so do their orbits \(\|Aut\|=24\|\\mathrm\{Aut\}\|=24, transitive,0%0\\%\); on Kandinsky they coincide as well \(\|Aut\|=36\|\\mathrm\{Aut\}\|=36, the same six orbits,81\.99%81\.99\\%\)\. The two readings genuinely part in two situations: on entirely unconstrained positions, as in CLE4EVR’s free size slots \(Table[1](https://arxiv.org/html/2608.10420#S2.T1): componentwise stays transitive, typed splits equal\-size from unequal\-size pairs,44\.86%44\.86\\%\), and on*equality patterns*inside constrained levels, where the diagonal action preserves whether two same\-type positions agree while independent permutations do not\.[Section6](https://arxiv.org/html/2608.10420#S6)meets thirteen levels of the second kind and turns the divergence into this paper’s sharpest experiment, a three\-way separation of what symmetry permits, what architecture realizes, and what optimization selects\. The padded reading agrees with no rung of the hierarchy on any instance measured\. Throughout, componentwise is the default instrument, the coarsest\-orbit member \(most generous to the symmetry hypothesis\) requiring no typing choice, and every place the rung changes an answer is flagged where it occurs\.

Componentwise value symmetry still sits inside Cohen et al\.’s general solution symmetry\[[10](https://arxiv.org/html/2608.10420#bib.bib10)\]\. It fixes positions pointwise and factors through the product∏i=1nSym​\(Si\)\\prod\_\{i=1\}^\{n\}\\mathrm\{Sym\}\(S\_\{i\}\), so it cannot reach the unstructured pair permutations behind theirn\!​\(n​\(d−1\)\)\!n\!\\,\(n\(d\-1\)\)\!blow\-up\. It remains sensitive to a milder version of the same underlying issue\. A position that no constraint inCCactually restricts contributes its fullSym​\(Si\)\\mathrm\{Sym\}\(S\_\{i\}\)toAut​\(ΦC\)\\mathrm\{Aut\}\(\\Phi\_\{C\}\)regardless of the rest of the instance, inflating the group with automorphisms that reflect an absent constraint rather than a genuine symmetry of the rule\. Section[2\.3](https://arxiv.org/html/2608.10420#S2.SS3)encounters exactly this pattern in CLE4EVR’s unconstrained size attributes, and we return to recognizing such positions systematically, as a decision problem in its own right, in[Section5](https://arxiv.org/html/2608.10420#S5)\.

###### Observation 2\.8\(Boolean domains give linear structure\)\.

SupposeSi=\{0,1\}S\_\{i\}=\\\{0,1\\\}for everyi∈Ni\\in N\. ThenSym​\(Si\)\\mathrm\{Sym\}\(S\_\{i\}\)has order 2, generated by the bit flip, soSym​\(Si\)≅𝔽2\\mathrm\{Sym\}\(S\_\{i\}\)\\cong\\mathbb\{F\}\_\{2\}as a group\. Consequently∏i=1nSym​\(Si\)≅𝔽2n\\prod\_\{i=1\}^\{n\}\\mathrm\{Sym\}\(S\_\{i\}\)\\cong\\mathbb\{F\}\_\{2\}^\{n\}, coordinatewise\. SinceAut​\(ΦC\)≤∏i=1nSym​\(Si\)\\mathrm\{Aut\}\(\\Phi\_\{C\}\)\\leq\\prod\_\{i=1\}^\{n\}\\mathrm\{Sym\}\(S\_\{i\}\)is a subgroup, and every subgroup of an𝔽2\\mathbb\{F\}\_\{2\}\-vector space is automatically an𝔽2\\mathbb\{F\}\_\{2\}\-linear subspace,Aut​\(ΦC\)\\mathrm\{Aut\}\(\\Phi\_\{C\}\)is an𝔽2\\mathbb\{F\}\_\{2\}\-linear subspace of𝔽2n\\mathbb\{F\}\_\{2\}^\{n\}\.

Observation[2\.8](https://arxiv.org/html/2608.10420#S2.Thmtheorem8)is a statement about the ambient group\. It does not say which subspace actually arises for a given rule\. BDD\-OIA and SDD\-OIA are Boolean in exactly this sense \(Section[2\.1](https://arxiv.org/html/2608.10420#S2.SS1)\), and the algebraic characterization in[Section4](https://arxiv.org/html/2608.10420#S4)determines which subspaceAut​\(ΦC\)\\mathrm\{Aut\}\(\\Phi\_\{C\}\)occupies once the rule structure is taken into account\.

### 2\.3The padded extension: a measured false positive

The generalization in Section[2\.2](https://arxiv.org/html/2608.10420#S2.SS2)is only useful if it changes the answer on real rules\. This section measures that on CLE4EVR, using rsbench’s public default configuration\[[7](https://arxiv.org/html/2608.10420#bib.bib7)\], and finds that it does\. The two definitions do not just differ in generality\. On the same data, they disagree about whether a pathology exists at all\.

Definition[2\.3](https://arxiv.org/html/2608.10420#S2.Thmtheorem3)cannot be evaluated on CLE4EVR directly\. Its eight positions split across four differently sized attribute domains \(Section[2\.1](https://arxiv.org/html/2608.10420#S2.SS1)\), so there is no sharedSSand no bijectiveΦCbij\\Phi\_\{C\}^\{\\mathrm\{bij\}\}\. The most direct way to force the definition to apply, and the one a practitioner reaching for Definition[2\.3](https://arxiv.org/html/2608.10420#S2.Thmtheorem3)off the shelf would likely try first, is to pad every position’s domain to a common sizeM=maxi⁡\|Si\|M=\\max\_\{i\}\|S\_\{i\}\|, using the order in which values are listed in the source configuration file as an arbitrary numeric labeling\{0,…,\|Si\|−1\}\\\{0,\\dots,\|S\_\{i\}\|\-1\\\}\. The search then looks for a single permutationσ∈Sym​\(\{0,…,M−1\}\)\\sigma\\in\\mathrm\{Sym\}\(\\\{0,\\dots,M\-1\\\}\), applied identically, by numeric label, at every position\.

One thing must be pinned down before any number is reported: the padded object is*not*Definition[2\.3](https://arxiv.org/html/2608.10420#S2.Thmtheorem3)verbatim, and cannot be\. Padding equalizes domain sizes, but it does not restore the definition’s bijective hypothesis: CLE4EVR has\|N\|=6\|N\|=6or88against\|S\|=M=3\|S\|=M=3, soΦCbij\\Phi\_\{C\}^\{\\mathrm\{bij\}\}is empty after padding, and the literal Definition[2\.3](https://arxiv.org/html/2608.10420#S2.Thmtheorem3)evaluates to the full groupSym​\(M\)\\mathrm\{Sym\}\(M\)stabilizing an empty solution set, a verdict about nothing\. The informative object, the one a practitioner in fact computes, is the definition’s action extended to the general solution set, the*padded diagonal extension*

Autpad:=\{σ∈Sym​\(\{0,…,M−1\}\):σ∘ϕ∈ΦC​for all​ϕ∈ΦC\}\.\\mathrm\{Aut\}\_\{\\mathrm\{pad\}\}\\;:=\\;\\big\\\{\\,\\sigma\\in\\mathrm\{Sym\}\(\\\{0,\\dots,M\-1\\\}\)\\;:\\;\\sigma\\circ\\phi\\in\\Phi\_\{C\}\\text\{ for all \}\\phi\\in\\Phi\_\{C\}\\,\\big\\\}\.Every padded figure in this paper isAutpad\\mathrm\{Aut\}\_\{\\mathrm\{pad\}\}, labeled as the extension it is; that the port must already drop the bijective restriction to produce any verdict at all is one more sense in which the translation step is not innocuous\. The comparison below is therefore between the two objects one can actually evaluate on the benchmark,Autpad\\mathrm\{Aut\}\_\{\\mathrm\{pad\}\}and the componentwiseAut​\(ΦC\)\\mathrm\{Aut\}\(\\Phi\_\{C\}\)\(Definition[2\.5](https://arxiv.org/html/2608.10420#S2.Thmtheorem5)\), on the same real rule and the same real solution set\.

CLE4EVR pairs two rendered objects, each with four attributes: color, shape, material and size, with domain sizes 2, 3, 2 and 3 respectively\. The public default rule requires the two objects to match on the first three attributes and leaves size unconstrained,

C:color1=color2∧shape1=shape2∧material1=material2\.C:\\quad\\mathrm\{color\}\_\{1\}=\\mathrm\{color\}\_\{2\}\\ \\wedge\\ \\mathrm\{shape\}\_\{1\}=\\mathrm\{shape\}\_\{2\}\\ \\wedge\\ \\mathrm\{material\}\_\{1\}=\\mathrm\{material\}\_\{2\}\.Restricting to the six positions the rule actually mentions \(color\_1,shape\_1,material\_1,color\_2,shape\_2,material\_2\), the raw space has2⋅3⋅2⋅2⋅3⋅2=1442\\cdot 3\\cdot 2\\cdot 2\\cdot 3\\cdot 2=144tuples, of which\|ΦC\|=12\|\\Phi\_\{C\}\|=12satisfyCC: the diagonal set of matching \(color, shape, material\) triples,2⋅3⋅2=122\\cdot 3\\cdot 2=12\. Including the two free size coordinates gives a second, larger instance with\|ΦC\|=108=12×9\|\\Phi\_\{C\}\|=108=12\\times 9, confirming that the free coordinates contribute exactly a multiplicative factor of3×33\\times 3and nothing else\.

This is a different, well\-defined quantity from Takemura et al\.’s own reported count of 5,759 bijective shortcuts for CLE4EVR\. Their Appendix G states only that all 8 concepts are preserved and that 4 synthetic samples encode the classification rule, without specifying how four differently sized attribute domains are packed into one bijective label space\. This encoding is not reconstructible from the public rsbench configuration\. rsbench’s own paper is not fully consistent about CLE4EVR’s shape and color domain sizes either, reporting 10 shapes and 10 colors in one table and nine shapes with eight predefined colors in its appendix, against the repository default of 3 shapes and 2 colors used throughout this paper\. We therefore measure the general solution setΦC\\Phi\_\{C\}\(Definition[2\.1](https://arxiv.org/html/2608.10420#S2.Thmtheorem1)\) directly, on the real public rule and domains\. This is the reading that is actually well defined for this data\.

Table 1:Componentwise value symmetry \(Definition[2\.5](https://arxiv.org/html/2608.10420#S2.Thmtheorem5)\) and typed value symmetry \(Definition[2\.7](https://arxiv.org/html/2608.10420#S2.Thmtheorem7)\) against the padded diagonal extensionAutpad\\mathrm\{Aut\}\_\{\\mathrm\{pad\}\}of Takemura et al\.’s global value symmetry \(Section[2\.3](https://arxiv.org/html/2608.10420#S2.SS3); the literal Definition[2\.3](https://arxiv.org/html/2608.10420#S2.Thmtheorem3)degenerates after padding, since no bijectionN→SN\\to Sexists\), on the same real rule and solution set\. “6\-dim” restricts to the six positions the rule mentions \(the primary measurement\); “8\-dim” includes the two unconstrained size positions\. Pairwise% is the fraction of unordered solution pairs\{ϕ,ϕ′\}⊆ΦC\\\{\\phi,\\phi^\{\\prime\}\\\}\\subseteq\\Phi\_\{C\}that lie in different orbits of the corresponding group\. On the constrained six dimensions the two well\-defined readings agree exactly, as groups and orbit by orbit; they part only on the free size slots, and the padded verdict agrees with neither on either instance\.[Figure1](https://arxiv.org/html/2608.10420#S2.F1)visualizes this same contrast directly, including how the padded definition’s choice of which shape counts as “fixed” rotates with attribute list order alone\.

Componentwise \(Definition[2\.5](https://arxiv.org/html/2608.10420#S2.Thmtheorem5)\)\|Aut​\(ΦC\)\|=24\|\\mathrm\{Aut\}\(\\Phi\_\{C\}\)\|=24, 1 orbit0\.00% unexplainedPadded extension of Definition[2\.3](https://arxiv.org/html/2608.10420#S2.Thmtheorem3)\|Autpad\|=2\|\\mathrm\{Aut\}\_\{\\mathrm\{pad\}\}\|=2, 6 orbits90\.91% unexplainedsame 12solutions\(toroid, star, cube\)fixed:cube\(cube, star, toroid\)fixed:toroid\(star, cube, toroid\)fixed:toroid\(toroid, cube, star\)fixed:starconfigorder:Figure 1:The same\|ΦC\|=12\|\\Phi\_\{C\}\|=12CLE4EVR solutions from Table[1](https://arxiv.org/html/2608.10420#S2.T1)’s 6\-dim row, under the componentwise definition \(Definition[2\.5](https://arxiv.org/html/2608.10420#S2.Thmtheorem5)\) versus the padded diagonal extensionAutpad\\mathrm\{Aut\}\_\{\\mathrm\{pad\}\}of Takemura et al\.’s global definition \(the literal Definition[2\.3](https://arxiv.org/html/2608.10420#S2.Thmtheorem3)has no bijective solutions to act on after padding\)\. Left:\|Aut​\(ΦC\)\|=24\|\\mathrm\{Aut\}\(\\Phi\_\{C\}\)\|=24, a single orbit,0\.00%0\.00\\%of solution pairs unexplained\. Right:\|Autpad\|=2\|\\mathrm\{Aut\}\_\{\\mathrm\{pad\}\}\|=2, the same 12 solutions split into 6 orbits of size 2,90\.91%90\.91\\%of pairs unexplained\. Bottom: re\-running the padded search after reordering only the shape attribute’s listing in the source config file leaves the group size and orbit count unchanged but changes which shape is left unpaired \(toroid, then cube, then toroid, then star across four orderings\)—the padded pathology’s*content*is an artifact of list order, not of rule structure\.The padded definition’s headline number,90\.91%90\.91\\%of solution pairs unexplained by any automorphism \(6060of\(122\)=66\\binom\{12\}\{2\}=66pairs, since 6 orbits of size 2 each account for 6 same\-orbit pairs\), looks like a serious pathology\. Decoding the one non\-trivial padded automorphism back into real attribute values shows what it actually is\. Under the natural ordering, the order in which colors, shapes and materials are listed in the public config file, the non\-trivial element simultaneously mapsred↔blue\\mathrm\{red\}\\leftrightarrow\\mathrm\{blue\},rubber↔metal\\mathrm\{rubber\}\\leftrightarrow\\mathrm\{metal\}, and swaps two of the three shapes while fixing the third \(cube↔star\\mathrm\{cube\}\\leftrightarrow\\mathrm\{star\}, toroid fixed\)\. Padding forces three semantically unrelated attributes, color, material and shape, to share one abstract label space, so the search for a single global permutation finds one only by inventing cross\-attribute correspondences the rule never states\. Which shape ends up the odd one out is decided entirely by list order, not by the rule\. Re\-running the same search after permuting only the order in which shapes are listed changes which shape is fixed, while the group’s size stays exactly 2 throughout:

- •shape order\(cube, star, toroid\), the order in the public config file: toroid is fixed;
- •reversed,\(toroid, star, cube\): cube is fixed;
- •\(star, cube, toroid\): toroid is fixed;
- •\(toroid, cube, star\): star is fixed\.

The group’s order is stable under these relabelings\. Three further reorderings, reversing the shape list, reversing the color list, and swapping the color list, all leave\|Autpad\|=2\|\\mathrm\{Aut\}\_\{\\mathrm\{pad\}\}\|=2, 6 orbits, and the90\.91%90\.91\\%pairwise figure unchanged\. So the magnitude of the padded pathology is not noise\. Its content, which values it identifies as interchangeable, is bookkeeping, not structure\. Nothing in the rule distinguishes toroid from cube from star\. Padding manufactures a distinction anyway, and hands out a different one depending on how the config file happens to list its attributes\.

The componentwise definition disagrees with this completely\. On the same rule and the same solution set,Aut​\(ΦC\)\\mathrm\{Aut\}\(\\Phi\_\{C\}\)is transitive: all 12 solutions form a single orbit, and0%0\\%of pairs are unexplained\. This is not a matter of the componentwise definition being more permissive and therefore finding more structure by construction\. It is the more restrictive of the two groups relative to its own ambient group,2424of576576possible independent\-coordinate permutations \(4\.17%4\.17\\%\) against22of66possible padded permutations \(33\.33%33\.33\\%\), and it still explains every solution as one orbit, while the padded definition, despite retaining a larger share of its own ambient group, fails to explain90\.91%90\.91\\%of pairs\. The disagreement is not a rounding difference\. One definition reports a rule with no unexplained shortcuts\. The other reports a rule that is90\.91%90\.91\\%pathological\. Both cannot be describing the same underlying structure well\. Observation[2\.6](https://arxiv.org/html/2608.10420#S2.Thmtheorem6)explains why: on a heterogeneous instance like CLE4EVR, Definition[2\.3](https://arxiv.org/html/2608.10420#S2.Thmtheorem3)is not merely coarser than Definition[2\.5](https://arxiv.org/html/2608.10420#S2.Thmtheorem5)\. It is undefined\. Padding does not fix that\. It silently substitutes a different, config\-order\-dependent question and answers that one instead\.

We take this as the paper’s central methodological finding\. Generalizing Definition[2\.3](https://arxiv.org/html/2608.10420#S2.Thmtheorem3)to heterogeneous domains is not a matter of elegance or coverage\. Applying the original, global definition to a heterogeneous benchmark by the most direct means available does not merely lose precision\. It produces a confident, wrong answer, and it produces a different wrong answer depending on an arbitrary choice, attribute list order, that carries no information about the rule under analysis\.

## 3Empirical Measurements: Structural Determinants of Pathology

[Section2](https://arxiv.org/html/2608.10420#S2)establishes the two competing readings of value symmetry used throughout this paper: Takemura et al\.’s global value symmetryAut​\(X\)\\mathrm\{Aut\}\(X\)\(Definition[2\.3](https://arxiv.org/html/2608.10420#S2.Thmtheorem3)\), a single permutation applied identically at every position, and the componentwise generalizationAut​\(ΦC\)\\mathrm\{Aut\}\(\\Phi\_\{C\}\)\(Definition[2\.5](https://arxiv.org/html/2608.10420#S2.Thmtheorem5)\) this paper argues for, in which every position chooses its own value permutation\.[Section2](https://arxiv.org/html/2608.10420#S2)also shows the two disagree in kind, not just in generality: on CLE4EVR’s real rule, forcing Definition[2\.3](https://arxiv.org/html/2608.10420#S2.Thmtheorem3)to apply by padding every attribute domain to a common size reports90\.91%90\.91\\%\(66\-dimensional\) to99\.07%99\.07\\%\(88\-dimensional\) spurious pairwise pathology \([Table1](https://arxiv.org/html/2608.10420#S2.T1)\), traced there to attribute\-list bookkeeping rather than rule structure, whereAut​\(ΦC\)\\mathrm\{Aut\}\(\\Phi\_\{C\}\)finds none\. This section asks the constructive question that finding leaves open: once the padding artifact is removed, how often doesAut​\(ΦC\)\\mathrm\{Aut\}\(\\Phi\_\{C\}\)\-orbit membership actually account for the alternative solutions inΦC\\Phi\_\{C\}, on real neurosymbolic rule sets? We extend Table[1](https://arxiv.org/html/2608.10420#S2.T1)to two further published benchmark families \([Section3\.2](https://arxiv.org/html/2608.10420#S3.SS2)\), stress\-test the resulting pattern on eight further rule families spanning 15 predictions fixed before measurement \([Section3\.3](https://arxiv.org/html/2608.10420#S3.SS3)\), and distill the result into a four\-mechanism characterization \([Section3\.4](https://arxiv.org/html/2608.10420#S3.SS4)\)\. Every reported number is machine\-computed; LaTeX comments cite the source JSON file and field in the project’s verification\-data directory\.

### 3\.1Setup and measurement protocol

#### The object of measurement\.

We useΦC\\Phi\_\{C\},∏i=1nSym​\(Si\)=∏i=1nSym​\(Si\)\\prod\_\{i=1\}^\{n\}\\mathrm\{Sym\}\(S\_\{i\}\)=\\prod\_\{i=1\}^\{n\}\\mathrm\{Sym\}\(S\_\{i\}\), andAut​\(ΦC\)\\mathrm\{Aut\}\(\\Phi\_\{C\}\)exactly as fixed in Definitions[2\.1](https://arxiv.org/html/2608.10420#S2.Thmtheorem1)and[2\.5](https://arxiv.org/html/2608.10420#S2.Thmtheorem5): every positioni∈Ni\\in Nkeeps its own local domainSiS\_\{i\}, and

Aut​\(ΦC\)=\{σ=\(σ1,…,σn\)∈∏i=1nSym​\(Si\):σ⋅φ∈ΦC​for all​φ∈ΦC\}≤∏i=1nSym​\(Si\)\\mathrm\{Aut\}\(\\Phi\_\{C\}\)\\;=\\;\\bigl\\\{\\,\\sigma=\(\\sigma\_\{1\},\\dots,\\sigma\_\{n\}\)\\in\\prod\_\{i=1\}^\{n\}\\mathrm\{Sym\}\(S\_\{i\}\)\\;:\\;\\sigma\\cdot\\varphi\\in\\Phi\_\{C\}\\text\{ for all \}\\varphi\\in\\Phi\_\{C\}\\,\\bigr\\\}\\;\\leq\\;\\prod\_\{i=1\}^\{n\}\\mathrm\{Sym\}\(S\_\{i\}\)is the coordinatewise value permutations that fixΦC\\Phi\_\{C\}setwise\. The padded diagonal extensionAutpad\\mathrm\{Aut\}\_\{\\mathrm\{pad\}\}of Definition[2\.3](https://arxiv.org/html/2608.10420#S2.Thmtheorem3)’s action \([Section2](https://arxiv.org/html/2608.10420#S2)’s notation and object, reused here\) reappears twice below, for BDD\-OIA/SDD\-OIA and for the Latin\-square/Sudoku family, where the two readings behave differently for reasons specific to those rules\.

Forφ,φ′∈ΦC\\varphi,\\varphi^\{\\prime\}\\in\\Phi\_\{C\}writeφ∼φ′\\varphi\\sim\\varphi^\{\\prime\}when they lie in the sameAut​\(ΦC\)\\mathrm\{Aut\}\(\\Phi\_\{C\}\)\-orbit\.[Section2](https://arxiv.org/html/2608.10420#S2)informally reports the fraction of unordered solution pairs not related by any automorphism as “pairwise%,” in the caption of[Table1](https://arxiv.org/html/2608.10420#S2.T1); we use it as the headline statistic throughout this paper and fix notation for it here,

ρ​\(ΦC\)=\|\{\{φ,φ′\}⊆ΦC:φ≠φ′,φ≁φ′\}\|\(\|ΦC\|2\)∈\[0,1\],\\rho\(\\Phi\_\{C\}\)\\;=\\;\\frac\{\\bigl\|\\\{\\\{\\varphi,\\varphi^\{\\prime\}\\\}\\subseteq\\Phi\_\{C\}:\\varphi\\neq\\varphi^\{\\prime\},\\ \\varphi\\not\\sim\\varphi^\{\\prime\}\\\}\\bigr\|\}\{\\binom\{\|\\Phi\_\{C\}\|\}\{2\}\}\\;\\in\\;\[0,1\],withρ=0\\rho=0exactly whenAut​\(ΦC\)\\mathrm\{Aut\}\(\\Phi\_\{C\}\)acts transitively onΦC\\Phi\_\{C\}\(a single orbit accounts for every solution pair\) andρ→1\\rho\\to 1when almost no pair of solutions is related by any automorphism\. A companion*existence*statistic,ρ∃​\(ΦC\)\\rho\_\{\\exists\}\(\\Phi\_\{C\}\), is the fraction ofφ∈ΦC\\varphi\\in\\Phi\_\{C\}with*some*orbit\-external partner elsewhere inΦC\\Phi\_\{C\}; because a single non\-trivial orbit already pullsρ∃\\rho\_\{\\exists\}close to11, it is close to a step function \(0 iff transitive, close to 1 otherwise\) and adds little beyond transitivity itself\. We report it only in passing and useρ\\rhoas the headline statistic throughout\.

#### Toolchain and cross\-validation\.

Automorphism groups and orbits are computed two ways\. For small instances,real\_data\_measurement\.pyenumerates∏i=1nSym​\(Si\)\\prod\_\{i=1\}^\{n\}\\mathrm\{Sym\}\(S\_\{i\}\)directly and tests setwise stabilization by brute force\. When∏i=1nSym​\(Si\)\\prod\_\{i=1\}^\{n\}\\mathrm\{Sym\}\(S\_\{i\}\)is too large to enumerate \(e\.g\.\(10\!\)2≈1\.3×1013\(10\!\)^\{2\}\\approx 1\.3\\times 10^\{13\}for two free MNIST digits\),empirical\_ext\_nauty\_indep\.pyreduces the independent\-coordinate automorphism problem to a colored\-graph automorphism problem solved withpynauty\[[16](https://arxiv.org/html/2608.10420#bib.bib16)\], giving each coordinate’s value domain its own color class\. The two engines were cross\-checked against each other on CLE4EVR \(\|Aut​\(ΦC\)\|=24\|\\mathrm\{Aut\}\(\\Phi\_\{C\}\)\|=24, one orbit\) and Kandinsky \(\|Aut​\(ΦC\)\|=36\|\\mathrm\{Aut\}\(\\Phi\_\{C\}\)\|=36, six orbits of sizes36,36,36,18,18,1836,36,36,18,18,18\): they agree not only on group order and orbit\-size multiset but on the exact partition ofΦC\\Phi\_\{C\}into orbits\. Group\-axiom checks \(closure under composition; every element’s inverse present\) and a second, independent orbit algorithm \(direct image\-set computation rather than union\-find\) were additionally run on the Kandinsky result, since it is this paper’s first non\-degenerate positive finding and the one result most exposed if the enumeration code itself had a bug\.

#### Label\-driven reformulation \(BDD\-OIA/SDD\-OIA\)\.

BDD\-OIA and SDD\-OIA share one decision function,sddoiaK, mapping 20 free binary concepts to 4 binary actions \([Section3\.2](https://arxiv.org/html/2608.10420#S3.SS2)\)\.[Section2](https://arxiv.org/html/2608.10420#S2)shows Definition[2\.3](https://arxiv.org/html/2608.10420#S2.Thmtheorem3)cannot even be posed here: with 20 heterogeneous binary detectors there is no shared value domainSS, so its bijective restrictionΦCbij\\Phi\_\{C\}^\{\\mathrm\{bij\}\}is empty andAut​\(X\)\\mathrm\{Aut\}\(X\)collapses to the full, uninformativeSym​\(S\)\\mathrm\{Sym\}\(S\)under the universally\-quantified\-over\-the\-empty\-set reading of that definition\. Definition[2\.5](https://arxiv.org/html/2608.10420#S2.Thmtheorem5)does not need a sharedSS, but it does need a fixed intended mappingφ∗\\varphi^\{\*\}to define shortcuts relative to, and BDD\-OIA/SDD\-OIA is naturally posed the other way around, as a decision rule that maps concepts to an observed action\. We therefore reformulate around a fixed*label*rather than a fixed mapping: for a reachable action vectory∗y^\{\*\}, define

Φy∗=\{c∈\{0,1\}20:sddoiaK​\(c\)=y∗\},\\Phi\_\{y^\{\*\}\}\\;=\\;\\bigl\\\{\\,c\\in\\\{0,1\\\}^\{20\}\\;:\\;\\texttt\{sddoiaK\}\(c\)=y^\{\*\}\\,\\bigr\\\},directly specializing Definition[2\.1](https://arxiv.org/html/2608.10420#S2.Thmtheorem1)’sΦC\\Phi\_\{C\}\(which never requires bijectivity\) to the single functional constraint “sddoiaK​\(⋅\)=y∗\\texttt\{sddoiaK\}\(\\cdot\)=y^\{\*\},” syntactically on the same footing as Takemura et al\.’s own arithmetic\-equality examples\.Aut​\(Φy∗\)\\mathrm\{Aut\}\(\\Phi\_\{y^\{\*\}\}\)is then defined exactly asAut​\(ΦC\)\\mathrm\{Aut\}\(\\Phi\_\{C\}\)above, under∏i=1nSym​\(Si\)=Sym​\(\{0,1\}\)20≅\(𝔽2\)20\\prod\_\{i=1\}^\{n\}\\mathrm\{Sym\}\(S\_\{i\}\)=\\mathrm\{Sym\}\(\\\{0,1\\\}\)^\{20\}\\cong\(\\mathbb\{F\}\_\{2\}\)^\{20\}\.

The reformulation is a direction\-dual of Takemura et al\.’s framework, and the two directions are worth setting side by side\. Definition[2\.1](https://arxiv.org/html/2608.10420#S2.Thmtheorem1)\(Takemura et al\.’s Definitions 3/4\) asks, for a fixed intended mappingφ∗\\varphi^\{\*\}, which*other*concept assignments satisfy the same constraints: shortcuts relative to a ground\-truth*mapping*\.Φy∗\\Phi\_\{y^\{\*\}\}asks, for a fixed observed*label*, which concept assignments produce it: shortcuts relative to a ground\-truth*label*\. Both are specializations of the same generalΦC=\{φ:N→S∣φ​satisfies​C\}\\Phi\_\{C\}=\\\{\\varphi:N\\to S\\mid\\varphi\\text\{ satisfies \}C\\\}, and the label\-driven direction is the one BDD\-OIA’s own structure poses, a decision rule mapping concepts to an observed action; it is also the direction under which rsbench’s flagship failure mode, the pedestrian confused for a red light, becomes a measurable orbit fact rather than an anecdote \([Section3\.2](https://arxiv.org/html/2608.10420#S3.SS2)\)\.

### 3\.2Three benchmark families

#### CLE4EVR\.

[Section2](https://arxiv.org/html/2608.10420#S2)already reports CLE4EVR in full \([Table1](https://arxiv.org/html/2608.10420#S2.T1)\): on rsbench’s real rule\[[7](https://arxiv.org/html/2608.10420#bib.bib7)\],Aut​\(ΦC\)\\mathrm\{Aut\}\(\\Phi\_\{C\}\)is fully transitive at both66dimensions \(\|ΦC\|=12\|\\Phi\_\{C\}\|=12,\|Aut​\(ΦC\)\|=24\|\\mathrm\{Aut\}\(\\Phi\_\{C\}\)\|=24\) and88dimensions \(\|ΦC\|=108\|\\Phi\_\{C\}\|=108,\|Aut​\(ΦC\)\|=864\|\\mathrm\{Aut\}\(\\Phi\_\{C\}\)\|=864\),ρ=0%\\rho=0\\%throughout, while the padded global reading reports90\.91%90\.91\\%–99\.07%99\.07\\%pathology traced to an arbitrary attribute\-list ordering rather than to the rule\. CLE4EVR is this paper’s cleanest transitive case, and the reference point the next two families are measured against\.

#### Kandinsky\.

All 6 symbols are constrained: three objects, each with a shape \(circle, square, or triangle\) and a color \(red, yellow, or blue\), under

\(c1=c2∧s1=s2∧s1≠s3\)∨\(c1=c3∧s1=s3∧s1≠s2\)∨\(c2=c3∧s2=s3∧s1≠s3\),\\bigl\(c\_\{1\}\{=\}c\_\{2\}\\wedge s\_\{1\}\{=\}s\_\{2\}\\wedge s\_\{1\}\{\\neq\}s\_\{3\}\\bigr\)\\;\\vee\\;\\bigl\(c\_\{1\}\{=\}c\_\{3\}\\wedge s\_\{1\}\{=\}s\_\{3\}\\wedge s\_\{1\}\{\\neq\}s\_\{2\}\\bigr\)\\;\\vee\\;\\bigl\(c\_\{2\}\{=\}c\_\{3\}\\wedge s\_\{2\}\{=\}s\_\{3\}\\wedge s\_\{1\}\{\\neq\}s\_\{3\}\\bigr\),writingci,sic\_\{i\},s\_\{i\}for objectii’s color and shape: exactly one pair of the three objects matches on both attributes while differing from the third\. Exhaustive enumeration gives\|ΦC\|=162\|\\Phi\_\{C\}\|=162\(3×543\\times 54, matching an independent hand combinatorial count of the three mutually exclusive disjuncts\),\|Aut​\(ΦC\)\|=36\|\\mathrm\{Aut\}\(\\Phi\_\{C\}\)\|=36, and*six*orbits of sizes36,36,36,18,18,1836,36,36,18,18,18:ρ=81\.99%\\rho=81\.99\\%\(10,692/13,04110\{,\}692/13\{,\}041pairs\)\. This is this paper’s first non\-degenerate positive result, and it is not a weak\-definition artifact: even under the independent\-coordinate group \(the more defensible reading of value symmetry argued for in[Section2](https://arxiv.org/html/2608.10420#S2)\),100%100\\%of candidate solutions have at least one orbit\-external shortcut\. The mechanism is structural\. Independent\-coordinate automorphisms relabel values*within*each object slot but never exchange which physical object plays which role, so a solution in which objects 1 and 2 match cannot be relabeled into one where objects 1 and 3 match: the disjunction’s three branches pick out three genuinely different position patterns that no per\-slot relabeling can merge\.[Section3\.3](https://arxiv.org/html/2608.10420#S3.SS3)sharpens this into a general branch\-exchange criterion\.

#### BDD\-OIA and SDD\-OIA\.

Both benchmarks sharesddoiaK, extracted directly from the rsbench source and independently reproducing rsbench’s own Table 28 worked example exactly\[[7](https://arxiv.org/html/2608.10420#bib.bib7)\]\.[Section2](https://arxiv.org/html/2608.10420#S2)already establishes thatsddoiaKtakes exactly 20 free boolean parameters, not 21, since the 21st tabulated concept,clear, is identically¬\(car∨person∨rider∨other\_obstacle\)\\neg\(\\texttt\{car\}\\vee\\texttt\{person\}\\vee\\texttt\{rider\}\\vee\\texttt\{other\\\_obstacle\}\), double\-locked there byinspect\.signatureon the live function and by an exhaustive2202^\{20\}check, and independently corroborated by rsbench’s own text\[[7](https://arxiv.org/html/2608.10420#bib.bib7)\]\. Completing the measurement needs one further structural fact[Section2](https://arxiv.org/html/2608.10420#S2)does not use:move\_forwardis symbolically*identical*to¬stop\\neg\\texttt\{stop\}\(proved by an UNSAT check over all2202^\{20\}assignments, then independently reconfirmed by full brute\-force enumeration of the same2202^\{20\}points\), cutting the 16 syntactically possible \(stop, move\-forward, turn\-left, turn\-right\) combinations to the 8 that are actually reachable\. The 20 free variables factor into three disjoint blocks \(front\-8, left\-6, right\-6\) governing \(stop/move\-forward\), turn\-left, and turn\-right respectively\. Exhaustive per\-block stabilizer search \(768 candidates checked, not sampled\) givesAut​\(Φy∗\)\\mathrm\{Aut\}\(\\Phi\_\{y^\{\*\}\}\)exactly for all 8 reachable labels, independently reconfirmed by3,000/3,0003\{,\}000/3\{,\}000random cross\-block masks tested directly against the full2202^\{20\}indicator array without relying on the block\-factorization assumption\.[Table2](https://arxiv.org/html/2608.10420#S3.T2)reports all eight\.

Instance\|Φ\|\|\\Phi\|\|Aut\|\|\\mathrm\{Aut\}\|orbitsmax orbitpairwiseρ\\rhotransitiveCLE4EVR \(6\-dim\)12241120\.00%yesKandinsky1623663681\.99%noBDD\-OIA/SDD\-OIA: label\-drivenΦy∗\\Phi\_\{y^\{\*\}\},y∗=y^\{\*\}=\(stop, fwd, left, right\)\(1,0,0,0\)\(1,0,0,0\)812,2502406,125299\.9999%no\(1,0,0,1\)\(1,0,0,1\)99,750249,875299\.9990%no\(1,0,1,0\)\(1,0,1,0\)99,750249,875299\.9990%no\(1,0,1,1\)\(1,0,1,1\)12,25026,125299\.9918%no\(0,1,0,0\)\(0,1,0,0\)19,49429,747299\.9949%no\(0,1,0,1\)\(0,1,0,1\)2,39421,197299\.9582%no\(0,1,1,0\)\(0,1,1,0\)2,39421,197299\.9582%no\(0,1,1,1\)\(0,1,1,1\)2942147299\.6587%noTable 2:Three benchmark families underAut​\(ΦC\)\\mathrm\{Aut\}\(\\Phi\_\{C\}\), extending Table[1](https://arxiv.org/html/2608.10420#S2.T1); the CLE4EVR row repeats that table’s 6\-dimensional measurement for comparison\. BDD\-OIA/SDD\-OIA figures are shown to four decimal places because every value lies within0\.350\.35percentage points of100%100\\%; two decimals would flatten all eight rows to100\.00%100\.00\\%\.[Table2](https://arxiv.org/html/2608.10420#S3.T2)’s dominant finding is that\|Aut​\(Φy∗\)\|=2\|\\mathrm\{Aut\}\(\\Phi\_\{y^\{\*\}\}\)\|=2on*every*reachable label, and this constant is driven by a single coordinate\. One consequence should be read off before the percentages are: for Boolean instances the group acts freely, so every orbit has size exactly\|Aut\|\|\\mathrm\{Aut\}\|andρ=1−\(\|Aut\|−1\)/\(\|Φ\|−1\)\\rho=1\-\(\|\\mathrm\{Aut\}\|\-1\)/\(\|\\Phi\|\-1\)is an exact law, proved as[Proposition5\.12](https://arxiv.org/html/2608.10420#S5.Thmtheorem12); every BDD\-OIA/SDD\-OIA row of the table \(orbit count, maximum orbit, and each percentage\) is that law evaluated at its\(\|Φ\|,\|Aut\|\)\(\|\\Phi\|,\|\\mathrm\{Aut\}\|\)pair\. The nines are a corollary of the group order and the solution count, which is why the table reports\|Aut\|\|\\mathrm\{Aut\}\|, the orbit count, and the maximum orbit size alongsideρ\\rho, and why the informative claim in these rows is\|Aut\|=2\|\\mathrm\{Aut\}\|=2itself, not the percentage\.followis more subtle than CLE4EVR’s free size coordinates: it is not syntactically absent from the rule\. It appears explicitly in the unsimplified formulamove\_forward\_cond=Or​\(green\_light,follow,road\_clear\)\\texttt\{move\\\_forward\\\_cond\}=\\mathrm\{Or\}\(\\texttt\{green\\\_light\},\\texttt\{follow\},\\texttt\{road\\\_clear\}\), but oncestop=False\\texttt\{stop\}=\\mathrm\{False\}forcesroad\_clear=True\\texttt\{road\\\_clear\}=\\mathrm\{True\}, Boolean absorption erases its contribution\. This fact needed symbolic proof to surface, not inspection of the rule text\. This is a second, independent trigger of the same dead\-coordinate pathology already documented for CLE4EVR’ssize\_1/size\_2\(syntactic absence there; semantic absorption here\), an instance of a phenomenon long known in the classical CSP symmetry\-breaking literature: variables the constraints never really pin down contribute spurious automorphisms\[[10](https://arxiv.org/html/2608.10420#bib.bib10)\]\.

Because flippingfollowis a fixed\-point\-free involution,\|Φy∗\|\|\\Phi\_\{y^\{\*\}\}\|is even wheneverΦy∗≠∅\\Phi\_\{y^\{\*\}\}\\neq\\varnothing, soSM​\(y∗\)=\|Φy∗\|−1≥1\\mathrm\{SM\}\(y^\{\*\}\)=\|\\Phi\_\{y^\{\*\}\}\|\-1\\geq 1for every one of the 8 reachable labels: under Definition[2\.1](https://arxiv.org/html/2608.10420#S2.Thmtheorem1), this decision logic cannot be shortcut\-free for*any*label a real vehicle can reach\. The diagonal shared\-value extension of Definition[2\.3](https://arxiv.org/html/2608.10420#S2.Thmtheorem3)’s action \(one global bit\-flip applied to all 20 positions at once; the literal definition again has no bijective solutions to act on, since\|N\|=20\|N\|=20against\|S\|=2\|S\|=2\) does*worse*here than padding does on CLE4EVR\. Tested on the two most extreme labels, it preserves neither level set:Autpad​\(Φy∗\)\\mathrm\{Aut\}\_\{\\mathrm\{pad\}\}\(\\Phi\_\{y^\{\*\}\}\)collapses to the trivial group exactly where the independent\-coordinate reading still finds the genuine order\-2 symmetry\. rsbench’s own named example \(a model that cannot tell a pedestrian from a red light, since both correctly imply the*stop*action\[[7](https://arxiv.org/html/2608.10420#bib.bib7)\]\) is a direct instance of the unexplained99\.9999%99\.9999\\%: the all\-personand all\-red\_lightconcept vectors both map toy∗=\(1,0,0,0\)y^\{\*\}=\(1,0,0,0\), but they differ in two coordinates, not the one \(follow\) thatAut​\(Φ\(1,0,0,0\)\)\\mathrm\{Aut\}\(\\Phi\_\{\(1,0,0,0\)\}\)can flip, so they lie in different orbits\.

The quantity measured in all 8 BDD\-OIA/SDD\-OIA rows is fixed precisely:Φy∗\\Phi\_\{y^\{\*\}\}is the preimage ofy∗y^\{\*\}undersddoiaKover the full\{0,1\}20\\\{0,1\\\}^\{20\}hypercube, the object the rule itself defines, independent of any sampling distribution\.[Table2](https://arxiv.org/html/2608.10420#S3.T2)’s figures are therefore the rule’s combinatorial shortcut multiplicity; weighting by rsbench’s rendering distribution, which never samples physically contradictory concept vectors such as simultaneous red and green lights\[[7](https://arxiv.org/html/2608.10420#bib.bib7)\], would measure a different, distribution\-relative quantity, and the two should not be conflated in either direction\.

Across all three families the headline ranges over0%0\\%,81\.99%81\.99\\%, and99\.6699\.66–99\.9999%99\.9999\\%: not uniformly high, not uniformly low\. CLE4EVR’s conjunction of independent equality constraints is exactly transitive; Kandinsky’s and BDD\-OIA/SDD\-OIA’s disjunctive decision structure is not\.[Section3\.3](https://arxiv.org/html/2608.10420#S3.SS3)tests whether this pattern, and not just its two positive instances, generalizes\.

### 3\.3Eight further rule families, under pre\-specified predictions

Three benchmark families are not enough to tell a real structural pattern from a coincidence built on two hand\-picked disjunctive examples\. This section extends the measurement to eight further rule families, seven independent sources, and 15 separately pre\-specified structure\-to\-pathology predictions\.

#### Prediction discipline\.

Each family’s structural classification and predicted outcome were written into that family’s measurement script as a comment block*before*the script was executed\. We report the mechanism precisely so the reader can weigh it for themselves: each prediction sits in its measurement script’s docstring, recorded before the script was first executed, which is what separates an ex\-ante prediction from a post\-hoc rationalization of whatever the measurement returned\.

#### Sources and toolchain\.

Seven sources feed the eight families of[Table3](https://arxiv.org/html/2608.10420#S3.T3): \(i\) Takemura et al\.’s own Example 2\[[26](https://arxiv.org/html/2608.10420#bib.bib26)\]\(MNIST\-Half\), the one further fully worked example in their paper, with zero reconstruction uncertainty; \(ii\)–\(iv\) three furtherget\_labelrules in rsbench’s own MNIST\-addition source\[[7](https://arxiv.org/html/2608.10420#bib.bib7)\]\(sum, tracing to DeepProbLog’s MNIST\-addition task\[[14](https://arxiv.org/html/2608.10420#bib.bib14)\];product; and a previously untested third branch,multiop\), plus a same\-family structural analogue restricted to even digits \(MNAdd\-EvenOdd\); \(v\) an ensemble of 36 randomll\-CNF instances built from rsbench’s own MNLogic recipe \(own generator, not a byte\-exact port\); \(vi\) order\-3 Latin squares and order\-4 mini\-Sudoku, a public combinatorial rule outside rsbench; \(vii\) CLEVR\-Hans3\[[25](https://arxiv.org/html/2608.10420#bib.bib25)\], ground\-truth class rules fetched verbatim from the releasedClevr\_Hans\_GTClasses\_3\.json, a second source outside rsbench\. All are measured with the same two engines as[Section3\.1](https://arxiv.org/html/2608.10420#S3.SS1), plus the nauty\-based scalable engine for the largest domains \(e\.g\. two free MNIST digits over\{0,…,9\}\\\{0,\\dots,9\\\},\(10\!\)2≈1\.3×1013\(10\!\)^\{2\}\\approx 1\.3\\times 10^\{13\}\), which is the same engine already cross\-validated at the orbit level against the brute\-force results on CLE4EVR and Kandinsky\.

[Table3](https://arxiv.org/html/2608.10420#S3.T3)reports all eight families\. Family\-level rows aggregate a variable number of individually pre\-specified sub\-predictions \(17 summed target sums for MNAdd\-sum, 3 template classes for CLEVR\-Hans3, and so on\); the total across all eight rows is 15 pre\-specified units of varying granularity, of which13 \(86\.7%\) were confirmed\.

Table 3:Eight further rule families\. Structural class and prediction were fixed in each measurement script before execution\. 13/15 pre\-specified units confirmed; both misses are CLEVR\-Hans3, discussed below\.
#### The two misses: the branch\-exchangeability criterion\.

Both misses are CLEVR\-Hans3 classes predicted non\-transitive, by direct analogy with Kandinsky’s disjunctive slot\-matching, that measured fully transitive instead: class 0 \(\|Φ\|=512\|\\Phi\|=512\) and class 2 \(\|Φ\|=8\|\\Phi\|=8\), bothρ=0%\\rho=0\\%\. Each class rule is a disjunction over which of two generic object slots matches which of two attribute templates\. Class 0’s templates differ only in shape \(cubevs\.cylinder\), with size tied to the same value \(large\) in both and material/color free in both; class 2’s templates differ in size and color together \(large\+bluevs\.small\+yellow\), with shape \(sphere\) fixed in both\. In both cases, swapping the two templates leaves the constraint syntactically unchanged, so there is a coordinatewise permutation \(flip the discriminating attribute values in lockstep\) that exchanges the two disjuncts and merges them into one orbit\. Class 1 is different: it pinsmaterial=metalin one template and leaves material entirely free in the other, an asymmetric pinning that no per\-slot value permutation can exchange, and it measures non\-transitive as originally predicted \(ρ=75\.29%\\rho=75\.29\\%\)\. This sharpens Kandinsky’s and MNLogic’s “disjunction→\\topathology” pattern into a precise, checkable condition: transitivity underAut​\(ΦC\)\\mathrm\{Aut\}\(\\Phi\_\{C\}\)depends on whether a disjunction’s branches admit a coordinatewise permutation exchanging them, not on whether the rule is syntactically a disjunction at all\.

#### A conjunction exception: multiplicative zero\.

MNAdd\-product’s 32 reachable target products are 31/32 transitive, matching the “mild conjunction→\\totransitive” pattern, except aty=0y=0\(\|Φ\|=19\|\\Phi\|=19, every pair withc1=0c\_\{1\}\{=\}0orc2=0c\_\{2\}\{=\}0\), which is57\.89%57\.89\\%non\-transitive\. Zero is a multiplicative absorbing element: exactly three orbits result, of sizes 9, 9, and 1:\{\(0,0\)\}\\\{\(0,0\)\\\},\{\(0,k\):k≠0\}\\\{\(0,k\):k\\neq 0\\\}, and\{\(k,0\):k≠0\}\\\{\(k,0\):k\\neq 0\\\}\. Any automorphism fixing the doubly\-zero solution\(0,0\)\(0,0\)cannot also merge the two single\-zero families, since that would require one coordinate’s permutation to send0to a non\-zero value while a bijection has already fixed that coordinate at0\. This is the cleanest counterexample yet to “conjunction⇒\\Rightarrowtransitive”: a single arithmetic equality, syntactically as mild as MNAdd\-sum’s, made pathological by one exceptional value\.

#### A third, independent mechanism: the counting bound\.

Latin squares and mini\-Sudoku are all\-different constraints – syntactically a large conjunction of pairwise inequalities, closer to CLE4EVR’s side of the divide than to Kandinsky’s – yet all three instances tested are strongly non\-transitive:54\.55%54\.55\\%\(order\-3 Latin square,\|Φ\|=12\|\\Phi\|=12\),91\.99%91\.99\\%\(order\-4 Sudoku,\|Φ\|=288\|\\Phi\|=288\),96\.00%96\.00\\%\(order\-4 Latin square, no boxes,\|Φ\|=576\|\\Phi\|=576\)\. The mechanism is pure pigeonhole, recorded before running any code: an orbit has size at most\|Aut\|\|\\mathrm\{Aut\}\|, and\|Φ\|\|\\Phi\|\(1212,288288,576576, literature\-known counts\) exceeds the diagonal cap \(3\!=63\!\{=\}6or4\!=244\!\{=\}24\) in every case, so a transitive action is numerically impossible, independent of any conjunction/disjunction argument\. The recorded argument took the diagonal cap for granted, and under Definition[2\.5](https://arxiv.org/html/2608.10420#S2.Thmtheorem5)it is not free: the ambient componentwise group of even a3×33\\times 3grid has order696^\{9\}, so the cap has to be earned\. Lemma[4\.10](https://arxiv.org/html/2608.10420#S4.Thmtheorem10)earns it by a forcing argument \(pair\-rich all\-different lines admit only diagonal automorphisms\), and the exact groups land on the cap’s structure precisely: every element diagonal,\|Aut​\(ΦC\)\|=6\|\\mathrm\{Aut\}\(\\Phi\_\{C\}\)\|=6,2424,2424\. One nuance: because every cell of a grid draws from the same alphabet, the diagonal shared\-value extensionAutpad\\mathrm\{Aut\}\_\{\\mathrm\{pad\}\}\([Section2](https://arxiv.org/html/2608.10420#S2)\) is arguably the more natural symmetry concept for this family, notAut​\(ΦC\)\\mathrm\{Aut\}\(\\Phi\_\{C\}\)\. We verified computationally that the two coincide numerically on all three instances \(\|Aut​\(ΦC\)\|=\|Autpad\|=6,24,24\|\\mathrm\{Aut\}\(\\Phi\_\{C\}\)\|=\|\\mathrm\{Aut\}\_\{\\mathrm\{pad\}\}\|=6,24,24respectively, each computed independently rather than copied\), so the pigeonhole conclusion holds under either reading;[Table3](https://arxiv.org/html/2608.10420#S3.T3)reports theAut​\(ΦC\)\\mathrm\{Aut\}\(\\Phi\_\{C\}\)figures for consistency with the rest of this paper\.

Combined with[Section3\.2](https://arxiv.org/html/2608.10420#S3.SS2), 15 pre\-specified predictions across 8 families and 3 independent benchmark families give the clearest evidence so far that pathology underAut​\(ΦC\)\\mathrm\{Aut\}\(\\Phi\_\{C\}\)tracks specific, checkable structural properties of a rule, not a crude conjunction/disjunction label\.

### 3\.4The four\-mechanism characterization

The coarse pattern from[Section3\.2](https://arxiv.org/html/2608.10420#S3.SS2)\(conjunction is safe, disjunction is not\) does not survive[Section3\.3](https://arxiv.org/html/2608.10420#S3.SS3)intact: it is directionally right \(13/1513/15\) but wrong in exactly the two ways that matter most for a mechanistic account\.[Table4](https://arxiv.org/html/2608.10420#S3.T4)replaces it with four mechanisms, each tied to specific instances measured above\.

Table 4:Four\-mechanism characterization of transitivity underAut​\(ΦC\)\\mathrm\{Aut\}\(\\Phi\_\{C\}\), replacing the coarse conjunction/disjunction split\.NNcounts individual rule/label instances already reported in[Tables2](https://arxiv.org/html/2608.10420#S3.T2)and[3](https://arxiv.org/html/2608.10420#S3.T3)\.Mechanisms 1 and 3 recover the coarse pattern in the regime where it holds; mechanism 2 shows conjunction is not automatically safe \(one exceptional value is enough\); mechanism 4 shows non\-transitivity can be forced by counting alone, with no reference to conjunction or disjunction\. An all\-different constraint is, syntactically, exactly the kind of mild conjunction mechanism 1 predicts should be transitive, and it is not, for a reason that has nothing to do with mechanism 1’s failure mode\.

The four mechanisms are an empirical characterization with an 8\-family, 15\-prediction basis, and[Section4](https://arxiv.org/html/2608.10420#S4)then proves each at the level it admits: mechanism 1 becomes the matching\-decomposition condition \([Theorem4\.3](https://arxiv.org/html/2608.10420#S4.Thmtheorem3)\), mechanism 2 the degree invariant \([Theorem4\.8](https://arxiv.org/html/2608.10420#S4.Thmtheorem8)\), mechanism 3’s symmetric half the branch\-swapping condition \([Theorem4\.4](https://arxiv.org/html/2608.10420#S4.Thmtheorem4)\) and its Kandinsky\-type residual the Free Slot Lemma \([Theorem4\.11](https://arxiv.org/html/2608.10420#S4.Thmtheorem11)\), and mechanism 4 the orbit\-stabilizer bound \([Theorem4\.9](https://arxiv.org/html/2608.10420#S4.Thmtheorem9)\);[Theorem4\.6](https://arxiv.org/html/2608.10420#S4.Thmtheorem6)additionally exhibits purely conjunctive counterexamples showing mechanism 2 cannot be removed by any syntactic strengthening of mechanism 1\.[Section4\.7](https://arxiv.org/html/2608.10420#S4.SS7)tabulates this correspondence and its coverage boundary\. The one mechanism[Section4](https://arxiv.org/html/2608.10420#S4)leaves as an empirical criterion rather than a closed\-form test is branch \(a\)symmetry \(mechanism 3\) for disjunctions with more than two branches of unequal syntactic shape; Kandinsky’s three\-way disjunction and CLEVR\-Hans3’s two\-way disjunctions anchor it, and[Section3\.3](https://arxiv.org/html/2608.10420#S3.SS3)’s 8 families are its current basis\.

## 4Algebraic Characterization

Section[2](https://arxiv.org/html/2608.10420#S2)defined componentwise value symmetryAut​\(ΦC\)\\mathrm\{Aut\}\(\\Phi\_\{C\}\)\([Definition2\.5](https://arxiv.org/html/2608.10420#S2.Thmtheorem5)\), and[Section3](https://arxiv.org/html/2608.10420#S3)measured its action onΦC\\Phi\_\{C\}across real rule families: sometimes transitive, sometimes not, with both outcomes traceable to specific features of the constraint set rather than to whether the constraint is written as a conjunction or a disjunction\. This section makes that dependence precise\. We give six results, each a sufficient condition on the syntactic shape ofCCfor transitivity or for its failure, built on a single forcing technique that also clarifies what value symmetry can and cannot see\. The results are sufficient conditions, not a classification, and we say so precisely: Section[4\.7](https://arxiv.org/html/2608.10420#S4.SS7)states exactly which of the four empirical mechanisms from[Section3](https://arxiv.org/html/2608.10420#S3)each theorem covers, and which real instance resists all six\.

### 4\.1Setup

Fix an instanceX=\(N,S,C\)X=\(N,S,C\)in the sense of[Definition2\.1](https://arxiv.org/html/2608.10420#S2.Thmtheorem1), with solution setΦC⊆∏i∈NSi\\Phi\_\{C\}\\subseteq\\prod\_\{i\\in N\}S\_\{i\}\. WriteG:=∏i=1nSym​\(Si\)G:=\\prod\_\{i=1\}^\{n\}\\mathrm\{Sym\}\(S\_\{i\}\)for the ambient group andAut​\(ΦC\)≤G\\mathrm\{Aut\}\(\\Phi\_\{C\}\)\\leq Gfor its componentwise automorphism group \([Definition2\.5](https://arxiv.org/html/2608.10420#S2.Thmtheorem5)\), acting on∏i∈NSi\\prod\_\{i\\in N\}S\_\{i\}coordinatewise by\(σ⋅ϕ\)i=σi​\(ϕi\)\(\\sigma\\cdot\\phi\)\_\{i\}=\\sigma\_\{i\}\(\\phi\_\{i\}\)\. SinceAut​\(ΦC\)\\mathrm\{Aut\}\(\\Phi\_\{C\}\)stabilizesΦC\\Phi\_\{C\}as a set, it restricts to an action ofAut​\(ΦC\)\\mathrm\{Aut\}\(\\Phi\_\{C\}\)onΦC\\Phi\_\{C\}itself\. This section asks when that restricted action is*transitive*: a single orbit, so every two solutions are related by some element ofAut​\(ΦC\)\\mathrm\{Aut\}\(\\Phi\_\{C\}\)\.

The pair\(G,ΦC\)\(G,\\Phi\_\{C\}\)is the direct generalization, to arbitrary finite local domains, of the*autotopism group*of a Latin square or quasigroup in design theory, whereΦC\\Phi\_\{C\}is the set of triples satisfying a Latin condition andGGis a product of row, column, and symbol permutation groups;[Section7](https://arxiv.org/html/2608.10420#S7)discusses that connection\. In the Boolean caseSi≡\{0,1\}S\_\{i\}\\equiv\\\{0,1\\\},[2\.8](https://arxiv.org/html/2608.10420#S2.Thmtheorem8)already showedAut​\(ΦC\)\\mathrm\{Aut\}\(\\Phi\_\{C\}\)is always an𝔽2\\mathbb\{F\}\_\{2\}\-linear subspace of𝔽2n\\mathbb\{F\}\_\{2\}^\{n\};[Section5](https://arxiv.org/html/2608.10420#S5)develops that special structure\. The results below make no assumption on\|Si\|\|S\_\{i\}\|and use only the group action itself\.

### 4\.2The Forcing Lemma

Every intransitivity result in this section traces back to one observation: a sufficiently rigid two\-coordinate projection ofΦC\\Phi\_\{C\}forces the corresponding two coordinates of every automorphism to agree\.

###### Lemma 4\.1\(Forcing\)\.

LetX=\(N,S,C\)X=\(N,S,C\)be an instance in the sense of[Definition2\.1](https://arxiv.org/html/2608.10420#S2.Thmtheorem1)and leti,j∈Ni,j\\in NsatisfySi=Sj=:DS\_\{i\}=S\_\{j\}=:D\. Writeπi​j​\(ϕ\):=\(ϕi,ϕj\)\\pi\_\{ij\}\(\\phi\):=\(\\phi\_\{i\},\\phi\_\{j\}\)for the projection∏k∈NSk→D×D\\prod\_\{k\\in N\}S\_\{k\}\\to D\\times DandΔD:=\{\(d,d\):d∈D\}\\Delta\_\{D\}:=\\\{\(d,d\):d\\in D\\\}for the diagonal\. If

πi​j​\(ΦC\)=ΔDorπi​j​\(ΦC\)=D×D∖ΔD,\\pi\_\{ij\}\(\\Phi\_\{C\}\)=\\Delta\_\{D\}\\qquad\\text\{or\}\\qquad\\pi\_\{ij\}\(\\Phi\_\{C\}\)=D\\times D\\setminus\\Delta\_\{D\},then everyσ=\(σ1,…,σn\)∈Aut​\(ΦC\)\\sigma=\(\\sigma\_\{1\},\\dots,\\sigma\_\{n\}\)\\in\\mathrm\{Aut\}\(\\Phi\_\{C\}\)satisfiesσi=σj\\sigma\_\{i\}=\\sigma\_\{j\}\.

###### Proof\.

Projection commutes with the coordinatewise action: for everyϕ∈ΦC\\phi\\in\\Phi\_\{C\},πi​j​\(σ⋅ϕ\)=\(σi​\(ϕi\),σj​\(ϕj\)\)\\pi\_\{ij\}\(\\sigma\\cdot\\phi\)=\(\\sigma\_\{i\}\(\\phi\_\{i\}\),\\sigma\_\{j\}\(\\phi\_\{j\}\)\)\. Sinceσ∈Aut​\(ΦC\)\\sigma\\in\\mathrm\{Aut\}\(\\Phi\_\{C\}\)mapsΦC\\Phi\_\{C\}onto itself, the pair\(σi,σj\)\(\\sigma\_\{i\},\\sigma\_\{j\}\)mapsπi​j​\(ΦC\)\\pi\_\{ij\}\(\\Phi\_\{C\}\)onto itself\.

Supposeπi​j​\(ΦC\)=ΔD\\pi\_\{ij\}\(\\Phi\_\{C\}\)=\\Delta\_\{D\}\. Fixd∈Dd\\in D; sinceΔD\\Delta\_\{D\}contains\(d,d\)\(d,d\), so doesπi​j​\(ΦC\)\\pi\_\{ij\}\(\\Phi\_\{C\}\), so\(σi​\(d\),σj​\(d\)\)=\(σi,σj\)⋅\(d,d\)∈ΔD\(\\sigma\_\{i\}\(d\),\\sigma\_\{j\}\(d\)\)=\(\\sigma\_\{i\},\\sigma\_\{j\}\)\\cdot\(d,d\)\\in\\Delta\_\{D\}, givingσi​\(d\)=σj​\(d\)\\sigma\_\{i\}\(d\)=\\sigma\_\{j\}\(d\)\. Asddwas arbitrary,σi=σj\\sigma\_\{i\}=\\sigma\_\{j\}\.

Suppose insteadπi​j​\(ΦC\)=D×D∖ΔD\\pi\_\{ij\}\(\\Phi\_\{C\}\)=D\\times D\\setminus\\Delta\_\{D\}\. Fixd∈Dd\\in Dand letd′d^\{\\prime\}range overD∖\{d\}D\\setminus\\\{d\\\}\. Each\(d,d′\)\(d,d^\{\\prime\}\)lies inπi​j​\(ΦC\)\\pi\_\{ij\}\(\\Phi\_\{C\}\), so\(σi​\(d\),σj​\(d′\)\)∉ΔD\(\\sigma\_\{i\}\(d\),\\sigma\_\{j\}\(d^\{\\prime\}\)\)\\notin\\Delta\_\{D\}, that isσi​\(d\)≠σj​\(d′\)\\sigma\_\{i\}\(d\)\\neq\\sigma\_\{j\}\(d^\{\\prime\}\)for everyd′≠dd^\{\\prime\}\\neq d\. Sinceσj\\sigma\_\{j\}is a bijection ofDD, this forcesσi​\(d\)=σj​\(d\)\\sigma\_\{i\}\(d\)=\\sigma\_\{j\}\(d\): it is the one value ofDDthatσi​\(d\)\\sigma\_\{i\}\(d\)is not excluded from\. Asddwas arbitrary,σi=σj\\sigma\_\{i\}=\\sigma\_\{j\}\. ∎

The lemma says nothing about whetherAut​\(ΦC\)\\mathrm\{Aut\}\(\\Phi\_\{C\}\)is transitive; it only pins down a relationship between two coordinates of every automorphism, whether or not one exists\. Theorem[4\.6](https://arxiv.org/html/2608.10420#S4.Thmtheorem6)and Theorem[4\.11](https://arxiv.org/html/2608.10420#S4.Thmtheorem11)both build intransitivity results on top of this forced relationship, and the proof of Theorem[4\.3](https://arxiv.org/html/2608.10420#S4.Thmtheorem3)uses the same commuting\-projection identity to establish the opposite conclusion on a different family of instances\.

### 4\.3Sufficient conditions for transitivity

The first two results identify constraint shapes under whichAut​\(ΦC\)\\mathrm\{Aut\}\(\\Phi\_\{C\}\)is guaranteed to act transitively onΦC\\Phi\_\{C\}\.

###### Definition 4\.2\(Matching decomposition\)\.

A partitionN=N1⊔⋯⊔Nr⊔FN=N\_\{1\}\\sqcup\\cdots\\sqcup N\_\{r\}\\sqcup Fis a*matching decomposition*ofΦC\\Phi\_\{C\}if, for each blockNl=\{il,1,…,il,ml\}N\_\{l\}=\\\{i\_\{l,1\},\\dots,i\_\{l,m\_\{l\}\}\\\}, there is a nonempty setTl⊆Sil,1T\_\{l\}\\subseteq S\_\{i\_\{l,1\}\}and injectionsfl,j:Tl→Sil,jf\_\{l,j\}:T\_\{l\}\\to S\_\{i\_\{l,j\}\}forj=2,…,mlj=2,\\dots,m\_\{l\}\(withfl,1:=idTlf\_\{l,1\}:=\\mathrm\{id\}\_\{T\_\{l\}\}\), such that

ΦC=∏l=1rΨl×∏i∈FSi,Ψl:=\{\(fl,1​\(t\),…,fl,ml​\(t\)\):t∈Tl\}⊆∏j=1mlSil,j\.\\Phi\_\{C\}\\;=\\;\\prod\_\{l=1\}^\{r\}\\Psi\_\{l\}\\;\\times\\;\\prod\_\{i\\in F\}S\_\{i\},\\qquad\\Psi\_\{l\}:=\\big\\\{\(f\_\{l,1\}\(t\),\\dots,f\_\{l,m\_\{l\}\}\(t\)\):t\\in T\_\{l\}\\big\\\}\\subseteq\\textstyle\\prod\_\{j=1\}^\{m\_\{l\}\}S\_\{i\_\{l,j\}\}\.

Each block is parametrized by a single valuet∈Tlt\\in T\_\{l\}that determines every coordinate in the block through the injectionsfl,jf\_\{l,j\}; blocks and free positionsFFcombine freely\. Taking everyfl,jf\_\{l,j\}to be an identity map on a shared domain recovers “all positions in the block are equal,” the pattern behind CLE4EVR’s three matching\-attribute constraints; takingfl,j​\(t\)=k−tf\_\{l,j\}\(t\)=k\-tor another arithmetic bijection recovers a sum or difference constraint such as MNIST\-Half’s four summation equalities, chained across a tree of positions by composing the bijections along the tree\.

###### Theorem 4\.3\(Matching decomposition, Theorem A\)\.

IfN=N1⊔⋯⊔Nr⊔FN=N\_\{1\}\\sqcup\\cdots\\sqcup N\_\{r\}\\sqcup Fis a matching decomposition ofΦC\\Phi\_\{C\}, thenAut​\(ΦC\)\\mathrm\{Aut\}\(\\Phi\_\{C\}\)acts transitively onΦC\\Phi\_\{C\}\.

###### Proof\.

Fix a blockNlN\_\{l\}andα∈Sym​\(Tl\)\\alpha\\in\\mathrm\{Sym\}\(T\_\{l\}\)\. Defineσ\(l\)​\(α\)=\(σ1,…,σn\)∈G\\sigma^\{\(l\)\}\(\\alpha\)=\(\\sigma\_\{1\},\\dots,\\sigma\_\{n\}\)\\in Gby:σil,1\\sigma\_\{i\_\{l,1\}\}extendsα\\alphaby the identity onSil,1∖TlS\_\{i\_\{l,1\}\}\\setminus T\_\{l\};σil,j\\sigma\_\{i\_\{l,j\}\}forj≥2j\\geq 2extendsfl,j∘α∘fl,j−1f\_\{l,j\}\\circ\\alpha\\circ f\_\{l,j\}^\{\-1\}, a permutation offl,j​\(Tl\)f\_\{l,j\}\(T\_\{l\}\), by the identity onSil,j∖fl,j​\(Tl\)S\_\{i\_\{l,j\}\}\\setminus f\_\{l,j\}\(T\_\{l\}\); every coordinate outsideNlN\_\{l\}is the identity\. Composing two such maps composes the underlying permutations ofTlT\_\{l\}coordinatewise, soα↦σ\(l\)​\(α\)\\alpha\\mapsto\\sigma^\{\(l\)\}\(\\alpha\)is a group homomorphismSym​\(Tl\)→G\\mathrm\{Sym\}\(T\_\{l\}\)\\to G, injective becauseσ\(l\)​\(α\)\\sigma^\{\(l\)\}\(\\alpha\)determinesα\\alphaonil,1i\_\{l,1\}; writeGl≤GG\_\{l\}\\leq Gfor its image\.

GlG\_\{l\}stabilizesΦC\\Phi\_\{C\}:σ\(l\)​\(α\)\\sigma^\{\(l\)\}\(\\alpha\)is the identity outsideNlN\_\{l\}, so it suffices to check it mapsΨl\\Psi\_\{l\}onto itself\. Fort∈Tlt\\in T\_\{l\}, the point\(fl,1​\(t\),…,fl,ml​\(t\)\)∈Ψl\(f\_\{l,1\}\(t\),\\dots,f\_\{l,m\_\{l\}\}\(t\)\)\\in\\Psi\_\{l\}maps to\(α​\(t\),fl,2​\(α​\(fl,2−1​\(fl,2​\(t\)\)\)\),…\)=\(α​\(t\),fl,2​\(α​\(t\)\),…,fl,ml​\(α​\(t\)\)\)\\big\(\\alpha\(t\),\\,f\_\{l,2\}\(\\alpha\(f\_\{l,2\}^\{\-1\}\(f\_\{l,2\}\(t\)\)\)\),\\,\\dots\\big\)=\\big\(\\alpha\(t\),f\_\{l,2\}\(\\alpha\(t\)\),\\dots,f\_\{l,m\_\{l\}\}\(\\alpha\(t\)\)\\big\), using thatfl,jf\_\{l,j\}is injective; this is again the point ofΨl\\Psi\_\{l\}indexed byα​\(t\)\\alpha\(t\)\. HenceGl≤Aut​\(ΦC\)G\_\{l\}\\leq\\mathrm\{Aut\}\(\\Phi\_\{C\}\), andGlG\_\{l\}acts onΨl\\Psi\_\{l\}exactly asSym​\(Tl\)\\mathrm\{Sym\}\(T\_\{l\}\)acts onTlT\_\{l\}under the bijectiont↔\(fl,1​\(t\),…,fl,ml​\(t\)\)t\\leftrightarrow\(f\_\{l,1\}\(t\),\\dots,f\_\{l,m\_\{l\}\}\(t\)\), transitively\.

For the free positions,GF:=∏i∈FSym​\(Si\)≤Aut​\(ΦC\)G\_\{F\}:=\\prod\_\{i\\in F\}\\mathrm\{Sym\}\(S\_\{i\}\)\\leq\\mathrm\{Aut\}\(\\Phi\_\{C\}\)trivially, andGFG\_\{F\}is transitive on∏i∈FSi\\prod\_\{i\\in F\}S\_\{i\}\.

The subgroup∏l=1rGl×GF≤Aut​\(ΦC\)\\prod\_\{l=1\}^\{r\}G\_\{l\}\\times G\_\{F\}\\leq\\mathrm\{Aut\}\(\\Phi\_\{C\}\)acts onΦC=∏lΨl×∏FSi\\Phi\_\{C\}=\\prod\_\{l\}\\Psi\_\{l\}\\times\\prod\_\{F\}S\_\{i\}coordinatewise, factor by factor, on pairwise disjoint sets of positions\. A product of transitive actions on disjoint coordinates is transitive on the product: given two points ofΦC\\Phi\_\{C\}, transitivity of each factor supplies a group element matching that factor, and the factors compose into a single element of∏lGl×GF\\prod\_\{l\}G\_\{l\}\\times G\_\{F\}matching every factor at once\. HenceAut​\(ΦC\)\\mathrm\{Aut\}\(\\Phi\_\{C\}\), which contains this subgroup, is transitive onΦC\\Phi\_\{C\}\. ∎

Computationally verified; see[AppendixB](https://arxiv.org/html/2608.10420#A2)\.

The second transitivity result covers instances built from several disjoint syntactic cases, or branches, rather than a single matching pattern\.

###### Theorem 4\.4\(Branch swapping, Theorem B\)\.

LetΦC=Φ1∪⋯∪Φr\\Phi\_\{C\}=\\Phi\_\{1\}\\cup\\cdots\\cup\\Phi\_\{r\}\. Suppose there is a subgroupG1≤Aut​\(ΦC\)G\_\{1\}\\leq\\mathrm\{Aut\}\(\\Phi\_\{C\}\)withG1​\(Φ1\)=Φ1G\_\{1\}\(\\Phi\_\{1\}\)=\\Phi\_\{1\}acting transitively onΦ1\\Phi\_\{1\}, and elementsκ2,…,κr∈Aut​\(ΦC\)\\kappa\_\{2\},\\dots,\\kappa\_\{r\}\\in\\mathrm\{Aut\}\(\\Phi\_\{C\}\)withκl​\(Φ1\)=Φl\\kappa\_\{l\}\(\\Phi\_\{1\}\)=\\Phi\_\{l\}forl=2,…,rl=2,\\dots,r\. ThenAut​\(ΦC\)\\mathrm\{Aut\}\(\\Phi\_\{C\}\)acts transitively onΦC\\Phi\_\{C\}\.

###### Proof\.

Setκ1:=id\\kappa\_\{1\}:=\\mathrm\{id\}\. Givenϕ∈Φl\\phi\\in\\Phi\_\{l\}andϕ′∈Φl′\\phi^\{\\prime\}\\in\\Phi\_\{l^\{\\prime\}\}\(possiblyl=l′l=l^\{\\prime\}\),κl−1​\(ϕ\)\\kappa\_\{l\}^\{\-1\}\(\\phi\)andκl′−1​\(ϕ′\)\\kappa\_\{l^\{\\prime\}\}^\{\-1\}\(\\phi^\{\\prime\}\)both lie inΦ1\\Phi\_\{1\}, sinceκl​\(Φ1\)=Φl\\kappa\_\{l\}\(\\Phi\_\{1\}\)=\\Phi\_\{l\}\. Transitivity ofG1G\_\{1\}onΦ1\\Phi\_\{1\}suppliesh∈G1h\\in G\_\{1\}withh​\(κl−1​\(ϕ\)\)=κl′−1​\(ϕ′\)h\(\\kappa\_\{l\}^\{\-1\}\(\\phi\)\)=\\kappa\_\{l^\{\\prime\}\}^\{\-1\}\(\\phi^\{\\prime\}\)\. Theng:=κl′∘h∘κl−1∈Aut​\(ΦC\)g:=\\kappa\_\{l^\{\\prime\}\}\\circ h\\circ\\kappa\_\{l\}^\{\-1\}\\in\\mathrm\{Aut\}\(\\Phi\_\{C\}\)satisfiesg​\(ϕ\)=ϕ′g\(\\phi\)=\\phi^\{\\prime\}\. ∎

Computationally verified; see[AppendixB](https://arxiv.org/html/2608.10420#A2)\.

### 4\.4Sufficient conditions for intransitivity, I: forced fibers

The next result gives a sufficient condition for the failure of transitivity, built directly on the Forcing Lemma\. It shows that a conjunctive constraint set, with no disjunction anywhere in it, can still fail to be transitive: transitivity is not implied by conjunction, even though every diagonal\-equality example in Section[4\.3](https://arxiv.org/html/2608.10420#S4.SS3)is a conjunction\.

###### Theorem 4\.6\(Anchor forcing, Theorem C\)\.

LetX=\(N,S,C\)X=\(N,S,C\)be an instance in the sense of[Definition2\.1](https://arxiv.org/html/2608.10420#S2.Thmtheorem1)and leti,j,k∈Ni,j,k\\in NsatisfySi=Sj=Sk=:DS\_\{i\}=S\_\{j\}=S\_\{k\}=:D\. Suppose

1. \(a\)πi​j​\(ΦC\)\\pi\_\{ij\}\(\\Phi\_\{C\}\)equalsΔD\\Delta\_\{D\}orD×D∖ΔDD\\times D\\setminus\\Delta\_\{D\};
2. \(b\)πi​k​\(ΦC\)\\pi\_\{ik\}\(\\Phi\_\{C\}\)equalsΔD\\Delta\_\{D\}orD×D∖ΔDD\\times D\\setminus\\Delta\_\{D\}, independently of the choice made in \(a\);
3. \(c\)bothϕj=ϕk\\phi\_\{j\}=\\phi\_\{k\}andϕj≠ϕk\\phi\_\{j\}\\neq\\phi\_\{k\}occur among solutionsϕ∈ΦC\\phi\\in\\Phi\_\{C\}\.

ThenAut​\(ΦC\)\\mathrm\{Aut\}\(\\Phi\_\{C\}\)does not act transitively onΦC\\Phi\_\{C\}\.

###### Proof\.

By Lemma[4\.1](https://arxiv.org/html/2608.10420#S4.Thmtheorem1)applied to\(i,j\)\(i,j\)and to\(i,k\)\(i,k\), everyσ∈Aut​\(ΦC\)\\sigma\\in\\mathrm\{Aut\}\(\\Phi\_\{C\}\)satisfiesσi=σj\\sigma\_\{i\}=\\sigma\_\{j\}andσi=σk\\sigma\_\{i\}=\\sigma\_\{k\}, henceσj=σk=:γ\\sigma\_\{j\}=\\sigma\_\{k\}=:\\gamma, a single permutation ofDDshared by every automorphism\. Ifϕ′=σ⋅ϕ\\phi^\{\\prime\}=\\sigma\\cdot\\phifor someσ∈Aut​\(ΦC\)\\sigma\\in\\mathrm\{Aut\}\(\\Phi\_\{C\}\), thenϕj′=γ​\(ϕj\)\\phi^\{\\prime\}\_\{j\}=\\gamma\(\\phi\_\{j\}\)andϕk′=γ​\(ϕk\)\\phi^\{\\prime\}\_\{k\}=\\gamma\(\\phi\_\{k\}\), soϕj′=ϕk′\\phi^\{\\prime\}\_\{j\}=\\phi^\{\\prime\}\_\{k\}if and only ifϕj=ϕk\\phi\_\{j\}=\\phi\_\{k\}, sinceγ\\gammais a bijection\. The predicate “ϕj=ϕk\\phi\_\{j\}=\\phi\_\{k\}” is therefore constant on everyAut​\(ΦC\)\\mathrm\{Aut\}\(\\Phi\_\{C\}\)\-orbit\. By \(c\) it takes both values onΦC\\Phi\_\{C\}, soΦC\\Phi\_\{C\}is not a single orbit\. ∎

The smallest instance exhibiting this mechanism hasD=\{0,1,2\}D=\\\{0,1,2\\\}and

ΦC=\{\(a,b,c\)∈D3:a≠b,a≠c\},\\Phi\_\{C\}=\\\{\(a,b,c\)\\in D^\{3\}:a\\neq b,\\ a\\neq c\\\},a conjunction of two inequalities with no disjunction\. Here\|ΦC\|=12\|\\Phi\_\{C\}\|=12,πi​j​\(ΦC\)=πi​k​\(ΦC\)=D×D∖ΔD\\pi\_\{ij\}\(\\Phi\_\{C\}\)=\\pi\_\{ik\}\(\\Phi\_\{C\}\)=D\\times D\\setminus\\Delta\_\{D\}and\|Aut​\(ΦC\)\|=6\|\\mathrm\{Aut\}\(\\Phi\_\{C\}\)\|=6\(the diagonal copy ofSym​\(D\)\\mathrm\{Sym\}\(D\)\), splitting into two orbits of size 6, exactly the classesb=cb=candb≠cb\\neq cpredicted by the proof\. This directly falsifies the conjecture that a conjunctive constraint set implies transitivity: two inequality constraints, sharing no disjunction with any other structure, already break transitivity, by leaving open whether the two non\-anchor legs agree with each other\.

The counterexample predates the theorem: it surfaced in a randomized search and was then proved, and the searches around it carry falsification value of their own\. A broader random search over conjunctive and disjunctive constraint sets confirms neither connective determines the outcome on its own; a second, independent search targeting false positives of the theorem’s hypothesis found none; and the anchor\-and\-two\-legs pattern generalizes to more attached legs without degenerating, confirming the mechanism is not an artifact of the smallest case\. Computationally verified; see[AppendixB](https://arxiv.org/html/2608.10420#A2)\.

### 4\.5Sufficient conditions for intransitivity, II: two invariants

The anchor\-forcing pattern needs two positions sharing a domain with the anchor\. The next two results give intransitivity criteria that need no such coincidence, built from invariants anyσ∈Aut​\(ΦC\)\\sigma\\in\\mathrm\{Aut\}\(\\Phi\_\{C\}\)must preserve\.

###### Lemma 4\.7\.

Forσ∈Aut​\(ΦC\)\\sigma\\in\\mathrm\{Aut\}\(\\Phi\_\{C\}\), positioni∈Ni\\in N, and valuev∈Siv\\in S\_\{i\}, writedegi⁡\(v\):=\|\{ϕ∈ΦC:ϕi=v\}\|\\deg\_\{i\}\(v\):=\|\\\{\\phi\\in\\Phi\_\{C\}:\\phi\_\{i\}=v\\\}\|\. Thendegi⁡\(v\)=degi⁡\(σi​\(v\)\)\\deg\_\{i\}\(v\)=\\deg\_\{i\}\(\\sigma\_\{i\}\(v\)\)\.

###### Proof\.

σ\\sigmarestricts to a bijectionΦC→ΦC\\Phi\_\{C\}\\to\\Phi\_\{C\}, sinceσ\\sigmaandσ−1\\sigma^\{\-1\}both lie inAut​\(ΦC\)\\mathrm\{Aut\}\(\\Phi\_\{C\}\)\. It carries\{ϕ∈ΦC:ϕi=v\}\\\{\\phi\\in\\Phi\_\{C\}:\\phi\_\{i\}=v\\\}bijectively onto\{ϕ∈ΦC:ϕi=σi​\(v\)\}\\\{\\phi\\in\\Phi\_\{C\}:\\phi\_\{i\}=\\sigma\_\{i\}\(v\)\\\}, becauseϕi=v\\phi\_\{i\}=vholds if and only if\(σ⋅ϕ\)i=σi​\(v\)\(\\sigma\\cdot\\phi\)\_\{i\}=\\sigma\_\{i\}\(v\)holds\. Bijective images have equal cardinality\. ∎

###### Theorem 4\.8\(Degree invariant, Theorem D\)\.

If some positioni∈Ni\\in Nhas two valuesv,v′∈Siv,v^\{\\prime\}\\in S\_\{i\}that both occur inΦC\\Phi\_\{C\}withdegi⁡\(v\)≠degi⁡\(v′\)\\deg\_\{i\}\(v\)\\neq\\deg\_\{i\}\(v^\{\\prime\}\), thenAut​\(ΦC\)\\mathrm\{Aut\}\(\\Phi\_\{C\}\)does not act transitively onΦC\\Phi\_\{C\}\.

###### Proof\.

SupposeAut​\(ΦC\)\\mathrm\{Aut\}\(\\Phi\_\{C\}\)is transitive\. Chooseϕ,ϕ′∈ΦC\\phi,\\phi^\{\\prime\}\\in\\Phi\_\{C\}withϕi=v\\phi\_\{i\}=vandϕi′=v′\\phi^\{\\prime\}\_\{i\}=v^\{\\prime\}; transitivity suppliesσ∈Aut​\(ΦC\)\\sigma\\in\\mathrm\{Aut\}\(\\Phi\_\{C\}\)withσ⋅ϕ=ϕ′\\sigma\\cdot\\phi=\\phi^\{\\prime\}, soσi​\(v\)=σi​\(ϕi\)=\(σ⋅ϕ\)i=ϕi′=v′\\sigma\_\{i\}\(v\)=\\sigma\_\{i\}\(\\phi\_\{i\}\)=\(\\sigma\\cdot\\phi\)\_\{i\}=\\phi^\{\\prime\}\_\{i\}=v^\{\\prime\}\. Lemma[4\.7](https://arxiv.org/html/2608.10420#S4.Thmtheorem7)then givesdegi⁡\(v\)=degi⁡\(σi​\(v\)\)=degi⁡\(v′\)\\deg\_\{i\}\(v\)=\\deg\_\{i\}\(\\sigma\_\{i\}\(v\)\)=\\deg\_\{i\}\(v^\{\\prime\}\), contradicting the hypothesis\. ∎

Theorem[4\.8](https://arxiv.org/html/2608.10420#S4.Thmtheorem8)directly matches a real reasoning shortcut mechanism: a value with a special algebraic role, such as a multiplicative zero, is taken by a different number of solutions than an ordinary value\. On an abstract zero\-factor family, exact enumeration confirms the predicted degree asymmetry and non\-transitivity at every tested size\. Computationally verified; see[AppendixB](https://arxiv.org/html/2608.10420#A2)\. A parallel measurement identifies the same mechanism in rsbench’s real multiplication task: 31 of 32 achievable productsyygive a transitiveAut​\(ΦC\)\\mathrm\{Aut\}\(\\Phi\_\{C\}\), buty=0y=0\(the 19 factor pairsc1×c2=0c\_\{1\}\\times c\_\{2\}=0\) does not, because degree\-0 factor pairs are strictly more numerous than degree\-1 pairs and no coordinate permutation can equalize them\. An arithmetic control with no absorbing element is constant\-degree and transitive throughout, as the theorem predicts, and a random battery of instances built from equality and inequality atoms produces neither false nor true positives for the theorem, confirming the degree invariant targets absorbing\-element structure specifically rather than substituting for Theorem[4\.6](https://arxiv.org/html/2608.10420#S4.Thmtheorem6)’s equality\-atom mechanism\. Computationally verified; see[AppendixB](https://arxiv.org/html/2608.10420#A2)\.

###### Theorem 4\.9\(Orbit\-stabilizer counting, Theorem E\)\.

IfAut​\(ΦC\)\\mathrm\{Aut\}\(\\Phi\_\{C\}\)acts transitively onΦC\\Phi\_\{C\}, then\|ΦC\|\|\\Phi\_\{C\}\|divides\|Aut​\(ΦC\)\|\|\\mathrm\{Aut\}\(\\Phi\_\{C\}\)\|; in particular\|ΦC\|≤\|Aut​\(ΦC\)\|≤\|G\|=∏i\|Si\|\!\|\\Phi\_\{C\}\|\\leq\|\\mathrm\{Aut\}\(\\Phi\_\{C\}\)\|\\leq\|G\|=\\prod\_\{i\}\|S\_\{i\}\|\!\.

###### Proof\.

Fixϕ0∈ΦC\\phi\_\{0\}\\in\\Phi\_\{C\}\. The orbit\-stabilizer theorem gives orbit size\|Aut​\(ΦC\)\|/\|Stab​\(ϕ0\)\|\|\\mathrm\{Aut\}\(\\Phi\_\{C\}\)\|/\|\\mathrm\{Stab\}\(\\phi\_\{0\}\)\|, which divides\|Aut​\(ΦC\)\|\|\\mathrm\{Aut\}\(\\Phi\_\{C\}\)\|\. Transitivity means this orbit is all ofΦC\\Phi\_\{C\}\. The bound\|Aut​\(ΦC\)\|≤\|G\|\|\\mathrm\{Aut\}\(\\Phi\_\{C\}\)\|\\leq\|G\|is Lagrange’s theorem applied toAut​\(ΦC\)≤G\\mathrm\{Aut\}\(\\Phi\_\{C\}\)\\leq G\. ∎

The proof is four lines, a direct instance of a standard fact, and its value is entirely in the observation that it applies\. Applying it to grid puzzles takes one preparatory step\. Under Definition[2\.5](https://arxiv.org/html/2608.10420#S2.Thmtheorem5)the ambient group of a3×33\\times 3grid isSym​\(3\)9\\mathrm\{Sym\}\(3\)^\{9\}, of order696^\{9\}, so the raw Lagrange bound of Theorem[4\.9](https://arxiv.org/html/2608.10420#S4.Thmtheorem9)obstructs nothing; the useful bound is that the constraints collapseAut​\(ΦC\)\\mathrm\{Aut\}\(\\Phi\_\{C\}\)to the*diagonal*, and that is a forcing argument in the pattern of Lemma[4\.1](https://arxiv.org/html/2608.10420#S4.Thmtheorem1), not an ambient fact\.

###### Lemma 4\.10\(Pair\-rich all\-different lines force the diagonal\)\.

Let every position ofXXshare one value domainDD, and let some family of all\-different constraints \(“lines”\) connect all positions\. SupposeΦC\\Phi\_\{C\}is*pair\-rich*: for every line, every ordered pairi≠ji\\neq jof positions on it, and every ordered paira≠ba\\neq bof values, some solution assigns\(a,b\)\(a,b\)to\(i,j\)\(i,j\)\. Then everyσ∈Aut​\(ΦC\)\\sigma\\in\\mathrm\{Aut\}\(\\Phi\_\{C\}\)has all components equal, soAut​\(ΦC\)≤\{\(π,…,π\):π∈Sym​\(D\)\}\\mathrm\{Aut\}\(\\Phi\_\{C\}\)\\leq\\\{\(\\pi,\\dots,\\pi\):\\pi\\in\\mathrm\{Sym\}\(D\)\\\}and\|Aut​\(ΦC\)\|≤\|D\|\!\|\\mathrm\{Aut\}\(\\Phi\_\{C\}\)\|\\leq\|D\|\!\.

###### Proof\.

Fix a line, positionsi≠ji\\neq jon it, and valuesa≠ba\\neq b\. Pair\-richness givesϕ∈ΦC\\phi\\in\\Phi\_\{C\}withϕ​\(i\)=a\\phi\(i\)=a,ϕ​\(j\)=b\\phi\(j\)=b\. Sinceσ⋅ϕ∈ΦC\\sigma\\cdot\\phi\\in\\Phi\_\{C\}andi,ji,jshare an all\-different line,σi​\(a\)≠σj​\(b\)\\sigma\_\{i\}\(a\)\\neq\\sigma\_\{j\}\(b\), for every such paira≠ba\\neq b\. Fixingbband lettingaarange overD∖\{b\}D\\setminus\\\{b\\\}:σj​\(b\)\\sigma\_\{j\}\(b\)avoidsσi​\(D∖\{b\}\)=D∖\{σi​\(b\)\}\\sigma\_\{i\}\(D\\setminus\\\{b\\\}\)=D\\setminus\\\{\\sigma\_\{i\}\(b\)\\\}, forcingσj​\(b\)=σi​\(b\)\\sigma\_\{j\}\(b\)=\\sigma\_\{i\}\(b\)\. Soσi=σj\\sigma\_\{i\}=\\sigma\_\{j\}wheneveri,ji,jshare a line, and line\-connectivity propagates equality to every position\. ∎

Pair\-richness is a property of the solution set, checked mechanically \(it is a finite scan\), and it holds for all three grid instances measured in[Section3](https://arxiv.org/html/2608.10420#S3): 3rd\-order Latin squares \(\|ΦC\|=12\|\\Phi\_\{C\}\|=12\),4×44\\times 4Sudoku with2×22\\times 2boxes \(\|ΦC\|=288\|\\Phi\_\{C\}\|=288\), and 4th\-order Latin squares without boxes \(\|ΦC\|=576\|\\Phi\_\{C\}\|=576\), over value domains of size 3 or 4\. Lemma[4\.10](https://arxiv.org/html/2608.10420#S4.Thmtheorem10)then caps\|Aut​\(ΦC\)\|\|\\mathrm\{Aut\}\(\\Phi\_\{C\}\)\|at3\!=63\!=6or4\!=244\!=24, and the exact groups, computed independently by backtracking, hit the cap’s structure exactly: every element diagonal, orders66,2424, and2424\. Since a transitive action would makeΦC\\Phi\_\{C\}a single orbit of size at most\|Aut​\(ΦC\)\|\|\\mathrm\{Aut\}\(\\Phi\_\{C\}\)\|, and12\>612\>6,288\>24288\>24,576\>24576\>24, Theorem[4\.9](https://arxiv.org/html/2608.10420#S4.Thmtheorem9)rules out transitivity for the whole family: a counting argument, once the collapse lemma supplies the bound the count runs against\. Computationally verified; see[AppendixB](https://arxiv.org/html/2608.10420#A2)\. This is not automatic for every all\-different instance: a single row of three pairwise\-distinct cells,D=\{0,1,2\}D=\\\{0,1,2\\\}, has\|ΦC\|=6=\|Aut​\(ΦC\)\|\|\\Phi\_\{C\}\|=6=\|\\mathrm\{Aut\}\(\\Phi\_\{C\}\)\|and is transitive, since the count only obstructs transitivity once\|ΦC\|\|\\Phi\_\{C\}\|exceeds\|Aut​\(ΦC\)\|\|\\mathrm\{Aut\}\(\\Phi\_\{C\}\)\|, which a single row does not\. Row and column constraints compounded together grow\|ΦC\|\|\\Phi\_\{C\}\|past the diagonal bound well beforeNNgrows large, and Theorem[4\.9](https://arxiv.org/html/2608.10420#S4.Thmtheorem9)then applies for a combinatorial reason that has nothing to do with equalities, inequalities, or absorbing elements\.

### 4\.6The Kandinsky residual and the Free Slot Lemma

Kandinsky’s rule, three branches indexed by which pair of three objects matches on shape and color, is the single most consequential positive result in the empirical measurements of[Section3](https://arxiv.org/html/2608.10420#S3):81\.99%81\.99\\%of solution pairs are not explained by any automorphism, split across 6 orbits of sizes\[36,36,36,18,18,18\]\[36,36,36,18,18,18\]out of\|ΦC\|=162\|\\Phi\_\{C\}\|=162solutions and\|Aut​\(ΦC\)\|=36\|\\mathrm\{Aut\}\(\\Phi\_\{C\}\)\|=36\. None of Theorems[4\.3](https://arxiv.org/html/2608.10420#S4.Thmtheorem3)through[4\.9](https://arxiv.org/html/2608.10420#S4.Thmtheorem9)accounts for it\. Theorem A does not apply; the rule is a genuine three\-way disjunction, not a matching decomposition\. Theorem B does not apply, and Remark[4\.5](https://arxiv.org/html/2608.10420#S4.Thmtheorem5)already explains why: the three branches are exchanged by relabeling*which object is which*, a positional symmetry with no representative inAut​\(ΦC\)\\mathrm\{Aut\}\(\\Phi\_\{C\}\)\. Theorem C does not apply either: checking all pairs among the two shape positions and the two color positions used by the rule shows each projection mixes diagonal and off\-diagonal pairs across the three branches, so no anchor\-and\-two\-legs pattern is pure in the sense Lemma[4\.1](https://arxiv.org/html/2608.10420#S4.Thmtheorem1)requires\. Theorem D is silent: exhaustive computation givesdegshape1⁡\(v\)=54\\deg\_\{\\mathrm\{shape\}\_\{1\}\}\(v\)=54for every shape valuevv, and the same uniformity holds for color, so no coordinate carries a degree asymmetry\. Theorem E does confirm intransitivity, since162162does not divide3636, but only once\|Aut​\(ΦC\)\|=36\|\\mathrm\{Aut\}\(\\Phi\_\{C\}\)\|=36is already known from exhaustive computation; it gives no route to that fact on its own\.

This section closes that gap with a sixth result that certifies Kandinsky’s branch structure directly from the rule, without first computingAut​\(ΦC\)\\mathrm\{Aut\}\(\\Phi\_\{C\}\)\.

###### Theorem 4\.11\(Free Slot Lemma, Theorem F\)\.

LetΦC=Φ1⊔⋯⊔Φr\\Phi\_\{C\}=\\Phi\_\{1\}\\sqcup\\cdots\\sqcup\\Phi\_\{r\}and fix a positionf∈Nf\\in Nand an indexl0l\_\{0\}\. Suppose:

\(H\-free\)Φl0\\Phi\_\{l\_\{0\}\}is saturated atff: there is a setΨ⊆∏i≠fSi\\Psi\\subseteq\\prod\_\{i\\neq f\}S\_\{i\}withΦl0=\{z∪\{f:v\}:z∈Ψ,v∈Sf\}\\Phi\_\{l\_\{0\}\}=\\\{z\\cup\\\{f\{:\}v\\\}:z\\in\\Psi,\\ v\\in S\_\{f\}\\\}, so membership inΦl0\\Phi\_\{l\_\{0\}\}places no restriction at all on the value atff;

\(H\-pin\)for everyl≠l0l\\neq l\_\{0\}and every assignmentzzto the positions other thanff, at most one valuev∈Sfv\\in S\_\{f\}hasz∪\{f:v\}∈Φlz\\cup\\\{f\{:\}v\\\}\\in\\Phi\_\{l\};

\(H\-count\)\|Sf\|\>r−1\|S\_\{f\}\|\>r\-1\.

Then everyσ∈Aut​\(ΦC\)\\sigma\\in\\mathrm\{Aut\}\(\\Phi\_\{C\}\)satisfiesσ​\(Φl0\)=Φl0\\sigma\(\\Phi\_\{l\_\{0\}\}\)=\\Phi\_\{l\_\{0\}\}\.

###### Proof\.

Writex=z0∪\{f:xf\}∈Φl0x=z\_\{0\}\\cup\\\{f\{:\}x\_\{f\}\\\}\\in\\Phi\_\{l\_\{0\}\}withz0∈Ψz\_\{0\}\\in\\Psi, and letz0′z\_\{0\}^\{\\prime\}be the image ofz0z\_\{0\}’s non\-ffcoordinates underσ\\sigma; it does not depend onxfx\_\{f\}, sinceσ\\sigmaacts coordinatewise\. By \(H\-free\),z0∪\{f:v\}∈Φl0⊆ΦCz\_\{0\}\\cup\\\{f\{:\}v\\\}\\in\\Phi\_\{l\_\{0\}\}\\subseteq\\Phi\_\{C\}for*every*v∈Sfv\\in S\_\{f\}, not onlyv=xfv=x\_\{f\}, soσ​\(z0∪\{f:v\}\)=z0′∪\{f:σf​\(v\)\}∈ΦC\\sigma\(z\_\{0\}\\cup\\\{f\{:\}v\\\}\)=z\_\{0\}^\{\\prime\}\\cup\\\{f\{:\}\\sigma\_\{f\}\(v\)\\\}\\in\\Phi\_\{C\}for every suchvv\. Asvvranges overSfS\_\{f\}, so doesσf​\(v\)\\sigma\_\{f\}\(v\), sinceσf\\sigma\_\{f\}is a bijection; hencez0′∪\{f:w\}∈ΦCz\_\{0\}^\{\\prime\}\\cup\\\{f\{:\}w\\\}\\in\\Phi\_\{C\}for everyw∈Sfw\\in S\_\{f\}\.

Suppose toward a contradiction thatz0′∉Ψz\_\{0\}^\{\\prime\}\\notin\\Psi\. Then by \(H\-free\), none of these\|Sf\|\|S\_\{f\}\|points lies inΦl0\\Phi\_\{l\_\{0\}\}, so every one lies in someΦl\\Phi\_\{l\}withl≠l0l\\neq l\_\{0\}\. By \(H\-pin\), each suchllaccounts for at most one value ofww, and there are at mostr−1r\-1choices ofll, so at mostr−1r\-1of the\|Sf\|\|S\_\{f\}\|points are covered\. This contradicts \(H\-count\)\. Hencez0′∈Ψz\_\{0\}^\{\\prime\}\\in\\Psi, and \(H\-free\) givesz0′∪\{f:w\}∈Φl0z\_\{0\}^\{\\prime\}\\cup\\\{f\{:\}w\\\}\\in\\Phi\_\{l\_\{0\}\}for everyw∈Sfw\\in S\_\{f\}; takingw=σf​\(xf\)w=\\sigma\_\{f\}\(x\_\{f\}\)givesσ​\(x\)∈Φl0\\sigma\(x\)\\in\\Phi\_\{l\_\{0\}\}\.

This holds for everyσ∈Aut​\(ΦC\)\\sigma\\in\\mathrm\{Aut\}\(\\Phi\_\{C\}\), in particular forσ−1\\sigma^\{\-1\}, givingσ−1​\(Φl0\)⊆Φl0\\sigma^\{\-1\}\(\\Phi\_\{l\_\{0\}\}\)\\subseteq\\Phi\_\{l\_\{0\}\}and henceΦl0⊆σ​\(Φl0\)\\Phi\_\{l\_\{0\}\}\\subseteq\\sigma\(\\Phi\_\{l\_\{0\}\}\); together withσ​\(Φl0\)⊆Φl0\\sigma\(\\Phi\_\{l\_\{0\}\}\)\\subseteq\\Phi\_\{l\_\{0\}\}this gives equality\. ∎

The proof never refers toAut​\(ΦC\)\\mathrm\{Aut\}\(\\Phi\_\{C\}\)’s order or to any other branch’s internal structure; it only uses the three named hypotheses, each checked directly against the rule\. Applied to Kandinsky withf=f=the color position of the object not mentioned by branchl0l\_\{0\}’s matching pair \(color3for branch 1, color2for branch 2, color1for branch 3\): \(H\-free\) holds because that color is unconstrained given the rest of the solution \(54 solutions per branch, 3 color values each,54×3=16254\\times 3=162substitutions checked, all remaining inΦC\\Phi\_\{C\}and in the same branch\); \(H\-pin\) holds because the other two branches pin that color to at most one value given the rest \(243×2=486243\\times 2=486checks, maximum attainable count exactly 1\); and \(H\-count\) holds since3\>3−13\>3\-1\. Theorem[4\.11](https://arxiv.org/html/2608.10420#S4.Thmtheorem11)then gives that each of the three branches is setwise invariant under everyσ∈Aut​\(ΦC\)\\sigma\\in\\mathrm\{Aut\}\(\\Phi\_\{C\}\), and three nonempty invariant branches already force at least 3 orbits: Kandinsky is not transitive, established from the rule’s syntax and without enumeratingAut​\(ΦC\)\\mathrm\{Aut\}\(\\Phi\_\{C\}\)\.

### 4\.7Synthesis: coverage and its boundary

[Table5](https://arxiv.org/html/2608.10420#S4.T5)lines up the six results above against the four constraint\-structure mechanisms[Section3](https://arxiv.org/html/2608.10420#S3)isolates empirically\.

Table 5:The six algebraic results against the four mechanisms identified empirically in[Section3](https://arxiv.org/html/2608.10420#S3)\. “Full” means every measured instance of the mechanism is accounted for by a proof; “partial” means the theorem covers the minimal instances tested but a fully general statement is open; “none” means no result in this section applies and the outcome is established only by exhaustive computation\.Two entries need qualification beyond the table\. Asymmetric disjunction is only*partially*covered: the minimal two\-branch example behind Theorem[4\.4](https://arxiv.org/html/2608.10420#S4.Thmtheorem4)’s counterpart has a degree asymmetry that Theorem[4\.8](https://arxiv.org/html/2608.10420#S4.Thmtheorem8)also detects, but nothing in this section proves that every asymmetric disjunction produces a degree asymmetry, and Kandinsky’s own branches are a case where it does not \(uniform degree throughout, Section[4\.6](https://arxiv.org/html/2608.10420#S4.SS6)\), so the two phenomena the empirical mechanisms group together, asymmetric pinning and degree imbalance, are related but not shown to coincide in general\. Kandinsky itself is covered by Theorem[4\.11](https://arxiv.org/html/2608.10420#S4.Thmtheorem11)for the reason Section[4\.6](https://arxiv.org/html/2608.10420#S4.SS6)gives, but BDD\-OIA and SDD\-OIA are not: their pathology is a single dead coordinate absorbed by a logical implication rather than a multi\-branch disjunction, a mechanism[Section5](https://arxiv.org/html/2608.10420#S5)addresses with different tools \(the𝔽2\\mathbb\{F\}\_\{2\}\-linear structure of[2\.8](https://arxiv.org/html/2608.10420#S2.Thmtheorem8)and the AND\-gain lemma of Section[5](https://arxiv.org/html/2608.10420#S5)\), not with Theorem[4\.11](https://arxiv.org/html/2608.10420#S4.Thmtheorem11)\. That two independent toolkits, orbit combinatorics here and linear algebra over𝔽2\\mathbb\{F\}\_\{2\}in[Section5](https://arxiv.org/html/2608.10420#S5), both explain the same dead\-variable phenomenon by different means is a cross\-check worth noting rather than a duplication: neither result was built to reproduce the other\.

None of the six results is a disguised instance of Schaefer’s dichotomy for CSP satisfiability\[[22](https://arxiv.org/html/2608.10420#bib.bib22)\]\. Schaefer’s theorem classifies the complexity of deciding whether*some*solution exists, as a function of which relations the constraint language may use; this section instead takes a single, already nonemptyΦC\\Phi\_\{C\}as given and asks a group\-theoretic question about its orbit structure underGG\. The connection is real but indirect: the affine class in Schaefer’s dichotomy is generated by a Maltsev polymorphism, and the Bulatov–Dalmau family of algorithms for such languages is correct because of a rectangularity property proved through absorption arguments\[[3](https://arxiv.org/html/2608.10420#bib.bib3)\], the same “coordinates copy a single parameter” intuition behind Theorem[4\.3](https://arxiv.org/html/2608.10420#S4.Thmtheorem3)’s matching decomposition\. No proof in this section rewrites a Schaefer\-style algorithm, and none of the five other results has any counterpart in that literature at all, since none of it addresses the automorphism group of a fixed solution set\. We flag the connection because a reader who knows the CSP dichotomy literature will look for it, not because it does any of the work here\.

Finally, every result in this section is a sufficient condition, by design\. Theorem[4\.9](https://arxiv.org/html/2608.10420#S4.Thmtheorem9)gives a necessary numerical condition \(transitivity implies\|ΦC\|\|\\Phi\_\{C\}\|divides\|Aut​\(ΦC\)\|\|\\mathrm\{Aut\}\(\\Phi\_\{C\}\)\|\) that happens to be violated, hence sufficient for intransitivity, on every all\-different instance measured; nothing here gives a necessary and sufficient characterization of transitivity for general finite\-domain constraint sets, and[Section4\.1](https://arxiv.org/html/2608.10420#S4.SS1)’s discussion of autotopism groups suggests why: the analogous question for Latin squares has resisted a clean characterization for decades and is answered, on each instance individually, by direct computation\. What this section adds is a set of proved, checked reasons that cover four of the four empirical mechanisms at least partially and one real benchmark, Kandinsky, in full, leaving BDD\-OIA’s dead\-variable mechanism to the linear\-algebraic treatment in[Section5](https://arxiv.org/html/2608.10420#S5)and the general classification question open\.

## 5Computational Complexity

Section[4](https://arxiv.org/html/2608.10420#S4)gave sufficient conditions on the shape of a constraint set forAut​\(ΦC\)\\mathrm\{Aut\}\(\\Phi\_\{C\}\)to be transitive or not\. This section asks a different question: given the constraint set itself, packaged as a compact circuit rather than written out atom by atom, how hard is it to tell which case applies? We place two decision problems in the polynomial hierarchy, give five structural results that make the Boolean case’s automorphism group tractable to reason about \(though not to compute\), and transplant a collapse theorem from Boolean\-formula isomorphism to show that the harder of the two problems is unlikely to sit at the top of the range we prove it occupies\. Two results then settle their cases outright: transitivity is classified exactly in the Boolean case, and on monotone circuits the existence question is coNP\-complete under deterministic reductions\. The section closes there, where the gap closes;[AppendixA](https://arxiv.org/html/2608.10420#A1)distills eight independent attempts on the general gap into the three structural facts any future attack must clear\.

### 5\.1Succinct instances and two decision problems

Throughout,X=\(N,S,C\)X=\(N,S,C\)is an instance in the sense of[Definition2\.1](https://arxiv.org/html/2608.10420#S2.Thmtheorem1), withAut​\(ΦC\)≤∏i=1nSym​\(Si\)\\mathrm\{Aut\}\(\\Phi\_\{C\}\)\\leq\\prod\_\{i=1\}^\{n\}\\mathrm\{Sym\}\(S\_\{i\}\)its componentwise automorphism group \([Definition2\.5](https://arxiv.org/html/2608.10420#S2.Thmtheorem5)\)\. We now add a representational assumption that Section[4](https://arxiv.org/html/2608.10420#S4)did not need:CCis a Boolean circuit of sizepoly​\(n\+∑i\|Si\|\)\\mathrm\{poly\}\(n\+\\sum\_\{i\}\|S\_\{i\}\|\)deciding membership inΦC⊆∏iSi\\Phi\_\{C\}\\subseteq\\prod\_\{i\}S\_\{i\}\. This is the regime CLE4EVR and BDD\-OIA already forced on us in[Section2](https://arxiv.org/html/2608.10420#S2):CCis a few lines of symbolic logic, whileΦC\\Phi\_\{C\}itself can have thousands to millions of elements\. The input is the circuit together with an explicit listing of each domain, so the input length isL:=\|C\|\+∑i\|Si\|L:=\|C\|\+\\sum\_\{i\}\|S\_\{i\}\|, with domains in unary\. This matches CSP practice, where domains are enumerated, and it deliberately excludes succinctly specified exponential domains \(a single position with\|S1\|=2k\|S\_\{1\}\|=2^\{k\}given in binary\), a different regime in which even writing down one permutation of one domain takesΘ​\(2k​k\)\\Theta\(2^\{k\}k\)bits and every question below changes character\. A point of∏iSi\\prod\_\{i\}S\_\{i\}is named innbits:=∑i⌈log2⁡\|Si\|⌉≤Ln\_\{\\mathrm\{bits\}\}:=\\sum\_\{i\}\\lceil\\log\_\{2\}\|S\_\{i\}\|\\rceil\\leq Lbits, and an element of∏i=1nSym​\(Si\)\\prod\_\{i=1\}^\{n\}\\mathrm\{Sym\}\(S\_\{i\}\)is specified explicitly in∑i\|Si\|​⌈log2⁡\|Si\|⌉=O​\(L​log⁡L\)\\sum\_\{i\}\|S\_\{i\}\|\\lceil\\log\_\{2\}\|S\_\{i\}\|\\rceil=O\(L\\log L\)bits, polynomial in the input; every hardness construction in this section uses\|Si\|≤2\|S\_\{i\}\|\\leq 2, where the two conventions coincide\.

###### Definition 5\.1\(Dead\-Var\)\.

An input is a circuitCCand a positioni∈Ni\\in Nwith\|Si\|=2\|S\_\{i\}\|=2, written\{0,1\}\\\{0,1\\\}\.Dead\-Varaccepts\(C,i\)\(C,i\)ifflipi:=\(id,…,id,σi,id,…,id\)∈Aut​\(ΦC\)\\mathrm\{flip\}\_\{i\}:=\(\\mathrm\{id\},\\dots,\\mathrm\{id\},\\sigma\_\{i\},\\mathrm\{id\},\\dots,\\mathrm\{id\}\)\\in\\mathrm\{Aut\}\(\\Phi\_\{C\}\), whereσi\\sigma\_\{i\}swaps0and11: equivalently,C​\(c\)=C​\(flipi​\(c\)\)C\(c\)=C\(\\mathrm\{flip\}\_\{i\}\(c\)\)for everyc∈∏jSjc\\in\\prod\_\{j\}S\_\{j\}\.

###### Definition 5\.2\(Nontriv\-Aut\)\.

An input is a circuitCC\.Nontriv\-AutacceptsCCifAut​\(ΦC\)≠\{id\}\\mathrm\{Aut\}\(\\Phi\_\{C\}\)\\neq\\\{\\mathrm\{id\}\\\}, that is, someσ∈∏i=1nSym​\(Si\)∖\{id\}\\sigma\\in\\prod\_\{i=1\}^\{n\}\\mathrm\{Sym\}\(S\_\{i\}\)\\setminus\\\{\\mathrm\{id\}\\\}satisfiesC​\(c\)=C​\(σ⋅c\)C\(c\)=C\(\\sigma\\cdot c\)for everyc∈∏jSjc\\in\\prod\_\{j\}S\_\{j\}\.

Dead\-Varasks about one designated candidate;Nontriv\-Autasks whether any candidate at all works\.[Section2](https://arxiv.org/html/2608.10420#S2)’s observation that a position absent from every constraint inflatesAut​\(ΦC\)\\mathrm\{Aut\}\(\\Phi\_\{C\}\)with automorphisms that carry no information about the rule is exactly the phenomenonDead\-Varis built to detect\.

### 5\.2Dead variables: a coNP\-complete baseline

###### Theorem 5\.3\.

Dead\-Varis coNP\-complete\.

###### Proof\.

*Membership\.*The complement is NP: guessc∈∏jSjc\\in\\prod\_\{j\}S\_\{j\}and verifyC​\(c\)≠C​\(flipi​\(c\)\)C\(c\)\\neq C\(\\mathrm\{flip\}\_\{i\}\(c\)\)in two circuit evaluations\.

*Hardness\.*Reduce fromunsat\. Given a 3\-CNF formulaχ​\(z1,…,zk\)\\chi\(z\_\{1\},\\dots,z\_\{k\}\), letN=\{i,z1,…,zk\}N=\\\{i,z\_\{1\},\\dots,z\_\{k\}\\\}, all with domain\{0,1\}\\\{0,1\\\}, andC​\(xi,z\):=xi∧χ​\(z\)C\(x\_\{i\},z\):=x\_\{i\}\\wedge\\chi\(z\)\. ThenC​\(0,z\)≡0C\(0,z\)\\equiv 0andC​\(1,z\)=χ​\(z\)C\(1,z\)=\\chi\(z\), soflipi∈Aut​\(ΦC\)\\mathrm\{flip\}\_\{i\}\\in\\mathrm\{Aut\}\(\\Phi\_\{C\}\)\(that is,C​\(0,z\)=C​\(1,z\)C\(0,z\)=C\(1,z\)for everyzz\) if and only ifχ​\(z\)=0\\chi\(z\)=0for everyzz, if and only ifχ\\chiis unsatisfiable\. ∎

Dead\-Varis the special caseC↾xi=0≡C↾xi=1C\\restriction\_\{x\_\{i\}=0\}\\equiv C\\restriction\_\{x\_\{i\}=1\}of deciding whether two circuits compute the same Boolean function, and its classification is inherited from Beyersdorff, Meier, Thomas, and Vollmer, who give a complete dichotomy for that equivalence problem, restricted to any fixed set of allowed connectives, over the full Post lattice\[[4](https://arxiv.org/html/2608.10420#bib.bib4)\]\. The three\-line reduction above keeps Sections[5\.3](https://arxiv.org/html/2608.10420#S5.SS3)through[5\.7](https://arxiv.org/html/2608.10420#S5.SS7)self\-contained: every harder result in this section is built on top of this base case, and a reader should not have to leave the paper to check it\. When the allowed connectives are restricted to a fixed finite setBB,Dead\-Varrestricted toBBcoincides with their equivalence problemEQ​\(B∪\{0,1\}\)\\mathrm\{EQ\}\(B\\cup\\\{0,1\\\}\)after substituting the two constants forxix\_\{i\}, and inherits their dichotomy \(coNP\-complete,𝖠𝖢0​\[2\]\\mathsf\{AC\}^\{0\}\[2\]\-complete, or in𝖠𝖢0\\mathsf\{AC\}^\{0\}, depending on whereBBsits in Post’s lattice\) without further proof\. \(Their Theorem 4\.1 for the unrestricted implication problemIMP​\(B\)\\mathrm\{IMP\}\(B\)has a fourth,⊕L\\oplus L\-complete case atL2⊆\[B\]⊆LL\_\{2\}\\subseteq\[B\]\\subseteq L; Corollary 5\.2 records that this case collapses to𝖠𝖢0​\[2\]\\mathsf\{AC\}^\{0\}\[2\]once the problem is specialized to equivalence, which is the dichotomyDead\-Varactually inherits\.\)

### 5\.3Nontrivial automorphisms: upper and lower bounds

###### Theorem 5\.4\.

Nontriv\-Aut∈Σ2𝗉\\textup\{\{Nontriv\-Aut\}\}\\in\\Sigma\_\{2\}^\{\\mathsf\{p\}\}\.

###### Proof\.

An element of∏i=1nSym​\(Si\)\\prod\_\{i=1\}^\{n\}\\mathrm\{Sym\}\(S\_\{i\}\)is specified inO​\(L​log⁡L\)O\(L\\log L\)bits, polynomial in the input under Section[5\.1](https://arxiv.org/html/2608.10420#S5.SS1)’s unary\-domain convention\.Nontriv\-AutacceptsCCiff∃σ∈∏i=1nSym​\(Si\)​\(σ≠id\)​∀c∈∏jSj:C​\(c\)=C​\(σ⋅c\)\\exists\\sigma\\in\\prod\_\{i=1\}^\{n\}\\mathrm\{Sym\}\(S\_\{i\}\)\\ \(\\sigma\\neq\\mathrm\{id\}\)\\ \\forall c\\in\\prod\_\{j\}S\_\{j\}:\\ C\(c\)=C\(\\sigma\\cdot c\), an∃y​∀z​R​\(x,y,z\)\\exists y\\,\\forall z\\,R\(x,y,z\)sentence withRRevaluable in polynomial time, Stockmeyer’s normal form forΣ2𝗉\\Sigma\_\{2\}^\{\\mathsf\{p\}\}\. ∎

###### Observation 5\.5\.

IfDead\-Var​\(C,i\)\\textup\{\{Dead\-Var\}\}\(C,i\)holds, so doesNontriv\-Aut​\(C\)\\textup\{\{Nontriv\-Aut\}\}\(C\):flipi\\mathrm\{flip\}\_\{i\}is a nonidentity element ofAut​\(ΦC\)\\mathrm\{Aut\}\(\\Phi\_\{C\}\)\.

Observation[5\.5](https://arxiv.org/html/2608.10420#S5.Thmtheorem5)is immediate, but it is the only unconditional bridge fromDead\-VartoNontriv\-Autwe have\. It is tempting to read Theorem[5\.3](https://arxiv.org/html/2608.10420#S5.Thmtheorem3)’s reduction as already provingNontriv\-Autis coNP\-hard: exhibit the sameC​\(xi,z\)=xi∧χ​\(z\)C\(x\_\{i\},z\)=x\_\{i\}\\wedge\\chi\(z\)and noteflipi∈Aut​\(ΦC\)\\mathrm\{flip\}\_\{i\}\\in\\mathrm\{Aut\}\(\\Phi\_\{C\}\)exactly whenχ\\chiis unsatisfiable\. This is correct in one direction and incomplete in the other\. Ifχ\\chiis unsatisfiable,ΦC=∅\\Phi\_\{C\}=\\emptysetand everyσ∈∏i=1nSym​\(Si\)\\sigma\\in\\prod\_\{i=1\}^\{n\}\\mathrm\{Sym\}\(S\_\{i\}\)trivially stabilizes it, soNontriv\-Aut​\(C\)\\textup\{\{Nontriv\-Aut\}\}\(C\)holds\. Ifχ\\chiis satisfiable*and*has no nonzerob∈\{0,1\}kb\\in\\\{0,1\\\}^\{k\}withχ​\(z⊕b\)=χ​\(z\)\\chi\(z\\oplus b\)=\\chi\(z\)for everyzz, then\(id,σb\)∉Aut​\(ΦC\)\(\\mathrm\{id\},\\sigma\_\{b\}\)\\notin\\mathrm\{Aut\}\(\\Phi\_\{C\}\)for every candidate built from such abb, and one checks directly thatAut​\(ΦC\)=\{id\}\\mathrm\{Aut\}\(\\Phi\_\{C\}\)=\\\{\\mathrm\{id\}\\\}, soNontriv\-Aut​\(C\)\\textup\{\{Nontriv\-Aut\}\}\(C\)correctly fails\. The gap is formulas that are satisfiable*and*happen to have such an internal symmetry: a randomly chosenz↦z⊕bz\\mapsto z\\oplus bsymmetry ofχ\\chimakes\(id,σb\)\(\\mathrm\{id\},\\sigma\_\{b\}\)a nonidentity element ofAut​\(ΦC\)\\mathrm\{Aut\}\(\\Phi\_\{C\}\)regardless of whetherχ\\chiis satisfiable, so the reduction reportsNontriv\-Aut​\(C\)\\textup\{\{Nontriv\-Aut\}\}\(C\)even on some satisfiable instances\. This is not a rare edge case: a pressure test shows a nontrivial automorphism fromχ\\chi’s own accidental symmetry, unrelated toii, is common among satisfiable instances\. Computationally verified; see[AppendixB](https://arxiv.org/html/2608.10420#A2)\.

Closing this gap does not take a cleverer deterministic gadget\. Three natural deterministic fixes \(padding with a fixed unary tag, encodingzzas a single large\-domain position, and presenting aDead\-Varinstance unmodified\) fail for one shared reason, not three unrelated ones: each is a fixed,χ\\chi\-independent transformation, and no fixed transformation can know, for the specificχ\\chihanded to it, which internal symmetry, if any, to destroy\. A fixed tag adds a position with no interaction withzzat all, so it leaves whatever symmetryχ\\chialready has completely untouched\. Encodingzzas a single position with an abstract2k2^\{k\}\-element domain replaces the XOR shiftsχ\\chimight have with the full symmetric group on all2k2^\{k\}valueszzcould take, not just its XOR shifts, so almost anyχ\\chiwith at least two satisfying and two falsifying assignments picks up spurious automorphisms that have nothing to do withχ\\chi’s own structure\. Presenting the instance unmodified is just the construction the pressure test above already broke\. What removes the gap is randomization, which does not need to knowχ\\chi’s symmetry in advance: perturbχ\\chiwith a small number of random affine constraints before handing it to the Theorem[5\.3](https://arxiv.org/html/2608.10420#S5.Thmtheorem3)gadget, so that a satisfiableχ\\chiis cut down to a single satisfying assignment with non\-negligible probability\. A one\-element solution set has no nonzero internal symmetry at all, whatever symmetryχ\\chiitself started with: if\{p\}\\\{p\\\}is fixed setwise byz↦z⊕bz\\mapsto z\\oplus b, thenp⊕b=pp\\oplus b=p, forcingb=0b=0\.

###### Lemma 5\.6\(Automorphisms of the anchor\-conjunction gadget\)\.

Fixk≥1k\\geq 1and a Boolean formulaψ:\{0,1\}k→\{0,1\}\\psi:\\\{0,1\\\}^\{k\}\\to\\\{0,1\\\}\. LetN=\{xi,z1,…,zk\}N=\\\{x\_\{i\},z\_\{1\},\\dots,z\_\{k\}\\\}, all with domain\{0,1\}\\\{0,1\\\}, andC​\(xi,z\):=xi∧ψ​\(z\)C\(x\_\{i\},z\):=x\_\{i\}\\wedge\\psi\(z\), so an element\(ai,b\)∈∏i=1nSym​\(Si\)\(a\_\{i\},b\)\\in\\prod\_\{i=1\}^\{n\}\\mathrm\{Sym\}\(S\_\{i\}\)\(ai∈\{0,1\}a\_\{i\}\\in\\\{0,1\\\},b∈\{0,1\}kb\\in\\\{0,1\\\}^\{k\}\) acts by\(ai,b\)⋅\(xi,z\)=\(xi⊕ai,z⊕b\)\(a\_\{i\},b\)\\cdot\(x\_\{i\},z\)=\(x\_\{i\}\\oplus a\_\{i\},\\,z\\oplus b\)\.

1. \(i\)Ifψ\\psiis unsatisfiable,Aut​\(ΦC\)=∏i=1nSym​\(Si\)\\mathrm\{Aut\}\(\\Phi\_\{C\}\)=\\prod\_\{i=1\}^\{n\}\\mathrm\{Sym\}\(S\_\{i\}\)\.
2. \(ii\)Ifψ\\psiis satisfiable,Aut​\(ΦC\)=\{\(0,b\):b∈\{0,1\}k,ψ​\(z⊕b\)=ψ​\(z\)​for every​z\}\\mathrm\{Aut\}\(\\Phi\_\{C\}\)=\\\{\(0,b\):b\\in\\\{0,1\\\}^\{k\},\\ \\psi\(z\\oplus b\)=\\psi\(z\)\\text\{ for every \}z\\\}\.

###### Proof\.

\(ai,b\)∈Aut​\(ΦC\)\(a\_\{i\},b\)\\in\\mathrm\{Aut\}\(\\Phi\_\{C\}\)saysxi∧ψ​\(z\)=\(xi⊕ai\)∧ψ​\(z⊕b\)x\_\{i\}\\wedge\\psi\(z\)=\(x\_\{i\}\\oplus a\_\{i\}\)\\wedge\\psi\(z\\oplus b\)for everyxi∈\{0,1\}x\_\{i\}\\in\\\{0,1\\\}and everyzz\. Atxi=0x\_\{i\}=0this reads0=ai∧ψ​\(z⊕b\)0=a\_\{i\}\\wedge\\psi\(z\\oplus b\)for everyzz, and aszzranges over\{0,1\}k\\\{0,1\\\}^\{k\}so doesz⊕bz\\oplus b, so this forcesai=0a\_\{i\}=0wheneverψ\\psiis satisfiable, and holds for everyaia\_\{i\}whenψ\\psiis unsatisfiable\. Ifψ\\psiis satisfiable,ai=0a\_\{i\}=0turns thexi=1x\_\{i\}=1condition intoψ​\(z\)=ψ​\(z⊕b\)\\psi\(z\)=\\psi\(z\\oplus b\)for everyzz, giving \(ii\)\. Ifψ\\psiis unsatisfiable,xi∧ψ​\(z\)≡0x\_\{i\}\\wedge\\psi\(z\)\\equiv 0identically, so every\(ai,b\)∈∏i=1nSym​\(Si\)\(a\_\{i\},b\)\\in\\prod\_\{i=1\}^\{n\}\\mathrm\{Sym\}\(S\_\{i\}\)vacuously satisfies the automorphism condition, giving \(i\)\. ∎

Lemma[5\.6](https://arxiv.org/html/2608.10420#S5.Thmtheorem6)says the false positives above are not a defect in the gadget\. Wheneverψ\\psiis satisfiable,Aut​\(ΦC\)\\mathrm\{Aut\}\(\\Phi\_\{C\}\)is exactly\{0\}\\\{0\\\}timesψ\\psi’s own internal XOR symmetries, so the gadget correctly reportsψ\\psi’s symmetry back to us rather than manufacturing any of its own\. Part \(i\) also settles, with no extra gadgetry, the empty\-instance convention this construction leans on:NNalways containsxix\_\{i\}regardless ofψ\\psi, so∏i=1nSym​\(Si\)\\prod\_\{i=1\}^\{n\}\\mathrm\{Sym\}\(S\_\{i\}\)always hasSym​\(\{0,1\}\)\\mathrm\{Sym\}\(\\\{0,1\\\}\)as a factor and is never the trivial group, and an unsatisfiableψ\\psialways produces the full group, a clean nontrivial instance under Definition[5\.2](https://arxiv.org/html/2608.10420#S5.Thmtheorem2)’s stated convention with no promise or side condition needed\.

To make part \(ii\) trivial whenχ\\chiis satisfiable, we do not need to know or controlχ\\chi’s own symmetries\. We only needχ\\chi’s solution set to have no nonzero internal XOR symmetry, and cutting it down to a single point is enough for that, by the one\-line argument closing the transition paragraph above\. This is exactly what the Valiant–Vazirani isolation lemma\[[27](https://arxiv.org/html/2608.10420#bib.bib27)\]gives, applied here to an arbitrary nonempty subset of\{0,1\}k\\\{0,1\\\}^\{k\}rather than toAut​\(ΦC\)\\mathrm\{Aut\}\(\\Phi\_\{C\}\)itself, and that distinction matters for which form of the lemma applies\.Aut​\(ΦC\)\\mathrm\{Aut\}\(\\Phi\_\{C\}\)is always closed under coordinatewise XOR \(ifa,a′∈Aut​\(ΦC\)a,a^\{\\prime\}\\in\\mathrm\{Aut\}\(\\Phi\_\{C\}\), applyingaaand thena′a^\{\\prime\}showsa⊕a′∈Aut​\(ΦC\)a\\oplus a^\{\\prime\}\\in\\mathrm\{Aut\}\(\\Phi\_\{C\}\)too\), so isolating a nonzero element ofAut​\(ΦC\)\\mathrm\{Aut\}\(\\Phi\_\{C\}\)can use a stronger, constant\-probability construction that repeatedly intersects this closed set with a random hyperplane\.ΦC\\Phi\_\{C\}for an arbitrary 3\-CNFχ\\chihas no such structure\. It is just some subset of\{0,1\}k\\\{0,1\\\}^\{k\}, so we need the general form of the isolation lemma, and its success probability is correspondingly weaker\. For a nonemptyS⊆\{0,1\}kS\\subseteq\\\{0,1\\\}^\{k\}, drawingjjuniformly from\{0,…,k\}\\\{0,\\dots,k\\\}and thenjjaffine constraintsw1⋅z=c1,…,wj⋅z=cjw\_\{1\}\\cdot z=c\_\{1\},\\dots,w\_\{j\}\\cdot z=c\_\{j\}uniformly over𝔽2k\\mathbb\{F\}\_\{2\}^\{k\}cutsSSdown to exactly one element with probability at leastc0/\(k\+1\)c\_\{0\}/\(k\+1\)for an absolute constantc0\>0c\_\{0\}\>0not depending onSSorkk\. The standard analysis, which we cite rather than re\-derive, givesc0=1/8c\_\{0\}=1/8for the correctly guessedjj, combined with a1/\(k\+1\)1/\(k\+1\)chance of guessingjjcorrectly\. We use this as a standard imported fact, in the same spirit as this section’s use of Beyersdorff et al\.’s dichotomy above\.

###### Corollary 5\.7\.

Nontriv\-Autis coNP\-hard under randomized polynomial\-time many\-one reductions with one\-sided error and success probabilityΩ​\(1/k\)\\Omega\(1/k\), the same reduction type under which Valiant and Vazirani proveunique\-satNP\-hard\[[27](https://arxiv.org/html/2608.10420#bib.bib27)\]\. There is a probabilistic polynomial\-time algorithmRRsuch that for every 3\-CNF formulaχ\\chionkkvariables, writingC:=R​\(χ\)C:=R\(\\chi\),

1. \(i\)ifχ\\chiis unsatisfiable,Nontriv\-Aut​\(C\)\\textup\{\{Nontriv\-Aut\}\}\(C\)holds with probability11;
2. \(ii\)ifχ\\chiis satisfiable,Nontriv\-Aut​\(C\)\\textup\{\{Nontriv\-Aut\}\}\(C\)fails to hold with probability at leastc0/\(k\+1\)c\_\{0\}/\(k\+1\), for the constantc0c\_\{0\}above\.

###### Proof\.

RRdrawsjjuniformly from\{0,…,k\}\\\{0,\\dots,k\\\}, drawsjjaffine constraintsw1⋅z=c1,…,wj⋅z=cjw\_\{1\}\\cdot z=c\_\{1\},\\dots,w\_\{j\}\\cdot z=c\_\{j\}uniformly over𝔽2k\\mathbb\{F\}\_\{2\}^\{k\}, setsχ′​\(z\):=χ​\(z\)∧⋀t=1j\(wt⋅z=ct\)\\chi^\{\\prime\}\(z\):=\\chi\(z\)\\wedge\\bigwedge\_\{t=1\}^\{j\}\(w\_\{t\}\\cdot z=c\_\{t\}\), and outputsC​\(xi,z\):=xi∧χ′​\(z\)C\(x\_\{i\},z\):=x\_\{i\}\\wedge\\chi^\{\\prime\}\(z\), an instance of the family Lemma[5\.6](https://arxiv.org/html/2608.10420#S5.Thmtheorem6)covers withψ=χ′\\psi=\\chi^\{\\prime\}\. Adding constraints only shrinks a solution set, soχ\\chiunsatisfiable forcesχ′\\chi^\{\\prime\}unsatisfiable for every choice of constraints, and part \(i\) of the lemma givesAut​\(ΦC\)=∏i=1nSym​\(Si\)≠\{id\}\\mathrm\{Aut\}\(\\Phi\_\{C\}\)=\\prod\_\{i=1\}^\{n\}\\mathrm\{Sym\}\(S\_\{i\}\)\\neq\\\{\\mathrm\{id\}\\\}with probability11, proving \(i\)\. Ifχ\\chiis satisfiable, the isolation lemma above, applied toS:=\{z∈\{0,1\}k:χ​\(z\)=1\}S:=\\\{z\\in\\\{0,1\\\}^\{k\}:\\chi\(z\)=1\\\}, gives\|\{z:χ′​\(z\)=1\}\|=1\|\\\{z:\\chi^\{\\prime\}\(z\)=1\\\}\|=1with probability at leastc0/\(k\+1\)c\_\{0\}/\(k\+1\)\. When this happens, write\{z:χ′​\(z\)=1\}=\{p\}\\\{z:\\chi^\{\\prime\}\(z\)=1\\\}=\\\{p\\\}: for everyb≠0b\\neq 0,χ′​\(p⊕b\)=0≠1=χ′​\(p\)\\chi^\{\\prime\}\(p\\oplus b\)=0\\neq 1=\\chi^\{\\prime\}\(p\), soppitself witnesses thatχ′\\chi^\{\\prime\}has no nonzero internal XOR symmetry, and part \(ii\) of the lemma givesAut​\(ΦC\)=\{\(0,0\)\}=\{id\}\\mathrm\{Aut\}\(\\Phi\_\{C\}\)=\\\{\(0,0\)\\\}=\\\{\\mathrm\{id\}\\\}, soNontriv\-Aut​\(C\)\\textup\{\{Nontriv\-Aut\}\}\(C\)fails, proving \(ii\)\. ∎

Both directions of Corollary[5\.7](https://arxiv.org/html/2608.10420#S5.Thmtheorem7)were checked computationally before being trusted as a proof, not only reasoned about\. Computationally verified; see[AppendixB](https://arxiv.org/html/2608.10420#A2)\.

The full\-exposure reading is not a choice bookkeeping could avoid: sincez1,…,zkz\_\{1\},\\dots,z\_\{k\}are read byCCat all, Definition[2\.1](https://arxiv.org/html/2608.10420#S2.Thmtheorem1)forces them to be positions inNN, becauseCC’s domain is exactly∏i∈NSi\\prod\_\{i\\in N\}S\_\{i\}and no circuit can depend on a value without that value being a position the componentwise group acts on\. The isolation step in Corollary[5\.7](https://arxiv.org/html/2608.10420#S5.Thmtheorem7)’s proof is therefore not an optional strengthening but what a fully general, promise\-free statement requires\.

###### Proposition 5\.10\(Alive\-promise hardness\)\.

Dead\-Varremains coNP\-hard on the promise family of instances in which every position other than the designatediiis alive\. Consequently, an oracle reporting the correct dead/alive status of every position other thaniicannot make decidingDead\-Var​\(C,i\)\\textup\{\{Dead\-Var\}\}\(C,i\)easier: on this family its answers are constant \(“alive” everywhere\), so it supplies no information at all\.

###### Proof\.

The gadget of Theorem[5\.3](https://arxiv.org/html/2608.10420#S5.Thmtheorem3)does not have this promise: a positionzjz\_\{j\}is dead inxi∧χ​\(z\)x\_\{i\}\\wedge\\chi\(z\)exactly when it is dead inχ\\chi, which the reduction neither controls nor can afford to compute\. Modify it\. Given a 3\-CNFφ​\(w1,…,wm\)\\varphi\(w\_\{1\},\\dots,w\_\{m\}\), add one fresh positionttand output

C​\(xi,w,t\):=\(xi∧φ​\(w\)∧¬t\)∨\(⋀jwj∧t\)\.C\(x\_\{i\},w,t\)\\;:=\\;\\big\(x\_\{i\}\\wedge\\varphi\(w\)\\wedge\\neg t\\big\)\\;\\vee\\;\\big\(\\textstyle\\bigwedge\_\{j\}w\_\{j\}\\wedge t\\big\)\.Everywjw\_\{j\}is alive: att=1t=1,w=1mw=1^\{m\}, flippingwjw\_\{j\}changes the second disjunct and henceCC\. So istt:C​\(0,1m,1\)=1≠0=C​\(0,1m,0\)C\(0,1^\{m\},1\)=1\\neq 0=C\(0,1^\{m\},0\)\. Both checks are independent ofφ\\varphi, so the whole family satisfies the promise\. Finally,C​\(0,⋅\)C\(0,\\cdot\)is the second disjunct alone, andC​\(1,⋅\)C\(1,\\cdot\)adds the first, soxix\_\{i\}is dead iffφ​\(w\)∧¬t\\varphi\(w\)\\wedge\\neg timplies⋀jwj∧t\\bigwedge\_\{j\}w\_\{j\}\\wedge tpointwise; the two sides force opposite values oftt, so the implication holds iffφ∧¬t\\varphi\\wedge\\neg tis unsatisfiable iffφ\\varphiis\. DecidingDead\-Var​\(C,i\)\\textup\{\{Dead\-Var\}\}\(C,i\)on this family therefore decidesunsat\. Both claims were checked exhaustively on 500 random mixed satisfiable/unsatisfiable instances before being trusted as a proof\. Computationally verified; see[AppendixB](https://arxiv.org/html/2608.10420#A2)\. ∎

Proposition[5\.10](https://arxiv.org/html/2608.10420#S5.Thmtheorem10)answers a natural objection to Section[4\.5](https://arxiv.org/html/2608.10420#S4.SS5)’s degree invariant and to[Section2](https://arxiv.org/html/2608.10420#S2)’s observation that unconstrained positions inflateAut​\(ΦC\)\\mathrm\{Aut\}\(\\Phi\_\{C\}\): knowing which coordinates are free does not make the remaining question easy\. Stripping dead variables is a necessary cleaning step, not a complexity\-reducing one\.

### 5\.4Structural theorems in the Boolean case

[2\.8](https://arxiv.org/html/2608.10420#S2.Thmtheorem8)showed that when everySi=\{0,1\}S\_\{i\}=\\\{0,1\\\},Aut​\(ΦC\)\\mathrm\{Aut\}\(\\Phi\_\{C\}\)is an𝔽2\\mathbb\{F\}\_\{2\}\-linear subspace of𝔽2n\\mathbb\{F\}\_\{2\}^\{n\}\. WriteL0​\(f\):=Aut​\(ΦC\)L\_\{0\}\(f\):=\\mathrm\{Aut\}\(\\Phi\_\{C\}\)under the identification∏i=1nSym​\(Si\)≅𝔽2n\\prod\_\{i=1\}^\{n\}\\mathrm\{Sym\}\(S\_\{i\}\)\\cong\\mathbb\{F\}\_\{2\}^\{n\},σ↔a\\sigma\\leftrightarrow a,σ⋅c=c⊕a\\sigma\\cdot c=c\\oplus a, for the indicator functionffofΦC\\Phi\_\{C\}\. In the cryptographic literature this subspace is known as the*linear structures*offf\[[18](https://arxiv.org/html/2608.10420#bib.bib18),[9](https://arxiv.org/html/2608.10420#bib.bib9)\]; we keep the short derivations below self\-contained rather than importing statements from that setting\.

###### Corollary 5\.11\.

In the Boolean case,\|Aut​\(ΦC\)\|∈\{1,2,4,…,2n\}\|\\mathrm\{Aut\}\(\\Phi\_\{C\}\)\|\\in\\\{1,2,4,\\dots,2^\{n\}\\\}\.

###### Proof\.

The order of a subspace of annn\-dimensional𝔽2\\mathbb\{F\}\_\{2\}\-vector space is2dim2^\{\\dim\}for some0≤dim≤n0\\leq\\dim\\leq n\. ∎

This is why BDD\-OIA and SDD\-OIA’s measured\|Aut​\(ΦC\)\|=2\|\\mathrm\{Aut\}\(\\Phi\_\{C\}\)\|=2on every achievable label \([Section3](https://arxiv.org/html/2608.10420#S3)\) is not a coincidence to be explained away: any nonempty proper subgroup of𝔽2n\\mathbb\{F\}\_\{2\}^\{n\}that arises this way sits at one of finitely many, exponentially spaced steps, and a single generator lands exactly on the second one\.

The subspace structure yields more than the group’s order\. Because the group acts by translations, it acts*freely*, and freeness turns the entire orbit geometry into arithmetic\.

###### Proposition 5\.12\(Free action and exact orbit geometry\)\.

In the Boolean case the action ofAut​\(ΦC\)=L0​\(f\)\\mathrm\{Aut\}\(\\Phi\_\{C\}\)=L\_\{0\}\(f\)onΦC\\Phi\_\{C\}is free: no nonidentity shift fixes any point\. Consequently every orbit has size exactly\|Aut​\(ΦC\)\|\|\\mathrm\{Aut\}\(\\Phi\_\{C\}\)\|, the orbits partitionΦC\\Phi\_\{C\}into\|ΦC\|/\|Aut​\(ΦC\)\|\|\\Phi\_\{C\}\|/\|\\mathrm\{Aut\}\(\\Phi\_\{C\}\)\|equal classes, and for\|ΦC\|≥2\|\\Phi\_\{C\}\|\\geq 2the unexplained\-pair fraction of[Section3](https://arxiv.org/html/2608.10420#S3)is the exact law

ρ​\(ΦC\)=1−\|Aut​\(ΦC\)\|−1\|ΦC\|−1\.\\rho\(\\Phi\_\{C\}\)\\;=\\;1\-\\frac\{\|\\mathrm\{Aut\}\(\\Phi\_\{C\}\)\|\-1\}\{\|\\Phi\_\{C\}\|\-1\}\.

###### Proof\.

Ifc⊕a=cc\\oplus a=cthena=0a=0, so point stabilizers are trivial and every orbit is a bijective copy of the group\. Withk:=\|ΦC\|/\|Aut​\(ΦC\)\|k:=\|\\Phi\_\{C\}\|/\|\\mathrm\{Aut\}\(\\Phi\_\{C\}\)\|orbits of common sizeg:=\|Aut​\(ΦC\)\|g:=\|\\mathrm\{Aut\}\(\\Phi\_\{C\}\)\|, same\-orbit pairs numberk​\(g2\)k\\binom\{g\}\{2\}out of\(k​g2\)\\binom\{kg\}\{2\}, and1−k​\(g2\)/\(k​g2\)=1−\(g−1\)/\(k​g−1\)1\-k\\binom\{g\}\{2\}/\\binom\{kg\}\{2\}=1\-\(g\-1\)/\(kg\-1\), which is the display\. ∎

###### Proposition 5\.13\(Transitivity classification, Boolean case\)\.

A Boolean instance is transitive under componentwise value symmetry if and only ifΦC\\Phi\_\{C\}is an affine coset of the subspaceL0​\(f\)L\_\{0\}\(f\), equivalently if and only if\|ΦC\|=\|Aut​\(ΦC\)\|\|\\Phi\_\{C\}\|=\|\\mathrm\{Aut\}\(\\Phi\_\{C\}\)\|\.

###### Proof\.

If the action is transitive,ΦC\\Phi\_\{C\}equals the orbit of anyϕ0∈ΦC\\phi\_\{0\}\\in\\Phi\_\{C\}, which isϕ0⊕L0​\(f\)\\phi\_\{0\}\\oplus L\_\{0\}\(f\), a coset\. Conversely a coset is a single orbit by construction\. The numerical criterion is Proposition[5\.12](https://arxiv.org/html/2608.10420#S5.Thmtheorem12)’s equal\-orbit\-size statement with one orbit\. ∎

The proof is a torsor argument from a first course in group theory, and that is precisely the point: positioned on the right object, one elementary fact closes the Boolean case of this paper’s central question outright, in a literature where we have found no statement of it\. Sufficient conditions are what[Section4](https://arxiv.org/html/2608.10420#S4)could offer in general; here the question is not approximated but settled, and the settlement is what turns[Section3](https://arxiv.org/html/2608.10420#S3)’s measured percentages into values of a theorem\.

Two readings of Proposition[5\.13](https://arxiv.org/html/2608.10420#S5.Thmtheorem13)are worth separating\. As a classification, it settles for Boolean instances what[Section4](https://arxiv.org/html/2608.10420#S4)’s six theorems approximate in general: transitivity is not merely implied by certain syntactic shapes, it is*characterized*, and the characterization is checkable given\|Aut​\(ΦC\)\|\|\\mathrm\{Aut\}\(\\Phi\_\{C\}\)\|\(affine solution sets, in Schaefer’s vocabulary\[[22](https://arxiv.org/html/2608.10420#bib.bib22)\]the XOR\-definable ones, are exactly the shortcut\-free\-modulo\-symmetry Boolean rules\)\. As an orbit law, Proposition[5\.12](https://arxiv.org/html/2608.10420#S5.Thmtheorem12)retroactively explains every BDD\-OIA/SDD\-OIA row of[Table2](https://arxiv.org/html/2608.10420#S3.T2)to the last digit: orbit count\|Φ\|/2\|\\Phi\|/2, maximum orbit22, and each of the eight “many nines” percentages equal to1−1/\(\|Φ\|−1\)1\-1/\(\|\\Phi\|\-1\)exactly\. What looked like eight measured decimals is one proposition evaluated eight times\. Computationally verified; see[AppendixB](https://arxiv.org/html/2608.10420#A2)\.

###### Lemma 5\.14\(Fourier characterization\)\.

LetF​\(x\):=\(−1\)f​\(x\)F\(x\):=\(\-1\)^\{f\(x\)\}with Walsh expansionF​\(x\)=∑T⊆\[n\]F^​\(T\)​χT​\(x\)F\(x\)=\\sum\_\{T\\subseteq\[n\]\}\\widehat\{F\}\(T\)\\,\\chi\_\{T\}\(x\),χT​\(x\):=\(−1\)T⋅x\\chi\_\{T\}\(x\):=\(\-1\)^\{T\\cdot x\}\. ThenL0​\(f\)=\(span𝔽2​supp​\(F^\)\)⟂L\_\{0\}\(f\)=\\big\(\\mathrm\{span\}\_\{\\mathbb\{F\}\_\{2\}\}\\,\\mathrm\{supp\}\(\\widehat\{F\}\)\\big\)^\{\\perp\}, the orthogonal complement, under the standard𝔽2\\mathbb\{F\}\_\{2\}\-bilinear form, of the span ofF^\\widehat\{F\}’s nonzero Fourier coefficients\.

###### Proof\.

For anyaa,χT​\(x⊕a\)=\(−1\)T⋅\(x⊕a\)=\(−1\)T⋅a​\(−1\)T⋅x=χT​\(a\)​χT​\(x\)\\chi\_\{T\}\(x\\oplus a\)=\(\-1\)^\{T\\cdot\(x\\oplus a\)\}=\(\-1\)^\{T\\cdot a\}\(\-1\)^\{T\\cdot x\}=\\chi\_\{T\}\(a\)\\chi\_\{T\}\(x\), usingT⋅\(x⊕a\)≡T⋅x\+T⋅a\(mod2\)T\\cdot\(x\\oplus a\)\\equiv T\\cdot x\+T\\cdot a\\pmod\{2\}coordinatewise\. HenceF​\(x⊕a\)=∑TF^​\(T\)​χT​\(a\)​χT​\(x\)F\(x\\oplus a\)=\\sum\_\{T\}\\widehat\{F\}\(T\)\\chi\_\{T\}\(a\)\\chi\_\{T\}\(x\)\. By uniqueness of the Walsh expansion,F​\(x⊕a\)=F​\(x\)F\(x\\oplus a\)=F\(x\)for everyxxif and only ifF^​\(T\)​χT​\(a\)=F^​\(T\)\\widehat\{F\}\(T\)\\chi\_\{T\}\(a\)=\\widehat\{F\}\(T\)for everyTT, that is,χT​\(a\)=1\\chi\_\{T\}\(a\)=1\(equivalentlyT⋅a≡0T\\cdot a\\equiv 0\) for everyTTwithF^​\(T\)≠0\\widehat\{F\}\(T\)\\neq 0\. Being orthogonal to every element ofsupp​\(F^\)\\mathrm\{supp\}\(\\widehat\{F\}\)is, by bilinearity, the same condition as being orthogonal to its span\. ∎

Computationally verified; see[AppendixB](https://arxiv.org/html/2608.10420#A2)\.

The decomposition half of the Boolean theory does generalize, and it is worth recording exactly how much, because it gives the dead\-variable criterion and[Section4](https://arxiv.org/html/2608.10420#S4)’s degree invariant a common spectral home\. For each position letQiQ\_\{i\}average a function over coordinateii, and letPi:=id−QiP\_\{i\}:=\\mathrm\{id\}\-Q\_\{i\}\. The operatorsPT:=∏i∈TPi​∏i∉TQiP\_\{T\}:=\\prod\_\{i\\in T\}P\_\{i\}\\prod\_\{i\\notin T\}Q\_\{i\}, forT⊆NT\\subseteq N, are commuting projectors summing to the identity, so everyh:∏iSi→ℝh:\\prod\_\{i\}S\_\{i\}\\to\\mathbb\{R\}splits ash=∑T⊆NhTh=\\sum\_\{T\\subseteq N\}h\_\{T\}withhT:=PT​hh\_\{T\}:=P\_\{T\}h; in the Boolean casehTh\_\{T\}is precisely the Fourier component supported onTT, so this is the verbatim generalization of the levels used by Lemma[5\.14](https://arxiv.org/html/2608.10420#S5.Thmtheorem14)\.

###### Proposition 5\.16\(Level decomposition over arbitrary domains\)\.

Letffbe the indicator ofΦC\\Phi\_\{C\}andf=∑TfTf=\\sum\_\{T\}f\_\{T\}the decomposition above\. Then: \(i\) eachPTP\_\{T\}commutes with the componentwise action, soσ∈Aut​\(ΦC\)\\sigma\\in\\mathrm\{Aut\}\(\\Phi\_\{C\}\)if and only ifσ\\sigmafixes every componentfTf\_\{T\}; \(ii\) positioniiis symmetry\-inert \(dead\) if and only iffT=0f\_\{T\}=0for everyTTcontainingii; \(iii\) the degree profile of Theorem[4\.8](https://arxiv.org/html/2608.10420#S4.Thmtheorem8)is a function of the singleton components alone:degi⁡\(v\)=\|ΦC\|/\|Si\|\+∑ϕ:ϕi=vf\{i\}​\(ϕ\)\\deg\_\{i\}\(v\)=\|\\Phi\_\{C\}\|/\|S\_\{i\}\|\+\\sum\_\{\\phi:\\,\\phi\_\{i\}=v\}f\_\{\\\{i\\\}\}\(\\phi\)\.

###### Proof\.

\(i\) Averaging over all values of a coordinate is invariant under permuting those values and untouched by permutations of other coordinates, so eachQiQ\_\{i\}, hence eachPTP\_\{T\}, commutes with everyσ∈∏i=1nSym​\(Si\)\\sigma\\in\\prod\_\{i=1\}^\{n\}\\mathrm\{Sym\}\(S\_\{i\}\)\. Ifσ\\sigmafixesffit fixes eachPT​fP\_\{T\}f; the converse is the sum\. \(ii\)iiis dead iffffis constant along coordinateii, iffQi​f=fQ\_\{i\}f=f, iffPi​f=0P\_\{i\}f=0, iff every component withi∈Ti\\in Tvanishes\. \(iii\) Fixiiandvvand sumfTf\_\{T\}over\{ϕ:ϕi=v\}\\\{\\phi:\\phi\_\{i\}=v\\\}\. IfTTcontains somej≠ij\\neq i, the sum ranges over all values of coordinatejjandfTf\_\{T\}has zero mean alongjj, so the term vanishes;T=∅T=\\emptysetcontributes the constant\|ΦC\|/∏j\|Sj\|\|\\Phi\_\{C\}\|/\\prod\_\{j\}\|S\_\{j\}\|summed over∏j≠i\|Sj\|\\prod\_\{j\\neq i\}\|S\_\{j\}\|points, which is\|ΦC\|/\|Si\|\|\\Phi\_\{C\}\|/\|S\_\{i\}\|;T=\{i\}T=\\\{i\\\}contributes the display’s second term\. ∎

Part \(ii\) is thek≥3k\\geq 3generalization of Lemma[5\.14](https://arxiv.org/html/2608.10420#S5.Thmtheorem14)’s dead\-variable criterion, and part \(iii\) says the degree invariant,[Section4](https://arxiv.org/html/2608.10420#S4)’s most combinatorial\-looking tool, is exactly a level\-one statement: Theorem D certifies intransitivity from the first spectral level, the Forcing Lemma operates at level two, and what fails fork≥3k\\geq 3is only the final identification of stabilizers with orthogonal complements, since the stabilizer of a component inside a tensor power of standard representations carries no subspace structure\. Developing that stabilizer theory is left open\. Computationally verified; see[AppendixB](https://arxiv.org/html/2608.10420#A2)\.

###### Lemma 5\.17\(AND\-gain\)\.

For anyf,g:\{0,1\}n→\{0,1\}f,g:\\\{0,1\\\}^\{n\}\\to\\\{0,1\\\},L0​\(f\)∩L0​\(g\)⊆L0​\(f∧g\)L\_\{0\}\(f\)\\cap L\_\{0\}\(g\)\\subseteq L\_\{0\}\(f\\wedge g\), and the containment can be strict\.

###### Proof\.

Ifaastabilizes bothffandggpointwise,\(f∧g\)​\(x⊕a\)=f​\(x⊕a\)∧g​\(x⊕a\)=f​\(x\)∧g​\(x\)=\(f∧g\)​\(x\)\(f\\wedge g\)\(x\\oplus a\)=f\(x\\oplus a\)\\wedge g\(x\\oplus a\)=f\(x\)\\wedge g\(x\)=\(f\\wedge g\)\(x\)for everyxx\. Strictness is a matter of exhibiting one instance where it occurs \(below\)\. ∎

The proof’s promised witness: in a representative case,\|L0​\(f\)\|=64\|L\_\{0\}\(f\)\|=64,\|L0​\(g\)\|=8\|L\_\{0\}\(g\)\|=8, and\|L0​\(f\)∩L0​\(g\)\|=8\|L\_\{0\}\(f\)\\cap L\_\{0\}\(g\)\|=8, yet\|L0​\(f∧g\)\|=64\|L\_\{0\}\(f\\wedge g\)\|=64, so the containment is strict\. Computationally verified; see[AppendixB](https://arxiv.org/html/2608.10420#A2)\. Lemma[5\.17](https://arxiv.org/html/2608.10420#S5.Thmtheorem17)is the general phenomenon behind a specific observation from[Section2](https://arxiv.org/html/2608.10420#S2): a variable that is syntactically present in one clause of a rule but semantically absorbed once that clause is conjoined with the rest \(a Boolean absorption law swallowing its effect\) can hand the conjunction an automorphism that no individual clause possesses on its own\. Nothing about this is specific to BDD\-OIA’s ‘follow‘ variable; it is a property of pointwise conjunction \(and, by the same one\-line argument, of any pointwise logical combination\) applied to any two Boolean functions\.

###### Proposition 5\.18\(Bent\-function witness construction\)\.

For everynnwithn−1n\-1even and every nonzeroa∈\{0,1\}na\\in\\\{0,1\\\}^\{n\}, there is an explicit, polynomial\-sizeffwithL0​\(f\)=\{0,a\}L\_\{0\}\(f\)=\\\{0,a\\\}exactly\. In particular the Hamming weight ofaa, the unique nonzero witness, can be made as large asnn\.

###### Proof\.

Fixjjwithaj=1a\_\{j\}=1and define the linear surjectionπ:\{0,1\}n→\{0,1\}n−1\\pi:\\\{0,1\\\}^\{n\}\\to\\\{0,1\\\}^\{n\-1\},π​\(x\)i:=xi⊕ai​xj\\pi\(x\)\_\{i\}:=x\_\{i\}\\oplus a\_\{i\}x\_\{j\}fori≠ji\\neq j\. Its kernel is exactly\{0,a\}\\\{0,a\\\}: ifxj=0x\_\{j\}=0thenπ​\(x\)=0\\pi\(x\)=0forcesx=0x=0; ifxj=1x\_\{j\}=1thenπ​\(x\)=0\\pi\(x\)=0forcesxi=aix\_\{i\}=a\_\{i\}for everyi≠ji\\neq j, givingx=ax=a\. Being a linear surjection with a two\-element kernel,π\\piis exactly 2\-to\-1, with fibers\{y,y⊕a\}\\\{y,y\\oplus a\\\}\. Lethhbe a bent function on\{0,1\}n−1\\\{0,1\\\}^\{n\-1\}\(for instance the inner\-product functionh​\(y\)=y1​y2⊕⋯⊕yn−2​yn−1h\(y\)=y\_\{1\}y\_\{2\}\\oplus\\cdots\\oplus y\_\{n\-2\}y\_\{n\-1\}, defined whenevern−1n\-1is even\[[21](https://arxiv.org/html/2608.10420#bib.bib21)\]\), and setf​\(x\):=h​\(π​\(x\)\)f\(x\):=h\(\\pi\(x\)\)\. Sincea∈ker⁡πa\\in\\ker\\pi,f​\(x⊕a\)=h​\(π​\(x\)⊕π​\(a\)\)=h​\(π​\(x\)\)=f​\(x\)f\(x\\oplus a\)=h\(\\pi\(x\)\\oplus\\pi\(a\)\)=h\(\\pi\(x\)\)=f\(x\), soa∈L0​\(f\)a\\in L\_\{0\}\(f\)\. Forb∉\{0,a\}b\\notin\\\{0,a\\\},v:=π​\(b\)≠0v:=\\pi\(b\)\\neq 0; bentness meansh​\(y⊕v\)⊕h​\(y\)h\(y\\oplus v\)\\oplus h\(y\)is non\-constant as a function ofyy, and sinceπ\\piis surjective and 2\-to\-1,f​\(x⊕b\)⊕f​\(x\)=h​\(π​\(x\)⊕v\)⊕h​\(π​\(x\)\)f\(x\\oplus b\)\\oplus f\(x\)=h\(\\pi\(x\)\\oplus v\)\\oplus h\(\\pi\(x\)\)takes the same set of values, with multiplicity doubled, asyyranges over\{0,1\}n−1\\\{0,1\\\}^\{n\-1\}; hence it is non\-constant inxx, sob∉L0​\(f\)b\\notin L\_\{0\}\(f\)\. ∎

Computationally verified; see[AppendixB](https://arxiv.org/html/2608.10420#A2)\. Proposition[5\.18](https://arxiv.org/html/2608.10420#S5.Thmtheorem18)rules out the strongest form of a natural shortcut: that a nontrivial automorphism, when one exists, can always be found by scanning low\-weight candidates, collapsingNontriv\-Autinto a search over polynomially many witnesses\. It leaves open a weaker form, restricting the search to whatever candidates the circuit’s own syntactic structure exposes rather than to low\-weight vectors as such; Proposition[5\.18](https://arxiv.org/html/2608.10420#S5.Thmtheorem18)’s own witness is exposed exactly this way \(the linear layerπ\\piis visible inff’s description\), so defeating the weak form requires anffwhose unique nonzero automorphism is not merely large in weight but unrecoverable from the circuit by any polynomial\-time syntactic analysis, a circuit\-complexity lower bound in its own right that we do not attempt here\.

We turn last to the flip\-bit decomposition, which does not need the linear structure above: for anyS⊆\{0,1\}n∖\{0\}S\\subseteq\\\{0,1\\\}^\{n\}\\setminus\\\{0\\\}\(not necessarily a subspace\), every nonzero vector has a unique leading11, soNontriv\-Aut​\(f\)\\textup\{\{Nontriv\-Aut\}\}\(f\)decomposes as⋁i=1nQi​\(f\)\\bigvee\_\{i=1\}^\{n\}Q\_\{i\}\(f\), where

Qi\(f\):L0\(f\)∩\{a:a1=⋯=ai−1=0,ai=1\}≠∅\.Q\_\{i\}\(f\):\\quad L\_\{0\}\(f\)\\cap\\\{a:a\_\{1\}=\\dots=a\_\{i\-1\}=0,\\ a\_\{i\}=1\\\}\\neq\\emptyset\.Computationally verified; see[AppendixB](https://arxiv.org/html/2608.10420#A2)\. Ati=ni=n, the slice\{a:a1=⋯=an−1=0,an=1\}\\\{a:a\_\{1\}=\\dots=a\_\{n\-1\}=0,a\_\{n\}=1\\\}has exactly one element, soQn​\(f\)Q\_\{n\}\(f\)is literallyDead\-Var​\(C,n\)\\textup\{\{Dead\-Var\}\}\(C,n\)restated\. Computationally verified; see[AppendixB](https://arxiv.org/html/2608.10420#A2)\.

###### Proposition 5\.19\.

For every1≤i<n1\\leq i<n,QiQ\_\{i\}is coNP\-hard\.

###### Proof\.

Reduce fromunsat: givenχ​\(z1,…,zk\)\\chi\(z\_\{1\},\\dots,z\_\{k\}\), setn=\(i−1\)\+1\+kn=\(i\-1\)\+1\+k, positions1,…,i−11,\\dots,i\-1dummy \(the circuit ignores them\), positioniiplaying the role ofxix\_\{i\}above, and positionsi\+1,…,ni\{\+\}1,\\dots,nholdingzz;f​\(dummy,xi,z\):=xi∧χ​\(z\)f\(\\mathrm\{dummy\},x\_\{i\},z\):=x\_\{i\}\\wedge\\chi\(z\)\.Qi​\(f\)Q\_\{i\}\(f\)’s witnesses are exactly the vectors witha1=⋯=ai−1=0a\_\{1\}=\\dots=a\_\{i\-1\}=0andai=1a\_\{i\}=1, so the dummy coordinates of any witness are forced to0and contribute nothing \(the circuit does not depend on them\), leavingQi​\(f\)Q\_\{i\}\(f\)equivalent to∃b∈\{0,1\}k:∀xi,z​xi∧χ​\(z\)=\(¬xi\)∧χ​\(z⊕b\)\\exists b\\in\\\{0,1\\\}^\{k\}:\\forall x\_\{i\},z\\;\\;x\_\{i\}\\wedge\\chi\(z\)=\(\\lnot x\_\{i\}\)\\wedge\\chi\(z\\oplus b\)\. Checkingxi=0x\_\{i\}=0forcesχ​\(z⊕b\)=0\\chi\(z\\oplus b\)=0for everyzz, and checkingxi=1x\_\{i\}=1forcesχ​\(z\)=0\\chi\(z\)=0for everyzz; both together, for any fixedbb, hold exactly whenχ\\chiis unsatisfiable, and unsatisfiability makes them hold for everybb\. SoQi​\(f\)Q\_\{i\}\(f\)holds iffχ\\chiis unsatisfiable, regardless of any accidental symmetry ofχ\\chiitself:QiQ\_\{i\}’s witness set is restricted, by definition, to vectors with leading11at positioniiexactly, which excludes both the dummy\-flip witnesses and theχ\\chi\-internal\-symmetry witnesses that broke Corollary[5\.7](https://arxiv.org/html/2608.10420#S5.Thmtheorem7)’s unrestricted construction\. ∎

This reduction is immune to Corollary[5\.7](https://arxiv.org/html/2608.10420#S5.Thmtheorem7)’s gap for a structural reason worth stating plainly:QiQ\_\{i\}restricts attention to one coset of witnesses \(leading11atii\), so a candidate automorphism with leading11elsewhere, whether from a dummy position or fromχ\\chi’s own symmetry, is simply not inQiQ\_\{i\}’s domain of discourse\. It does not, however, repairNontriv\-Aut=⋁iQi\\textup\{\{Nontriv\-Aut\}\}=\\bigvee\_\{i\}Q\_\{i\}’s hardness in general: the same dummy\-flip andχ\\chi\-symmetry witnesses thatQiQ\_\{i\}excludes are exactly what can make some*other*QjQ\_\{j\}true regardless ofχ\\chi’s satisfiability, so the disjunction inherits the same gap the individualQiQ\_\{i\}avoids\.QiQ\_\{i\}tracksunsatexactly, with the dummy positions’ andχ\\chi’s own symmetry making no difference to the verdict, exactly as the proof predicts, including under adversarial choices ofχ\\chi\(the constant formulas andχ=parity\\chi=\\mathrm\{parity\}, among the most internally symmetric formulas possible\)\. Computationally verified; see[AppendixB](https://arxiv.org/html/2608.10420#A2)\.

Collectively,⋁iQi\\bigvee\_\{i\}Q\_\{i\}gives no asymptotic improvement overNontriv\-Autitself: onlyQnQ\_\{n\}collapses, to a problem we already knew was coNP\-complete, and everyQiQ\_\{i\}withi<ni<nis exactly as hard as the undecomposed problem, so the hardest disjunct still dominates\. A natural self\-reduction attempt, extending a partial witness one coordinate at a time using aDead\-Varoracle the waysat’s self\-reducibility extends a partial assignment using a satisfiability oracle, does not go through: “can this partial vector be extended to a full element ofL0​\(f\)L\_\{0\}\(f\)” unfolds to∃\(remaining coordinates\)​∀x:f​\(x\)=f​\(x⊕a\)\\exists\(\\text\{remaining coordinates\}\)\\forall x:f\(x\)=f\(x\\oplus a\), aΣ2𝗉\\Sigma\_\{2\}^\{\\mathsf\{p\}\}statement, not a coNP one, so it cannot be answered by the coNP oracleDead\-Varalready supplies\. Deciding which partial extension is promising requires exactly the kind of access toL0​\(f\)L\_\{0\}\(f\)that would already solveNontriv\-Aut\.

### 5\.5TheVal\-Isocollapse theorem

Boolean and formula isomorphism is a much\-studied cousin ofNontriv\-Aut: Borchert, Ranjan, and Stephan, and later Agrawal and Thierauf\[[1](https://arxiv.org/html/2608.10420#bib.bib1)\], ask whether two circuits are related by a*position*permutation \(π∈Sym​\(N\)\\pi\\in\\mathrm\{Sym\}\(N\), not a value permutation in∏i=1nSym​\(Si\)\\prod\_\{i=1\}^\{n\}\\mathrm\{Sym\}\(S\_\{i\}\)\), and systematized further by Böhler, Creignou, Galota, Reith, Schnoor, and Vollmer\[[5](https://arxiv.org/html/2608.10420#bib.bib5)\]across every restricted set of connectives\. That problem sits in the same coNP\-hard\-to\-Σ2𝗉\\Sigma\_\{2\}^\{\\mathsf\{p\}\}rangeNontriv\-Autdoes, using the same frozen\-variable technique for the lower bound, and Agrawal and Thierauf proved it is unlikely to reach the top of that range\. We port their argument to our setting\.

###### Definition 5\.20\(Val\-Iso\)\.

Given circuitsC1,C2C\_\{1\},C\_\{2\}over the same∏iSi\\prod\_\{i\}S\_\{i\}, with indicator functionsf1,f2f\_\{1\},f\_\{2\},Val\-Iso\(C1,C2\)\(C\_\{1\},C\_\{2\}\)holds if∃σ∈∏i=1nSym​\(Si\):f1​\(σ⋅x\)=f2​\(x\)\\exists\\sigma\\in\\prod\_\{i=1\}^\{n\}\\mathrm\{Sym\}\(S\_\{i\}\):f\_\{1\}\(\\sigma\\cdot x\)=f\_\{2\}\(x\)for everyxx\. In the Boolean case this is∃a∈\{0,1\}n:f1​\(x⊕a\)=f2​\(x\)\\exists a\\in\\\{0,1\\\}^\{n\}:f\_\{1\}\(x\\oplus a\)=f\_\{2\}\(x\)for everyxx, the two\-object counterpart ofL0L\_\{0\}\.

###### Lemma 5\.21\(Orbit uniformity\)\.

If∃a0:f1​\(x\)=f2​\(x⊕a0\)\\exists a\_\{0\}:f\_\{1\}\(x\)=f\_\{2\}\(x\\oplus a\_\{0\}\)for everyxx, the random variables “a↦f1\(⋅⊕a\)a\\mapsto f\_\{1\}\(\\cdot\\oplus a\)” and “a↦f2\(⋅⊕a\)a\\mapsto f\_\{2\}\(\\cdot\\oplus a\),” foraauniform on\{0,1\}n\\\{0,1\\\}^\{n\}, have identical distributions\. If no sucha0a\_\{0\}exists, the orbits\{f1\(⋅⊕a\):a\}\\\{f\_\{1\}\(\\cdot\\oplus a\):a\\\}and\{f2\(⋅⊕a\):a\}\\\{f\_\{2\}\(\\cdot\\oplus a\):a\\\}are disjoint\.

###### Proof\.

Iff2=f1\(⋅⊕a0\)f\_\{2\}=f\_\{1\}\(\\cdot\\oplus a\_\{0\}\), the orbit off2f\_\{2\}equals\{f1\(⋅⊕\(a0⊕a\)\):a\}\\\{f\_\{1\}\(\\cdot\\oplus\(a\_\{0\}\\oplus a\)\):a\\\}; sincea↦a0⊕aa\\mapsto a\_\{0\}\\oplus ais a bijection of\{0,1\}n\\\{0,1\\\}^\{n\}that also preserves the uniform distribution, this is the same set, with the same uniform distribution over it, as the orbit off1f\_\{1\}\. The second claim is the standard fact that two orbits of a group action either coincide or are disjoint: a common elementf1\(⋅⊕a\)=f2\(⋅⊕a′\)f\_\{1\}\(\\cdot\\oplus a\)=f\_\{2\}\(\\cdot\\oplus a^\{\\prime\}\)would givef2=f1\(⋅⊕\(a⊕a′\)\)f\_\{2\}=f\_\{1\}\(\\cdot\\oplus\(a\\oplus a^\{\\prime\}\)\), contradicting non\-isomorphism\. ∎

Computationally verified; see[AppendixB](https://arxiv.org/html/2608.10420#A2)\.

###### Theorem 5\.22\.

Val\-Isois notΣ2𝗉\\Sigma\_\{2\}^\{\\mathsf\{p\}\}\-complete unless𝖯𝖧=Σ3𝗉\\mathsf\{PH\}=\\Sigma\_\{3\}^\{\\mathsf\{p\}\}\.

###### Proof structure\.

We adapt Agrawal and Thierauf’s six\-step argument for Boolean formula isomorphism, replacingSym​\(N\)\\mathrm\{Sym\}\(N\)by∏i=1nSym​\(Si\)\\prod\_\{i=1\}^\{n\}\\mathrm\{Sym\}\(S\_\{i\}\)throughout\.

1. 1\.*Randomize the instance\.*The verifier picksr∈\{1,2\}r\\in\\\{1,2\\\}and uniforma∈\{0,1\}na\\in\\\{0,1\\\}^\{n\}, and formsg:=fr\(⋅⊕a\)g:=f\_\{r\}\(\\cdot\\oplus a\): a purely syntactic rewrite, no oracle needed\. \(Group\-independent step\.\)
2. 2\.*The naive protocol leaksrr\.*Sendingggdirectly can leakrrthrough syntactic invariants unrelated toaa\(gate count, for formulas; here, any statistic of the shifted circuit that a bare shift does not equalize betweenf1f\_\{1\}andf2f\_\{2\}\)\. \(Group\-independent diagnosis, present for either group\.\)
3. 3\.*Launderggthrough a semantically canonical randomized oracle\.*Bshouty, Cleve, Gavaldà, Kannan, and Tamon\[[8](https://arxiv.org/html/2608.10420#bib.bib8)\]give a probabilistic polynomial\-time algorithm, with an𝖭𝖯\\mathsf\{NP\}oracle, that on any Boolean circuit outputs, with probability at least2/32/3, an equivalent circuit, and never outputs an inequivalent one\. Its defining structural property, stated explicitly by Agrawal and Thierauf\[[1](https://arxiv.org/html/2608.10420#bib.bib1)\]in their restatement of the result, is stronger than equality of output distributions: the learner touches its input only through semantically answered queries \(equivalence tests, and counterexamples extracted canonically through the𝖭𝖯\\mathsf\{NP\}oracle\), so*on each fixed random path the output is identical across all representatives of the input’s equivalence class*, in their words “on each random path the output remains the same on anyF′∈\[F\]F^\{\\prime\}\\in\[F\]\.” Agrawal and Thierauf also state the circuit analogue explicitly \(their Section 5: Bshouty et al\. show the analog result for circuits, from which the interactive proof adapts to circuit isomorphism\)\. This is the one step specific to the object type \(Boolean circuits\), not to the group\.
4. 4\.*Correctness is a pure orbit fact\.*By Lemma[5\.21](https://arxiv.org/html/2608.10420#S5.Thmtheorem21), iff1f\_\{1\}andf2f\_\{2\}are isomorphic the laundered message’s distribution does not depend onrr, so the prover guessesrrcorrectly with probability at most1/21/2; if they are not, the orbits are disjoint and an unbounded prover can always tell them apart\. \(Group\-independent given step 3’s semantic\-only dependence\.\)
5. 5\.*Collapse rounds\.*Goldwasser–Sipser public\-coin conversion\[[13](https://arxiv.org/html/2608.10420#bib.bib13)\]and Babai’s collapse of constant\-round𝖠𝖬\\mathsf\{AM\}to one round\[[2](https://arxiv.org/html/2608.10420#bib.bib2)\]both hold relative to an𝖭𝖯\\mathsf\{NP\}oracle, givingVal\-Iso¯∈𝖠𝖬𝖭𝖯\\overline\{\\textup\{\{Val\-Iso\}\}\}\\in\\mathsf\{AM\}^\{\\mathsf\{NP\}\}\. \(Group\-independent, standard\.\)
6. 6\.*Apply the barrier\.*𝖠𝖬𝖭𝖯=𝖡𝖯⋅Σ2𝗉\\mathsf\{AM\}^\{\\mathsf\{NP\}\}=\\mathsf\{BP\}\\cdot\\Sigma\_\{2\}^\{\\mathsf\{p\}\}, and Schöning’s theorem that noΠ2𝗉\\Pi\_\{2\}^\{\\mathsf\{p\}\}\-complete set lies in𝖡𝖯⋅Σ2𝗉\\mathsf\{BP\}\\cdot\\Sigma\_\{2\}^\{\\mathsf\{p\}\}unless𝖯𝖧\\mathsf\{PH\}collapses, applied toVal\-Iso¯\\overline\{\\textup\{\{Val\-Iso\}\}\}, gives the claim\.

∎

Only step 3 is specific to Boolean circuits rather than generic to any group action, and it is exactly the step Agrawal and Thierauf state as holding for circuits directly, not only formulas, so no separate formula\-to\-circuit translation is needed\. Step 6 is a black box we do not re\-derive, taken at the same confidence level Agrawal and Thierauf themselves take it: their result depends on Schöning’s\[[24](https://arxiv.org/html/2608.10420#bib.bib24)\]collapse barrier without re\-proving it\.

### 5\.6A collapse theorem forNontriv\-Autitself

Theorem[5\.22](https://arxiv.org/html/2608.10420#S5.Thmtheorem22)is about two circuits, not one; it does not by itself say anything aboutNontriv\-Aut\. Agrawal and Thierauf’s own route from the two\-object case back to the one\-object case \(their Boolean Automorphism problem, exactly ourNontriv\-AutunderSym​\(N\)\\mathrm\{Sym\}\(N\)instead of∏i=1nSym​\(Si\)\\prod\_\{i=1\}^\{n\}\\mathrm\{Sym\}\(S\_\{i\}\)\) uses a labeling gadget that pins one variable’s identity by giving it an equivalence class no other variable can match, a technique that fundamentally needsSym​\(N\)\\mathrm\{Sym\}\(N\)to be a group that permutes*named*objects\.∏i=1nSym​\(Si\)\\prod\_\{i=1\}^\{n\}\\mathrm\{Sym\}\(S\_\{i\}\)acting by coordinatewiseXOR\\mathrm\{XOR\}has no such objects to name: it acts freely and transitively on\{0,1\}n\\\{0,1\\\}^\{n\}itself, not on any set ofnnlabeled positions, and four direct attempts at transplanting the labeling gadget each fail on the same point, confirmed on small instances rather than left as an intuition \([AppendixA](https://arxiv.org/html/2608.10420#A1)\)\.

The following result instead adapts the*other*proof Agrawal and Thierauf point to but do not themselves use for Boolean isomorphism: a direct, single\-object statistical argument in the spirit of Schöning’s original proof that graph isomorphism sits in𝖠𝖬\\mathsf\{AM\}\[[23](https://arxiv.org/html/2608.10420#bib.bib23)\]\. We work with the standard Goldwasser–Sipser set\-lower\-bound formulation of that technique\[[13](https://arxiv.org/html/2608.10420#bib.bib13)\]rather than Schöning’s original presentation, cross\-checked against Agrawal and Thierauf’s own citation of it\.

###### Definition 5\.23\.

WriteTRIV​\-​AUT\\mathrm\{TRIV\\text\{\-\}AUT\}for the complement ofNontriv\-Aut\.

###### Theorem 5\.24\.

TRIV​\-​AUT∈𝖠𝖬𝖭𝖯=𝖡𝖯⋅Σ2𝗉\\mathrm\{TRIV\\text\{\-\}AUT\}\\in\\mathsf\{AM\}^\{\\mathsf\{NP\}\}=\\mathsf\{BP\}\\cdot\\Sigma\_\{2\}^\{\\mathsf\{p\}\}\. Consequently,Nontriv\-Autis notΣ2𝗉\\Sigma\_\{2\}^\{\\mathsf\{p\}\}\-complete unless𝖯𝖧=Σ3𝗉\\mathsf\{PH\}=\\Sigma\_\{3\}^\{\\mathsf\{p\}\}\.

###### Proof\.

WriteOrbit\(f\):=\{f\(⋅⊕a\):a∈\{0,1\}n\}\\mathrm\{Orbit\}\(f\):=\\\{f\(\\cdot\\oplus a\):a\\in\\\{0,1\\\}^\{n\}\\\}; by orbit\-stabilizer,\|Orbit​\(f\)\|=2n/\|L0​\(f\)\|\|\\mathrm\{Orbit\}\(f\)\|=2^\{n\}/\|L\_\{0\}\(f\)\|, and by Corollary[5\.11](https://arxiv.org/html/2608.10420#S5.Thmtheorem11)this is always a power of22\.TRIV​\-​AUT​\(f\)\\mathrm\{TRIV\\text\{\-\}AUT\}\(f\)holds exactly when\|Orbit​\(f\)\|=2n\|\\mathrm\{Orbit\}\(f\)\|=2^\{n\}, the maximum possible value, so the claim reduces to a Goldwasser–Sipser set lower bound protocol onOrbit​\(f\)\\mathrm\{Orbit\}\(f\)with thresholdK=2nK=2^\{n\}, usingL0​\(f\)L\_\{0\}\(f\)’s power\-of\-two structure to avoid the usual promise gap\. The obstacle is representational: orbit elements are functions with2n2^\{n\}\-bit truth tables, and a syntactically shifted circuit is only a polynomial\-size handle on one, so a naive protocol would have to hash syntax rather than semantics, reproducing exactly the gap between circuit equivalence and circuit equality that makesDead\-VarcoNP\-hard in the first place\.

The fix reuses the Bshouty et al\. laundering black box from Theorem[5\.22](https://arxiv.org/html/2608.10420#S5.Thmtheorem22)’s step 3, whose defining guarantee is stronger than mere high accuracy: on a Boolean circuitggand a random tape, it*never outputs a circuit that is not equivalent togg*, and only occasionally aborts instead of succeeding\[[8](https://arxiv.org/html/2608.10420#bib.bib8)\]\. Fix once and for all a sequence oft=⌈2​n/log2⁡3⌉t=\\lceil 2n/\\log\_\{2\}3\\rceilrandom tapesR=\(r1,…,rt\)R=\(r\_\{1\},\\dots,r\_\{t\}\), shared across every candidate shiftaarather than redrawn per shift, and definecanon∗​\(g;R\)\\mathrm\{canon\}^\{\*\}\(g;R\)as the output of the launderer on the*first*rir\_\{i\}\(in the fixed orderr1,…,rtr\_\{1\},\\dots,r\_\{t\}\) that does not abort, or “abort” if allttdo\. Two properties of this fixed\-tape construction carry the argument\. First,*same\-class merging*\. This needs, and gets, more than equality of output distributions: it needs the per\-random\-path invariance that Agrawal and Thierauf state for the launderer \(“on each random path the output remains the same on anyF′∈\[F\]F^\{\\prime\}\\in\[F\]”\[[1](https://arxiv.org/html/2608.10420#bib.bib1)\]\), which holds because the launderer reads its input only through semantic queries, with counterexamples extracted by a canonical rule \(lexicographically least, via prefix search on the𝖭𝖯\\mathsf\{NP\}oracle\) so that even the oracle’s answers depend on the function, never the circuit\. On a fixed taperir\_\{i\}the launderer’s entire execution is then a function of the input’s equivalence class, and so is its abort\-or\-output outcome; hence for any two shiftsa,a′a,a^\{\\prime\}withf\(⋅⊕a\)=f\(⋅⊕a′\)f\(\\cdot\\oplus a\)=f\(\\cdot\\oplus a^\{\\prime\}\), the first\-successful tape index agrees andcanon∗\(f\(⋅⊕a\);R\)=canon∗\(f\(⋅⊕a′\);R\)\\mathrm\{canon\}^\{\*\}\(f\(\\cdot\\oplus a\);R\)=\\mathrm\{canon\}^\{\*\}\(f\(\\cdot\\oplus a^\{\\prime\}\);R\)for every fixedRR, so the number of distinct representatives produced asaaranges over\{0,1\}n\\\{0,1\\\}^\{n\}is at most\|Orbit​\(f\)\|\|\\mathrm\{Orbit\}\(f\)\|\. \(The verification scripts for this section implement the launderer with exactly this semantics, keyed on the truth table rather than the circuit; see[AppendixB](https://arxiv.org/html/2608.10420#A2)\.\) Second,*no false merging across classes*: because the launderer never outputs a circuit inequivalent to its input, two shifts landing in genuinely different classes can never launder \(on any tape\) to the same representative\. By geometric amplification over the per\-tape≥2/3\\geq 2/3success rate,canon∗​\(g;R\)\\mathrm\{canon\}^\{\*\}\(g;R\)aborts with probability at most2−2​n2^\{\-2n\}over the random choice ofRR; a union bound over the2n2^\{n\}possible shifts bounds the probability that laundering some shift offfaborts by2−n2^\{\-n\}\.

The Goldwasser–Sipser instantiation is fully explicit\. Lets​\(n\)s\(n\)be the polynomial bound on the launderer’s output size, fix a binary encoding of circuits padded to exactlyLc:=s​\(n\)L\_\{c\}:=s\(n\)bits, and letW⊆\{0,1\}LcW\\subseteq\\\{0,1\\\}^\{L\_\{c\}\}be the set of representatives realizable ascanon∗\(f\(⋅⊕a\);R\)\\mathrm\{canon\}^\{\*\}\(f\(\\cdot\\oplus a\);R\)asaaranges over the2n2^\{n\}shifts\. Arthur drawshhuniformly from the affine familyh​\(x\)=A​x⊕bh\(x\)=Ax\\oplus bwithA∈𝔽2m×LcA\\in\\mathbb\{F\}\_\{2\}^\{m\\times L\_\{c\}\},b∈𝔽2mb\\in\\mathbb\{F\}\_\{2\}^\{m\}, pairwise independent, at output lengthm:=n\+1m:=n\+1, and sends\(h,R\)\(h,R\); Merlin returns a shiftaa; the verifier recomputescanon∗\(f\(⋅⊕a\);R\)\\mathrm\{canon\}^\{\*\}\(f\(\\cdot\\oplus a\);R\)itself, with the same fixed tapes and first\-success rule \(deterministic polynomial time, given the𝖭𝖯\\mathsf\{NP\}oracle answering the launderer’s equivalence tests and lexicographically\-least counterexample queries\), and accepts iff the result hashes to0m0^\{m\}\.*Soundness*: same\-class merging caps\|W\|≤\|Orbit​\(f\)\|\|W\|\\leq\|\\mathrm\{Orbit\}\(f\)\|, and whenTRIV​\-​AUT​\(f\)\\mathrm\{TRIV\\text\{\-\}AUT\}\(f\)fails,\|Orbit​\(f\)\|≤2n−1\|\\mathrm\{Orbit\}\(f\)\|\\leq 2^\{n\-1\}by the power\-of\-two law, so a union bound gives acceptance probability at most\|W\|/2m≤2n−1/2n\+1=1/4\|W\|/2^\{m\}\\leq 2^\{n\-1\}/2^\{n\+1\}=1/4\.*Completeness*: whenTRIV​\-​AUT​\(f\)\\mathrm\{TRIV\\text\{\-\}AUT\}\(f\)holds, all2n2^\{n\}shifts lie in distinct classes, so no false merging plus the2−n2^\{\-n\}abort bound give\|W\|=2n\|W\|=2^\{n\}except with probability2−n2^\{\-n\}overRR; by inclusion–exclusion under pairwise independence, acceptance probability is at least\|W\|/2m−\|W\|2/\(2⋅22​m\)=1/2−1/8=3/8\|W\|/2^\{m\}\-\|W\|^\{2\}/\(2\\cdot 2^\{2m\}\)=1/2\-1/8=3/8, minus the2−n2^\{\-n\}abort term\. The3/83/8\-versus\-1/41/4gap is a constant; a constant number of parallel hash challenges inside the same round, accepted by majority, amplifies it to2/32/3versus1/31/3while keeping the protocol one\-round and public\-coin\. Every verifier step other than the launderer’s internal queries is oracle\-free; the launderer’s internal queries \(near\-uniform sampling within an equivalence class, and finding a counterexample when a candidate is wrong\) are each answerable with a polynomial number of adaptive𝖭𝖯\\mathsf\{NP\}queries, so the whole verifier is a𝖯𝖭𝖯\\mathsf\{P\}^\{\\mathsf\{NP\}\}machine, giving a one\-round, public\-coin protocol with an𝖭𝖯\\mathsf\{NP\}\-oracle verifier,TRIV​\-​AUT∈IP​\[1\]𝖭𝖯=𝖠𝖬𝖭𝖯\\mathrm\{TRIV\\text\{\-\}AUT\}\\in\\mathrm\{IP\}\[1\]^\{\\mathsf\{NP\}\}=\\mathsf\{AM\}^\{\\mathsf\{NP\}\}\. Unlike Theorem[5\.22](https://arxiv.org/html/2608.10420#S5.Thmtheorem22), this protocol never needs to hide which of two objects is which, so it is public\-coin and one\-round from the start, with no separate collapse step\. The identity𝖠𝖬𝖭𝖯=𝖡𝖯⋅Σ2𝗉\\mathsf\{AM\}^\{\\mathsf\{NP\}\}=\\mathsf\{BP\}\\cdot\\Sigma\_\{2\}^\{\\mathsf\{p\}\}and Schöning’s barrier, exactly as in Theorem[5\.22](https://arxiv.org/html/2608.10420#S5.Thmtheorem22)’s step 6, complete the argument\. ∎

The fixed\-tapecanon∗\\mathrm\{canon\}^\{\*\}construction was checked separately from the full protocol, and the full protocol was then checked end to end on real and synthetic instances, including a hand\-built copy of BDD\-OIA’s absorption structure\. Computationally verified; see[AppendixB](https://arxiv.org/html/2608.10420#A2)\.

Between the randomized lower bound and the collapse ceiling sits the section’s inheritance to future work, and it is handed over mapped, not merely left\.[AppendixA](https://arxiv.org/html/2608.10420#A1)distills a systematic sweep of the standard toolkits, direct encodings, interactive protocols, and linear algebra, into three structural facts any approach to the gap must clear:Aut​\(ΦC\)\\mathrm\{Aut\}\(\\Phi\_\{C\}\)is always a subgroup where a genericΣ2𝗉\\Sigma\_\{2\}^\{\\mathsf\{p\}\}witness set is not;∏i=1nSym​\(Si\)\\prod\_\{i=1\}^\{n\}\\mathrm\{Sym\}\(S\_\{i\}\)acts freely on assignments and names no objects, which starves every label\-and\-tag technique; and any access toL0​\(f\)L\_\{0\}\(f\)stronger than a pointwise oracle is already as hard to obtain asNontriv\-Autitself\. Theorem[5\.24](https://arxiv.org/html/2608.10420#S5.Thmtheorem24)’s laundering protocol succeeds precisely by needing none of the three\.

### 5\.7Deterministic completeness on monotone circuits

The gap between randomized and deterministic hardness is not uniform across circuit classes\. Section[5\.3](https://arxiv.org/html/2608.10420#S5.SS3)traced the failure of every deterministic gadget to a single phenomenon: the source formulaχ\\chican carry an accidental internal XOR symmetry, invisible to any fixed transformation, that hands the constructed instance a nontrivial automorphism unrelated to the question being encoded\. On monotone circuits that phenomenon cannot occur at all\. The objectL0​\(f\)L\_\{0\}\(f\)is classical in cryptography under the name*linear structures*offf\[[18](https://arxiv.org/html/2608.10420#bib.bib18),[9](https://arxiv.org/html/2608.10420#bib.bib9)\], where a large linear space signals a weak S\-box\. The following characterization for monotone functions appears to be new despite three decades of work on linear structures, and it is the keystone of this subsection: it collapses automorphism existence, aΣ2𝗉\\Sigma\_\{2\}^\{\\mathsf\{p\}\}\-shaped question in general, to dead\-variable detection\.

###### Lemma 5\.26\(Monotone functions cannot camouflage\)\.

Letf:\{0,1\}n→\{0,1\}f:\\\{0,1\\\}^\{n\}\\to\\\{0,1\\\}be monotone\. ThenL0​\(f\)L\_\{0\}\(f\)is exactly the set of shift vectors supported onff’s dead coordinates\. In particular, a monotoneffwith every coordinate alive hasL0​\(f\)=\{0\}L\_\{0\}\(f\)=\\\{0\\\}\.

###### Proof\.

Shifts supported on dead coordinates never change the value offf, so they lie inL0​\(f\)L\_\{0\}\(f\)\. Conversely leta∈L0​\(f\)a\\in L\_\{0\}\(f\)and letxxbe arbitrary\. The pointsx∧a¯x\\wedge\\bar\{a\}and\(x∧a¯\)⊕a\(x\\wedge\\bar\{a\}\)\\oplus aare related by the shift, and sincex∧a¯x\\wedge\\bar\{a\}andaahave disjoint supports,\(x∧a¯\)⊕a=\(x∧a¯\)∨a\(x\\wedge\\bar\{a\}\)\\oplus a=\(x\\wedge\\bar\{a\}\)\\vee a\. Monotonicity now sandwiches:

f​\(x∧a¯\)≤f​\(x\)≤f​\(x∨a\)≤f​\(\(x∧a¯\)∨a\)=f​\(x∧a¯\),f\(x\\wedge\\bar\{a\}\)\\;\\leq\\;f\(x\)\\;\\leq\\;f\(x\\vee a\)\\;\\leq\\;f\\big\(\(x\\wedge\\bar\{a\}\)\\vee a\\big\)\\;=\\;f\(x\\wedge\\bar\{a\}\),usingx∧a¯≤x≤x∨a≤\(x∧a¯\)∨ax\\wedge\\bar\{a\}\\leq x\\leq x\\vee a\\leq\(x\\wedge\\bar\{a\}\)\\vee acoordinatewise andaa\-shift\-invariance at the last step\. Sof​\(x\)=f​\(x∧a¯\)f\(x\)=f\(x\\wedge\\bar\{a\}\)for everyxx:ffdoes not depend on any coordinate insupp​\(a\)\\mathrm\{supp\}\(a\), and every such coordinate is dead\. ∎

###### Theorem 5\.27\(Deterministic completeness on monotone circuits\)\.

Restricted to monotone circuits,Nontriv\-Autis coNP\-complete under deterministic polynomial\-time many\-one reductions\.

###### Proof\.

*Membership\.*By Lemma[5\.26](https://arxiv.org/html/2608.10420#S5.Thmtheorem26),Nontriv\-Aut​\(f\)\\textup\{\{Nontriv\-Aut\}\}\(f\)holds for monotoneffiff some coordinate is dead\. The complement asks that every coordinate be alive, which has a polynomial witness: one pointx\(i\)x^\{\(i\)\}per coordinate withf​\(x\(i\)\)≠f​\(x\(i\)⊕ei\)f\(x^\{\(i\)\}\)\\neq f\(x^\{\(i\)\}\\oplus e\_\{i\}\)\. Hence the restricted problem is in coNP, already below the generalΣ2𝗉\\Sigma\_\{2\}^\{\\mathsf\{p\}\}upper bound of Theorem[5\.4](https://arxiv.org/html/2608.10420#S5.Thmtheorem4)\.

*Hardness\.*Reduce fromunsat\. Given a 3\-CNFφ​\(z1,…,zm\)\\varphi\(z\_\{1\},\\dots,z\_\{m\}\), introduce two railsyj,yj′y\_\{j\},y^\{\\prime\}\_\{j\}per variable and one further positionx∗x\_\{\*\}\. Letφ~\\widetilde\{\\varphi\}beφ\\varphiwith each positive literalzjz\_\{j\}replaced byyjy\_\{j\}and each negated literal¬zj\\neg z\_\{j\}byyj′y^\{\\prime\}\_\{j\}\(a monotone formula\), and set

A:=⋀j\(yj∨yj′\),B:=⋁j\(yj∧yj′\),h:=\(x∗∧φ~∧A\)∨B,A:=\\bigwedge\_\{j\}\(y\_\{j\}\\vee y^\{\\prime\}\_\{j\}\),\\qquad B:=\\bigvee\_\{j\}\(y\_\{j\}\\wedge y^\{\\prime\}\_\{j\}\),\\qquad h:=\\big\(x\_\{\*\}\\wedge\\widetilde\{\\varphi\}\\wedge A\\big\)\\vee B,a monotone circuit\. Every rail is alive inhhwhateverφ\\varphiis: at the point withyj′=1y^\{\\prime\}\_\{j\}=1, all other inputs0, flippingyjy\_\{j\}flipsBBand hencehh\. Andx∗x\_\{\*\}is dead iffφ~∧A≤B\\widetilde\{\\varphi\}\\wedge A\\leq Bpointwise\. If some point violates that implication, then byAAeach variable has at least one true rail and by¬B\\neg Bnone has two, so the rails encode an exact assignmentz:=yz:=y, andφ~=1\\widetilde\{\\varphi\}=1sayszzsatisfiesφ\\varphi; conversely a satisfyingzzgives the violating point\(y,y′\)=\(z,z¯\)\(y,y^\{\\prime\}\)=\(z,\\bar\{z\}\)\. Sox∗x\_\{\*\}is dead iffφ\\varphiis unsatisfiable\. By Lemma[5\.26](https://arxiv.org/html/2608.10420#S5.Thmtheorem26),hhhas a nontrivial automorphism iff it has a dead coordinate, iffx∗x\_\{\*\}is dead \(the rails never are\), iffφ\\varphiis unsatisfiable\. The mapφ↦h\\varphi\\mapsto his deterministic and polynomial\-time\. ∎

Theorem[5\.27](https://arxiv.org/html/2608.10420#S5.Thmtheorem27)is the counterpoint to this section’s central gap: the obstruction that forces Corollary[5\.7](https://arxiv.org/html/2608.10420#S5.Thmtheorem7)to randomize is precisely the camouflage that Lemma[5\.26](https://arxiv.org/html/2608.10420#S5.Thmtheorem26)rules out, so on the largest natural circuit class that forbids it, the existence question’s complexity is settled outright, with no randomness, no isolation, and no promise\. Read together with the diagnosis of[AppendixA](https://arxiv.org/html/2608.10420#A1), this locates the general case’s remaining gap exactly: it is a question about non\-monotone camouflage, not about automorphism existence per se\. Both the lemma and both directions of the reduction were checked computationally before being trusted as proofs\. Computationally verified; see[AppendixB](https://arxiv.org/html/2608.10420#A2)\.

## 6The Shortcut Geography of Trained Models

Every measurement so far is symbolic:ΦC\\Phi\_\{C\}andAut​\(ΦC\)\\mathrm\{Aut\}\(\\Phi\_\{C\}\)are computed from a rule’s combinatorial structure, never from a trained network’s actual behavior\. This section closes the loop\. Train real neurosymbolic models under ordinary weak supervision, so that a genuine reasoning shortcut in the sense of Definition[2\.1](https://arxiv.org/html/2608.10420#S2.Thmtheorem1)can actually occur\. When it occurs, does it land in the sameAut​\(ΦC\)\\mathrm\{Aut\}\(\\Phi\_\{C\}\)\-orbit as the ground truth, the case this paper’s algebra explains, or a different orbit, the case it does not?

#### Design\.

The experiment trains its models from scratch, by design\. rsbench’s released artifacts\[[7](https://arxiv.org/html/2608.10420#bib.bib7)\]\(Zenodo record 11612556\) provide images, embeddings, and generator configs but no trained checkpoints or per\-model concept predictions, and end\-to\-end control over training is what makes the comparison below exact: one fixed image pool, one uncurated pairing scheme, one held\-out yardstick shared by every model\. MNIST arithmetic is the family where the theory\-to\-training comparison can be made exact end to end: full\-domain orbit ground truth is computable for every target level, the exact semantic loss is available in closed form, and no curated split intervenes between the rule and the optimizer\. \(rsbench’s released Kandinsky package,kand\-logic\-3k, encodes a composite three\-figure rule distinct from the single six\-symbol triple[Table2](https://arxiv.org/html/2608.10420#S3.T2)measures, so it poses a different symbolic object, not a rendered version of this paper’s\.\)

### 6\.1Setup: weakly\-supervised MNIST\-Addition and MNIST\-Product

We train the standard DeepProbLog\-style MNIST\-Addition model\[[14](https://arxiv.org/html/2608.10420#bib.bib14),[7](https://arxiv.org/html/2608.10420#bib.bib7)\]: a single small CNN perception network, shared across both digit positions, maps each image to a categorical distribution over\{0,…,9\}\\\{0,\\dots,9\\\}\. No digit\-level label is ever provided\. Training supervises only the composed labely=c1​op​c2y=c\_\{1\}\\,\\mathrm\{op\}\\,c\_\{2\}, via the exact semantic lossP​\(Y=y∣x1,x2\)=∑\(c1,c2\):op​\(c1,c2\)=yp1​\(c1\)​p2​\(c2\)P\(Y\{=\}y\\mid x\_\{1\},x\_\{2\}\)=\\sum\_\{\(c\_\{1\},c\_\{2\}\):\\,\\mathrm\{op\}\(c\_\{1\},c\_\{2\}\)=y\}p\_\{1\}\(c\_\{1\}\)\\,p\_\{2\}\(c\_\{2\}\)\[[28](https://arxiv.org/html/2608.10420#bib.bib28)\], for the same two rsbench MNAdd rules already measured symbolically in[Table3](https://arxiv.org/html/2608.10420#S3.T3):sumandproduct\. We deliberately do not restrict which digit combinations appear in training, unlike rsbench’s own shortcut\-inducingshortcutmnistsplits\[[7](https://arxiv.org/html/2608.10420#bib.bib7)\]; any shortcut reported below survives standard, uncurated random pairing\.

Ten random seeds \(0–9, exceeding the pre\-specified minimum of five\) each train two independent models, one per task, on a training pool of 1,500 MNIST images per class and 6,000 random training pairs, for 20 epochs \(Adam,lr=10−3\\mathrm\{lr\}=10^\{\-3\}; training\-set label accuracy exceeds99\.8%99\.8\\%for every run\)\. All ten seeds share one fixed image pool, so cross\-seed variation reflects optimization stochasticity alone, not differing data availability\.

Evaluation uses a single fixed, stratified set of 2,000 held\-out instances, 20 for each of the 100 true digit pairs\(d1,d2\)\(d\_\{1\},d\_\{2\}\), shared across all 20 trained models so every comparison uses the same yardstick\. For each instance we compare the model’s argmax prediction\(p1,p2\)\(p\_\{1\},p\_\{2\}\)against the truth and classify it ascorrect\(\(p1,p2\)=\(d1,d2\)\(p\_\{1\},p\_\{2\}\)\{=\}\(d\_\{1\},d\_\{2\}\)\), a same\-orbit shortcut \(label\-preserving,\(p1,p2\)≠\(d1,d2\)\(p\_\{1\},p\_\{2\}\)\\neq\(d\_\{1\},d\_\{2\}\), and in the sameAut​\(Φy∗\)\\mathrm\{Aut\}\(\\Phi\_\{y^\{\*\}\}\)\-orbit as the truth\), a different\-orbit shortcut \(label\-preserving but in a different orbit\), orinvalid\(the composed label itself is wrong, not a shortcut in Definition[2\.1](https://arxiv.org/html/2608.10420#S2.Thmtheorem1)’s sense at all, the “third case” a real model can also produce\)\.

Orbit ground truth is recomputed independently in this experiment rather than trusted from[Table3](https://arxiv.org/html/2608.10420#S3.T3)’s source file, which records only orbit sizes, not the element\-level membership a specific model prediction needs\. We reuse the same validatedindep\_autgrp\_via\_nautyengine from[Section3\.1](https://arxiv.org/html/2608.10420#S3.SS1)to recover the full orbit partition for everysumandproducttarget level, and recover exactly the prior aggregate numbers as a consistency check: all 17sumlevels transitive, 31 of 32productlevels transitive, andy∗=0y^\{\*\}\{=\}0the sole exception, with orbit sizes\[9,9,1\]\[9,9,1\]matching\{\(0,0\)\}\\\{\(0,0\)\\\},\{\(0,k\):k≠0\}\\\{\(0,k\)\{:\}k\{\\neq\}0\\\}, and\{\(k,0\):k≠0\}\\\{\(k,0\)\{:\}k\{\\neq\}0\\\}exactly as reported for that target in[Section3\.3](https://arxiv.org/html/2608.10420#S3.SS3)\. A counting convention, fixed here once: the two tasks reach19\+37=5619\+37=56target values in total, but seven of them \(y∈\{0,18\}y\{\\in\}\\\{0,18\\\}forsum;\{1,25,49,64,81\}\\\{1,25,49,64,81\\\}forproduct\) are*singleton*levels whoseΦy\\Phi\_\{y\}contains exactly one concept pair, so no alternative solution exists, and transitivity and shortcuts are both vacuous there\. All level counts below refer to the 49 non\-singleton levels \(17sum\+\+32product\) that carry content\.

### 6\.2Results: predicted versus observed shortcut locations

Table 6:Ten\-seed aggregates over 2,000 held\-out instances per model \(20,000 total per task and architecture\)\. Top: the standard shared perception network \(typed rung realizable\)\. Bottom: the dual\-head control of[Section6\.4](https://arxiv.org/html/2608.10420#S6.SS4), one independent network per digit position \(componentwise rung realizable\)\. “Same\-orbit” and “diff\-orbit” are label\-preserving shortcuts \(Definition[2\.1](https://arxiv.org/html/2608.10420#S2.Thmtheorem1)’sΦC\\Phi\_\{C\}membership\) that do or do not shareAut​\(Φy∗\)\\mathrm\{Aut\}\(\\Phi\_\{y^\{\*\}\}\)’s orbit with the ground truth; “invalid” breaks the composed label and is not a shortcut at all\.sumproduces zero label\-preserving shortcuts, of either kind, in 20,000 evaluated instances across all ten seeds: every residual error breaks the composed label outright\. This is not automorphism trivially explaining every shortcut; there are none to explain\.productproduces 94, and every one of them occurs aty∗=0y^\{\*\}\{=\}0, the single level[Section3\.3](https://arxiv.org/html/2608.10420#S3.SS3)already flags asAut​\(ΦC\)\\mathrm\{Aut\}\(\\Phi\_\{C\}\)’s one non\-transitiveproductoutcome\. Across the other 48 non\-singleton levels combined \(sum’s 17 plusproduct’s remaining 31, all transitive underAut​\(ΦC\)\\mathrm\{Aut\}\(\\Phi\_\{C\}\)\), zero label\-preserving shortcuts were observed, over the 34,800 of the experiment’s 40,000 model\-instance evaluations whose true target lies at those levels \(the remainder: 3,800 evaluations atproduct’sy∗=0y^\{\*\}\{=\}0and 1,400 at the seven vacuous singleton levels\)\. The correspondence between whereAut​\(ΦC\)\\mathrm\{Aut\}\(\\Phi\_\{C\}\)’s symbolic computation predicts non\-trivial orbit structure and where a real trained model’s shortcuts actually appear is exact, not approximate, on the 20 models trained here\.[Figure2](https://arxiv.org/html/2608.10420#S6.F2)plots this correspondence directly across all 49 non\-singleton target levels, and[Section6\.4](https://arxiv.org/html/2608.10420#S6.SS4)shows the exactness is a stronger finding than it first appears, by playing the typed reading of[Definition2\.7](https://arxiv.org/html/2608.10420#S2.Thmtheorem7)against it\.

y=1y\{=\}1y=17y\{=\}17sum17/17 levels transitive, 0 shortcuts940producty∗=0y^\{\*\}\{=\}0y=72y\{=\}721/32 levels non\-transitive \(y∗=0y^\{\*\}\{=\}0\); all 94 shortcuts land theretheory: transitivetheory: non\-transitivesame\-orbit \(66,70\.2%70\.2\\%\)diff\-orbit \(28,29\.8%29\.8\\%\)typed\-ambiguous, no absorbing element \(12 levels, 0 shortcuts\)Figure 2:Observed concept\-level shortcuts \(bar height, stacked by same\-/different\-orbit\) against the componentwise transitivity of each of the 49 non\-singleton target levels \(sum: 17, top;product: 32, bottom; dark cell background marks the one level Section[3\.3](https://arxiv.org/html/2608.10420#S3.SS3)proves componentwise\-non\-transitive; open triangles mark the levels the typed reading \(Definition[2\.7](https://arxiv.org/html/2608.10420#S2.Thmtheorem7)\) additionally flags as ambiguous, the darky∗=0y^\{\*\}\{=\}0cell being the thirteenth\)\. Every one of the 94 observed shortcuts lands on the single level flagged by both readings and backed by the absorbing element, split 66 same\-orbit \(70\.2%70\.2\\%\) and 28 different\-orbit \(29\.8%29\.8\\%\); the other 48 componentwise\-transitive levels produce zero over their 34,800 model\-instance evaluations, including all twelve typed\-ambiguous levels without the absorbing element \(12,000 evaluations;[Section6\.4](https://arxiv.org/html/2608.10420#S6.SS4)\)\.Every one of the tenproductseeds produces both same\-orbit and different\-orbit shortcuts \(same\-orbit counts 4–9 and diff\-orbit counts 2–4 per seed\), not just a pooled aggregate driven by one atypical run\. Pooled,66/94=70\.2%66/94\{=\}70\.2\\%ofproduct’s shortcuts share the ground truth’s orbit and28/94=29\.8%28/94\{=\}29\.8\\%do not; per seed, the diff\-orbit share ranges from20%20\\%to50%50\\%, never zero and never dominant\.Aut​\(ΦC\)\\mathrm\{Aut\}\(\\Phi\_\{C\}\)accounts for most, but not all, of the real variation a trained model produces, and it does so consistently across seeds rather than on some seeds and not others\.

### 6\.3Mechanism: the absorbing element behind both outcomes

Table 7:Element\-level breakdown of all 94producty∗=0y^\{\*\}\{=\}0shortcuts, pooled over the 10 seeds, by which of the three orbits\{\(0,0\)\}\\\{\(0,0\)\\\},\{\(0,k\):k≠0\}\\\{\(0,k\)\{:\}k\{\\neq\}0\\\},\{\(k,0\):k≠0\}\\\{\(k,0\)\{:\}k\{\\neq\}0\\\}the true and predicted pairs occupy\.Concrete instances: same\-orbit shortcuts include true\(0,1\)→\(0,1\)\\topredicted\(0,3\)\(0,3\)and true\(7,0\)→\(7,0\)\\topredicted\(2,0\)\(2,0\); different\-orbit shortcuts are, with only two exceptions out of 28, of the form true\(0,3\)→\(0,3\)\\topredicted\(0,0\)\(0,0\)or true\(8,0\)→\(8,0\)\\topredicted\(0,0\)\(0,0\): the paired non\-zero digit collapses specifically onto zero itself, crossing into the singleton orbit rather than landing on some other non\-zero digit\.

This is not a post\-hoc story fitted to the numbers; it follows from the loss function’s algebra, stated before the mechanism was inspected\.P​\(Y=0∣x1,x2\)=1−\(1−p1​\(0\)\)​\(1−p2​\(0\)\)P\(Y\{=\}0\\mid x\_\{1\},x\_\{2\}\)=1\-\(1\-p\_\{1\}\(0\)\)\(1\-p\_\{2\}\(0\)\)already approaches 1 whenever*either*factor’s zero\-probability does, so once the network confidently recognizes one slot as zero, the semantic loss carries essentially no gradient signal about what the other slot’s network output actually is\. The proof in[Section3\.3](https://arxiv.org/html/2608.10420#S3.SS3)that\{\(0,0\)\}\\\{\(0,0\)\\\},\{\(0,k\)\}\\\{\(0,k\)\\\}, and\{\(k,0\)\}\\\{\(k,0\)\\\}are separate orbits is exactly this same absorbing\-element fact, read offAut​\(ΦC\)\\mathrm\{Aut\}\(\\Phi\_\{C\}\)instead of a loss gradient: a bijection fixing0in one coordinate cannot also send it to a non\-zero value, so no independent\-coordinate automorphism can merge the three\. One structural fact produces both the symbolic orbit split and the real optimizer’s failure to correct the under\-constrained slot; whether the resulting drift lands on another non\-zero digit \(same\-orbit\) or on zero itself \(26 of 28 diff\-orbit cases\) is the one part of the outcomeAut​\(ΦC\)\\mathrm\{Aut\}\(\\Phi\_\{C\}\)does not speak to\.

### 6\.4Three layers: what symmetry permits, architecture realizes, and optimization selects

The exact correspondence above is a statement about the*componentwise*reading\. Replaying the same 49 levels under the typed reading of[Definition2\.7](https://arxiv.org/html/2608.10420#S2.Thmtheorem7), the one whose relabelings the shared perception network can actually realize, changes the prediction table dramatically: the diagonal action preserves whether the two digit slots agree, so every level containing a doubled pair splits\. Exactly thirteen levels are typed\-non\-transitive, computed level by level: the eight evensumlevelsy∈\{2,4,…,16\}y\\in\\\{2,4,\\dots,16\\\}\(each isolates its doubled pair\(y/2,y/2\)\(y/2,y/2\)in its own orbit\) and the fiveproductlevels\{0,4,9,16,36\}\\\{0,4,9,16,36\\\}\(the square levels, plus zero\)\.

The trained models now deliver a verdict the symbolic analysis alone never could\. Of those thirteen typed\-ambiguous levels, twelve produced*zero*shortcuts across their 12,000 model\-instance evaluations \(9,6009\{,\}600at the evensumlevels,2,4002\{,\}400at the four squareproductlevels\); the thirteenth,y∗=0y^\{\*\}\{=\}0, produced all 94, in every seed\.sumy=2y\{=\}2makes the contrast concrete: its typed orbit split,\{\(1,1\)\}\\\{\(1,1\)\\\}against\{\(0,2\),\(2,0\)\}\\\{\(0,2\),\(2,0\)\\\}, is exactly as real asy∗=0y^\{\*\}\{=\}0’s, the shared network could realize a relabeling into it, and in 600 evaluations no model ever did\.

The architecture layer is not left as an inference\. We reran the entire experiment with the one change the three\-layer reading singles out: each digit position gets its own independently initialized, independently weighted perception network, so the architecture\-realizable relabelings become the full componentwise group rather than the typed subgroup\. Everything else, pools, pairs, evaluation set, orbit ground truth, hyperparameters, and the ten seeds, is held fixed, and two predictions were recorded in the script before it was first executed: shortcut location is selected by the optimization layer and should not move, and they∗=0y^\{\*\}\{=\}0mechanism should persist\. The dual\-head models produced 101productshortcuts, every one aty∗=0y^\{\*\}\{=\}0, in all ten seeds; the twelve typed\-ambiguous levels produced zero, again, across their further 12,000 evaluations; the same\-orbit share barely moved,72/101=71\.3%72/101=71\.3\\%against the shared network’s70\.2%70\.2\\%; and the collapse mechanism sharpened, with all 29 different\-orbit cases landing in\{\(0,0\)\}\\\{\(0,0\)\\\}\(the shared run had 26 of 28\)\. One event missed the pre\-specified prediction, and we report it rather than round it away:sumproduced a single label\-preserving shortcut in its 20,000 evaluations, true\(2,7\)\(2,7\)predicted as\(7,2\)\(7,2\), a pure swap\. That is exactly the new degree of freedom independent heads add, it is the only such event in 40,000 dual\-head evaluations, and it is same\-orbit: the one novel failure the architecture change enabled is a failure the symmetry analysis already classifies as explained\.

The three layers this separates are worth naming, because they are the paper’s answer to what an orbit computation is and is not for\. The*symmetry*layer says which alternative solutions are structurally interchangeable: componentwise draws the most generous boundary, typed the architecture\-matched one\. The*architecture*layer says which relabelings a given perception design can physically realize: the shared CNN realizes exactly the typed subgroup\. The*optimization*layer says which ambiguities training actually falls into, and here the loss algebra of[Section6\.3](https://arxiv.org/html/2608.10420#S6.SS3), written down before the mechanism was inspected, already named the selector: gradient starvation at the absorbing zero\. Twelve levels offer ambiguity without starvation and stay clean; one level offers both and fails in all ten seeds\. Bare orbit splits describe where shortcuts*can*hide; the absorbing element decides where they*do*\. That the componentwise transitivity table nonetheless predicted the realized shortcut locations exactly is now explained rather than lucky: on this family, the only level where componentwise and typed ambiguity coincide is also the only one the optimizer is driven into, so the coarsest instrument inherits the credit\. The twelve empty typed\-ambiguous levels are this paper’s cleanest evidence that identifiability analysis and learning\-dynamics analysis are different instruments, and that a symmetry verdict alone, at any rung, is a map of candidate failure sites rather than a forecast\.

### 6\.5Scope

sum’s null result should not be read asAut​\(ΦC\)\\mathrm\{Aut\}\(\\Phi\_\{C\}\)succeeding trivially; it means this architecture and training regime essentially never produces a label\-preserving shortcut forsumat all, so the orbit question has nothing to classify\. Whether shortcuts occur is itself governed by task structure, here the multiplicative zero that rsbench’s product task has and that additive structure does not, consistent with this paper’s recurring finding that structure, not task family, determines pathology; this time the structure determines whether a real optimizer finds a pathology to fall into in the first place, not just whether one exists combinatorially\.

Training used uncurated random pairing specifically so that any observed shortcut would not be an artifact of a shortcut\-inducing split;productstill produced one in every seed, but this also means the reported rates \(0\.33% same\-orbit, 0\.14% diff\-orbit\) are a conservative estimate under standard training, not an upper bound obtainable by deliberately restricting training coverage as rsbench’s ownshortcutmnistdoes\[[7](https://arxiv.org/html/2608.10420#bib.bib7)\]\. The 40,000 figures are model\-instance evaluations, not independent samples: the same 2,000 held\-out instances are scored by all ten seeds by design, so that seeds are compared on one yardstick, and per\-seed counts are reported wherever a rate is pooled\. The70\.2%70\.2\\%/29\.8%29\.8\\%split is a ten\-seed pooled statistic with no confidence interval; the per\-seed range \(2020–50%50\\%diff\-orbit\) is reported instead of a single point estimate for that reason\. The shared\-network and dual\-head runs together cover both ends of the architecture rung \(typed and componentwise realizable relabelings,[Section6\.4](https://arxiv.org/html/2608.10420#S6.SS4)\); the shortcut geography survived the change intact, which is itself the strongest single piece of evidence that the optimization layer, not the architecture layer, selects where shortcuts land on this family\. The orbit classification of the observed shortcuts is likewise rung\-independent: onΦ0\\Phi\_\{0\}the typed and componentwise orbit partitions coincide, both giving exactly\{\(0,0\)\}\\\{\(0,0\)\\\},\{\(0,k\)\}\\\{\(0,k\)\\\},\{\(k,0\)\}\\\{\(k,0\)\\\}\.[Tables2](https://arxiv.org/html/2608.10420#S3.T2)and[3](https://arxiv.org/html/2608.10420#S3.T3)’s figures for the other families are symbolic measurements in the sense of[Section3](https://arxiv.org/html/2608.10420#S3)\.

## 7Related Work

#### Reasoning shortcuts and Takemura et al\.’s framework\.

Marconato, Teso, Vergari, and Passerini characterize reasoning shortcuts as unintended optima of a neurosymbolic training objective and give four conditions under which they occur\[[15](https://arxiv.org/html/2608.10420#bib.bib15)\]; their analysis is distributional, over what a learner can converge to, and never introduces a symmetry group\. Their rsbench suite supplies the majority of the real rule families measured in[Section3](https://arxiv.org/html/2608.10420#S3): the CLE4EVR, Kandinsky, and BDD\-OIA/SDD\-OIA core measurements and five of the eight extension families\[[7](https://arxiv.org/html/2608.10420#bib.bib7)\]\. Takemura, Inoue, and Nishino introduce a permutation\-group account of this problem, Definition[2\.3](https://arxiv.org/html/2608.10420#S2.Thmtheorem3), and leave a complete characterization of uniqueness beyond triviality of that group as their paper’s most pressing open question\[[26](https://arxiv.org/html/2608.10420#bib.bib26)\]\.[Section2](https://arxiv.org/html/2608.10420#S2)shows their definition does not extend to any of the four benchmarks it was evaluated on without an embedding step the framework itself does not specify, and that the most direct such step gives a confident wrong answer rather than a conservative one \(Table[1](https://arxiv.org/html/2608.10420#S2.T1)\)\.[Sections4](https://arxiv.org/html/2608.10420#S4)and[5](https://arxiv.org/html/2608.10420#S5)answer their open question for the componentwise generalization: with sufficient, checked conditions for transitivity and its failure, and a complexity landscape for deciding which applies, rather than a complete characterization, which we show in[Section4](https://arxiv.org/html/2608.10420#S4)has no clean form even for the classical, decades\-older special case of Latin\-square autotopism groups\.

#### Classical CSP symmetry\.

Cohen, Jeavons, Jefferson, Petrie, and Smith give the vocabulary this paper builds on, separating constraint symmetry from solution symmetry and proving the former is a subgroup of the latter\[[10](https://arxiv.org/html/2608.10420#bib.bib10)\];[Section2](https://arxiv.org/html/2608.10420#S2)already used their Example 3 to justify working with∏i=1nSym​\(Si\)\\prod\_\{i=1\}^\{n\}\\mathrm\{Sym\}\(S\_\{i\}\)instead of their unrestricted variable\-value\-pair permutations, which degenerate to an uninformativen\!​\(n​\(d−1\)\)\!n\!\\,\(n\(d\{\-\}1\)\)\!on near\-unique solution sets\. Puget detects symmetries algorithmically, by encoding a CSP instance into a colored graph and calling a graph\-automorphism solver, covering global constraints and arithmetic expressions\[[20](https://arxiv.org/html/2608.10420#bib.bib20)\]\. The lineage of exploiting such groups goes back to Crawford, Ginsberg, Luks, and Roy’s symmetry\-breaking predicates, which cut the searched space to orbit representatives once the group is known\[[11](https://arxiv.org/html/2608.10420#bib.bib11)\]; this paper asks the converse question, what the orbits fail to cover\. Gent, Petrie, and Puget survey the field and are the classical reference Takemura et al\. cite for the connection their own Definition 7 does not fully use\[[12](https://arxiv.org/html/2608.10420#bib.bib12)\]\. All three ask how to detect or use symmetry given an explicit instance; none gives a complexity classification for the existence question itself, and none proves a sufficient condition for transitivity in the sense of Theorems[4\.3](https://arxiv.org/html/2608.10420#S4.Thmtheorem3)through[4\.11](https://arxiv.org/html/2608.10420#S4.Thmtheorem11)\. A direct text search of both versions of Cohen et al\.’s paper for “orbit” turns up no hits; the sole hit for “transitive” refers to the transitive closure of equality constraints, not to a group acting transitively on a set of solutions\.

#### Circuit and formula isomorphism\.

Borchert, Ranjan, and Stephan open the question of the complexity of deciding whether two Boolean objects are related by a*position*permutation, and Agrawal and Thierauf resolve one direction of it\[[6](https://arxiv.org/html/2608.10420#bib.bib6),[1](https://arxiv.org/html/2608.10420#bib.bib1)\]; Böhler, Creignou, Galota, Reith, Schnoor, and Vollmer extend the classification across Post’s lattice and confirm the isomorphism question itself is still open sixteen years later\[[5](https://arxiv.org/html/2608.10420#bib.bib5)\]\. This is the same coNP\-hard\-to\-Σ2𝗉\\Sigma\_\{2\}^\{\\mathsf\{p\}\}shape ourNontriv\-Autoccupies, using the same frozen\-variable hardness technique, but for a different group \(Sym​\(N\)\\mathrm\{Sym\}\(N\), permuting named positions, rather than∏i=1nSym​\(Si\)\\prod\_\{i=1\}^\{n\}\\mathrm\{Sym\}\(S\_\{i\}\), permuting values independently at each position\) and a different question \(two objects compared, rather than one object’s own automorphisms\)\. To our knowledge the complexity of*translation*\-automorphism existence, for general or for monotone circuits, does not appear in this line or elsewhere; the nearest objects are the permutation\-and\-negation \(NPN\) equivalences charted by Borchert et al\.\[[6](https://arxiv.org/html/2608.10420#bib.bib6)\], and[Theorem5\.27](https://arxiv.org/html/2608.10420#S5.Thmtheorem27)’s deterministic completeness on monotone circuits has no analogue there\. Section[5\.5](https://arxiv.org/html/2608.10420#S5.SS5)transplants their collapse theorem to the value\-permutation group directly;[Section5\.6](https://arxiv.org/html/2608.10420#S5.SS6)and[AppendixA](https://arxiv.org/html/2608.10420#A1)report that their own labeling technique for descending from the two\-object to the one\-object question does not transplant, because it needs a group that permutes named objects and∏i=1nSym​\(Si\)\\prod\_\{i=1\}^\{n\}\\mathrm\{Sym\}\(S\_\{i\}\)does not, and diagnose what does\.

#### Boolean function analysis and linear structures\.

O’Donnell’s Fourier\-analytic treatment of Boolean functions\[[19](https://arxiv.org/html/2608.10420#bib.bib19)\]supplies the exact language of Lemma[5\.14](https://arxiv.org/html/2608.10420#S5.Thmtheorem14):Aut​\(ΦC\)\\mathrm\{Aut\}\(\\Phi\_\{C\}\), in the Boolean case, is the orthogonal complement of the Fourier support, not merely an analogy to it\. Rothaus’s bent functions\[[21](https://arxiv.org/html/2608.10420#bib.bib21)\], maximally non\-linear in the sense of having no nonzero linear structure, are the building block behind Proposition[5\.18](https://arxiv.org/html/2608.10420#S5.Thmtheorem18)’s witness construction\. The cryptographic literature on linear structures \(S\-boxes invariant under a fixed input XOR\) is extensive but entirely constructive: given an explicit truth table, how few or zero linear structures can a designed function have\. None of it addresses the decision problem this paper studies, whether a*succinctly given*circuit has a nonzero linear structure at all, a question that is trivial once the truth table is in hand and coNP\-hard once it is not \(Theorem[5\.3](https://arxiv.org/html/2608.10420#S5.Thmtheorem3)\)\.

#### Latin square autotopism groups\.

A Latin square’s autotopism group, the subgroup ofSym​\(rows\)×Sym​\(columns\)×Sym​\(symbols\)\\mathrm\{Sym\}\(\\text\{rows\}\)\\times\\mathrm\{Sym\}\(\\text\{columns\}\)\\times\\mathrm\{Sym\}\(\\text\{symbols\}\)stabilizing its defining relation, is the special case ofAut​\(ΦC\)\\mathrm\{Aut\}\(\\Phi\_\{C\}\)studied since Section[4\.1](https://arxiv.org/html/2608.10420#S4.SS1)’s design\-theory remark\. McKay, Meynert, and Myrvold reduce computing it to graph automorphism via a vertex\-colored encoding and enumerate autotopism groups for all Latin squares up to order 10, finding no closed\-form classification even at that scale\[[17](https://arxiv.org/html/2608.10420#bib.bib17)\]\. This is the same pattern Section[4](https://arxiv.org/html/2608.10420#S4)finds for reasoning\-shortcut constraint sets: Theorem[4\.9](https://arxiv.org/html/2608.10420#S4.Thmtheorem9)already rules out transitivity for every measured all\-different instance by counting alone, matching the combinatorial\-design literature’s own experience that exhaustive computation, not a general theorem, is the working tool once the instance is not built from an equality or absorbing\-element pattern simple enough for Theorems[4\.3](https://arxiv.org/html/2608.10420#S4.Thmtheorem3)through[4\.8](https://arxiv.org/html/2608.10420#S4.Thmtheorem8)to reach\.

## 8Conclusion

Whether the automorphisms of a rule explain its reasoning shortcuts is not one question but three, and this paper has tried to answer each at the level of rigor it admits\. Which group? The published global definition does not apply as stated to any heterogeneous benchmark it was evaluated on; using it requires an embedding step the framework does not specify, the most direct embedding produces measured false pathology whose content is configuration\-file bookkeeping, and componentwise value symmetry is the instrument that needs no embedding at all \([Section2](https://arxiv.org/html/2608.10420#S2)\)\. When do orbits explain the shortcuts? Not uniformly\. Across eleven rule families the answer spans0%0\\%to99\.9999%99\.9999\\%, and it tracks provable structure: matching decompositions and exchangeable branches force transitivity, while anchored inequalities, absorbing elements, counting bounds and occupied free slots force its failure \([Sections3](https://arxiv.org/html/2608.10420#S3)and[4](https://arxiv.org/html/2608.10420#S4)\)\. In the Boolean case the second question closes completely: the group acts freely, transitivity holds exactly for affine solution sets, and the orbit lawρ=1−\(\|Aut​\(ΦC\)\|−1\)/\(\|ΦC\|−1\)\\rho=1\-\(\|\\mathrm\{Aut\}\(\\Phi\_\{C\}\)\|\-1\)/\(\|\\Phi\_\{C\}\|\-1\)turns[Section3](https://arxiv.org/html/2608.10420#S3)’s measured percentages into a theorem’s values\. How hard is the question itself? coNP\-complete for a designated coordinate, and for existence, coNP\-hard under randomized reductions yet notΣ2𝗉\\Sigma\_\{2\}^\{\\mathsf\{p\}\}\-complete unless the polynomial hierarchy collapses, with the gap closing entirely, to deterministic coNP\-completeness, on monotone circuits \([Section5](https://arxiv.org/html/2608.10420#S5)\)\. And the theory is not merely internally consistent: trained models place every one of their observed concept\-level shortcuts at exactly the level the componentwise analysis flags, and nowhere else, while the twelve extra candidates of the typed reading stay empty, splitting what symmetry permits from what optimization selects \([Section6](https://arxiv.org/html/2608.10420#S6)\)\.

Two findings deserve to outlive the paper’s specific numbers\. The first is methodological\. A definition applied outside its stated hypotheses did not fail loudly on real data\. It failed quietly, returning a stable\-looking90\.91%90\.91\\%whose content rotated with an arbitrary file ordering\. The padding sweep suggests this failure mode is generic, and nothing about it is specific to symmetry analysis: any instrument ported outside its stated domain by an unexamined embedding can fail the same way\. Checking the embedding, not just the instrument, is the transferable lesson\. The second is structural\. The same dead\-variable phenomenon was flagged by orbit combinatorics on one benchmark and by𝔽2\\mathbb\{F\}\_\{2\}\-linear algebra on another, two toolkits with no shared machinery agreeing on the same diagnosis\. Where independent formalisms converge, the phenomenon is a property of the problem, not of the method\.

The paper opens a program larger than itself, and we close by naming its two best problems, each handed over with equipment\. The sharpest is the exact complexity ofNontriv\-Autfor general circuits, between randomized coNP\-hardness and the collapse bound\. The next attacker inherits more than a question: the boundary is drawn, since the gap closes outright on monotone circuits \([Theorem5\.27](https://arxiv.org/html/2608.10420#S5.Thmtheorem27)\), so the general case is precisely a question about non\-monotone camouflage, and[AppendixA](https://arxiv.org/html/2608.10420#A1)maps the three structural obstructions any approach must clear\. The second is Takemura et al\.’s original question, a complete characterization of when rules pin concepts down\. This paper settles it for the Boolean case, where transitivity is classified outright \([Proposition5\.13](https://arxiv.org/html/2608.10420#S5.Thmtheorem13)\), and locates the general case at the tractable middle ground the Latin\-square literature’s decades of experience with autotopism groups recommends: checkable mechanisms rather than a closed form, which on every real benchmark measured sufficed to say which side of the line the rule falls on and why\. Extending the dual\-head control of[Section6](https://arxiv.org/html/2608.10420#S6)to rule families where the symmetry rungs disagree more sharply is the experiment we would run next\.

## Appendix AThe Obstruction Landscape ofNontriv\-Aut

Nontriv\-Aut’s complexity is still not pinned to a single class: we know it is coNP\-hard under randomized reductions \(Corollary[5\.7](https://arxiv.org/html/2608.10420#S5.Thmtheorem7)\), inΣ2𝗉\\Sigma\_\{2\}^\{\\mathsf\{p\}\}\(Theorem[5\.4](https://arxiv.org/html/2608.10420#S5.Thmtheorem4)\), and notΣ2𝗉\\Sigma\_\{2\}^\{\\mathsf\{p\}\}\-complete unless𝖯𝖧\\mathsf\{PH\}collapses \(Theorem[5\.24](https://arxiv.org/html/2608.10420#S5.Thmtheorem24)\)\. Seven attempts to close what gap remains failed before the eighth reached that last result, and the seven failures are not seven unrelated dead ends\.

###### Proposition A\.1\(Witnesses are not subgroups\)\.

There is no reduction fromΣ2​\-sat\\Sigma\_\{2\}\\textup\{\{\-sat\}\}toNontriv\-Autof the form “encode a candidate witnessx∈\{0,1\}px\\in\\\{0,1\\\}^\{p\}directly as a coordinate shiftax∈\{0,1\}pa\_\{x\}\\in\\\{0,1\\\}^\{p\}, so thatax∈L0​\(f\)a\_\{x\}\\in L\_\{0\}\(f\)exactly when∀y​φ​\(x,y\)\\forall y\\,\\varphi\(x,y\)”: for a fixed instanceφ\\varphi, the target setT:=\{x:∀y​φ​\(x,y\)\}T:=\\\{x:\\forall y\\,\\varphi\(x,y\)\\\}need not be a subgroup of\{0,1\}p\\\{0,1\\\}^\{p\}, whileL0​\(f\)L\_\{0\}\(f\), for anyffwhatsoever, always is\.

###### Proof\.

L0​\(f\)L\_\{0\}\(f\)is a stabilizer of the coordinatewise action of\{0,1\}p\\\{0,1\\\}^\{p\}on functions, hence a subgroup for anyff: this holds before any reduction\-specific reasoning\. A subgroup has order dividing2p2^\{p\}and contains0; on 216 random smallΣ2\\Sigma\_\{2\}\-satinstances \(p,q∈\{1,2,3\}p,q\\in\\\{1,2,3\\\}\), 50 \(23\.1%\) have aTTwhose size does not divide2p2^\{p\}, ruling out any suchTTfrom being a subgroup on the spot, and a direct implementation of the naive encoding disagrees with the true truth value ofφ\\varphion 201 of 216 instances \(93\.1%\)\. ∎

The seven attempts, spanning direct encoding, two indirect encodings, literature transplant, and interactive protocols:

1. 1\.*Direct witness encoding*\(Proposition[A\.1](https://arxiv.org/html/2608.10420#A1.Thmtheorem1)\): blocked because coordinatewise stabilizers are always subgroups and genericΣ2\\Sigma\_\{2\}\-satwitness sets are not\.
2. 2–3\.*Two indirect encodings*\(extra switch bit; XORed copies with bent\-function padding\):96\.0%96\.0\\%and73\.3%73\.3\\%mismatch rates, since both still let the witness set control a coordinate block, inheriting the same subgroup obstruction one layer down\.
3. 4\.*Small\-Hamming\-weight witnesses*\(Proposition[5\.18](https://arxiv.org/html/2608.10420#S5.Thmtheorem18)\): the strongest form is false by explicit construction\.
4. 5\.*Agrawal–Thierauf’s labeling gadget, transplanted*\(four tagging constructions\):28\.9%28\.9\\%to64\.4%64\.4\\%mismatch rates, since the gadget needs a group that permutes named objects, and coordinatewiseXOR\\mathrm\{XOR\}does not\.
5. 6\.*Direct hashing ofAut​\(ΦC\)\\mathrm\{Aut\}\(\\Phi\_\{C\}\)*: technically sound but information\-free, since it provesNontriv\-Aut∈𝖡𝖯⋅Σ2𝗉\\textup\{\{Nontriv\-Aut\}\}\\in\\mathsf\{BP\}\\cdot\\Sigma\_\{2\}^\{\\mathsf\{p\}\}, already implied for free by Theorem[5\.4](https://arxiv.org/html/2608.10420#S5.Thmtheorem4)\.
6. 7\.*The flip\-bit decomposition*\(Proposition[5\.19](https://arxiv.org/html/2608.10420#S5.Thmtheorem19)\): tautologically correct but every disjunct below the last is exactly as hard as the whole\.

Every one of these seven failures traces back to one of three structural facts, not to seven unrelated missed tricks:

1. \(i\)Aut​\(ΦC\)\\mathrm\{Aut\}\(\\Phi\_\{C\}\)is always a subgroup; a genericΣ2𝗉\\Sigma\_\{2\}^\{\\mathsf\{p\}\}witness set is not \(attempt 1\)\.
2. \(ii\)∏i=1nSym​\(Si\)\\prod\_\{i=1\}^\{n\}\\mathrm\{Sym\}\(S\_\{i\}\)acts freely and transitively on∏iSi\\prod\_\{i\}S\_\{i\}; it does not permute a set of named objects the waySym​\(N\)\\mathrm\{Sym\}\(N\)does, so techniques that need to distinguish “objectii” from “objectjj” have nothing to grab onto \(attempts 2, 3, and 5\)\.
3. \(iii\)Any access toL0​\(f\)L\_\{0\}\(f\)stronger than a pointwise oracle \(an explicit basis, or a syntactically exposed witness\) is already at least as hard to obtain as solvingNontriv\-Autitself \(attempts 4 and 6, and the residual, non\-collapsing disjuncts of attempt 7\)\.

Interactive\-proof and structural\-isomorphism toolkits are built for \(ii\): they turn one\-object questions into two\-object comparisons by naming and tagging, at the cost of needing a group that permutes named objects\. Linear\-algebraic toolkits are built for \(iii\): they turn implicit membership queries into explicit structure, at the cost of needing exactly the accessNontriv\-Aut’s succinct representation denies\.Nontriv\-Autcombines succinctness with single\-object existence, and no toolkit here is built for both at once\. This is a diagnosis, not a barrier theorem: we have not shown, and do not claim, that every future technique must fail this way, only that eight independently designed attempts, spanning direct encoding, interactive protocols, and linear algebra, either failed for one of these three reasons or \(the eighth, Theorem[5\.24](https://arxiv.org/html/2608.10420#S5.Thmtheorem24)\) found the one combination the diagnosis does not rule out: laundering an object’s syntax away before hashing it, which sidesteps \(ii\) by never naming anything and sidesteps \(iii\) by never asking for more than a laundered, single\-representative view of one object at a time\.

## Appendix BVerification Artifacts

Sections[4](https://arxiv.org/html/2608.10420#S4)and[5](https://arxiv.org/html/2608.10420#S5)mark each computational check behind a theorem, lemma, proposition, or corollary with a short pointer, “Computationally verified; see[AppendixB](https://arxiv.org/html/2608.10420#A2),” in place of an inline description of instance counts and outcomes\. This appendix collects those checks in one place\. The verification code and its result artifacts are released alongside this paper, and every number below carries a source\-file provenance comment \(% prov:\) at its original point of use in theLaTeXsource, recording the exact script, script section, and reported figures it traces to\.LABEL:tab:verification\-artifactsreports, for each result, the population of instances it was checked against, the outcome, and the artifact file responsible\. None of these checks substitutes for the proofs given in the main text: every result listed here is proved there, and the table documents an independent computational cross\-check of that proof, not the proof itself\.

Table 8:Computational\-verification artifacts referenced from Sections[4](https://arxiv.org/html/2608.10420#S4)and[5](https://arxiv.org/html/2608.10420#S5)\. “Outcome” reports exactly what the cited script measured; it supports, rather than substitutes for, the adjacent proof\.ResultVerification scopeOutcomeArtifact[Definition2\.7](https://arxiv.org/html/2608.10420#S2.Thmtheorem7)\(hierarchy robustness\)CLE4EVR 6\-dim and 8\-dim, Kandinsky 6\-dim \(exhaustive typed and componentwise groups and orbits, cross\-checked against the main pipeline’s stored groups\); MNAdd\-productΦ0\\Phi\_\{0\}\(structural characterization sampled on 4,000 random permutation pairs, orbits from generators\)typed==componentwise exactly on CLE4EVR 6\-dim and Kandinsky \(groups and orbit partitions\); they differ only on CLE4EVR’s free size slots \(144 vs\. 864, 2 orbits vs\. 1\);Φ0\\Phi\_\{0\}orbit partition\[9,9,1\]\[9,9,1\]identical under both; both measured componentwise groups non\-abelian via explicit non\-commuting pairstheoryF\_typed\_symmetry\.py[Theorem4\.3](https://arxiv.org/html/2608.10420#S4.Thmtheorem3)184 random equality\-block instances \(1–4 blocks, 1–3 positions/block, domain sizes 2–4, 0–2 free positions; equality case only,fl,j=idf\_\{l,j\}=\\mathrm\{id\}\); 116 further instances skipped \(ambient group order over budget\)0 counterexamplestheoryB\_theorem1\_verify\.py[Theorem4\.4](https://arxiv.org/html/2608.10420#S4.Thmtheorem4)two minimal instances \(2 attribute slots×\\times2 values\): symmetric \(\|ΦC\|=12\|\\Phi\_\{C\}\|=12\) and asymmetric \(\|ΦC\|=4\|\\Phi\_\{C\}\|=4\)symmetric: transitive, 6/6Aut​\(ΦC\)\\mathrm\{Aut\}\(\\Phi\_\{C\}\)elements map branch 1 onto branch 2; asymmetric: not transitive, 3 orbits of sizes\[2,1,1\]\[2,1,1\]theoryB\_theorem3\_verify\.py[Theorem4\.6](https://arxiv.org/html/2608.10420#S4.Thmtheorem6)\(broad search\)random search, 4,000 constraint sets built from equality/inequality atoms withand/or\(3,058 non\-trivial: 2,479 conjunction\-only, 579 disjunctive\)22 of 2,479 purely\-conjunctive instances non\-transitive; 349 of 579 disjunctive instances remain transitivetheoryB\_falsification\_search\_results\.json[Theorem4\.6](https://arxiv.org/html/2608.10420#S4.Thmtheorem6)\(false\-positive search\)second random search, 2,295 instances \(ambient group order≤15,000\\leq 15\{,\}000\)0 false positives; by connective, 15/15 \(100%\) conjunctive non\-transitive instances caught, 6/156 \(3\.8%\)or\-containing non\-transitive instances caughttheoryB\_theorem2\_verify\.py, theoryB\_followups\.py[Theorem4\.6](https://arxiv.org/html/2608.10420#S4.Thmtheorem6)\(multi\-leg sweep\)domain sizeD=3D=3\(k∈\{2,3,4\}k\\in\\\{2,3,4\\\}attached legs\) andD=4D=4\(k∈\{2,3\}k\\in\\\{2,3\\\}legs\)D=3D=3: 2, 4, 8 orbits respectively;D=4D=4: 2, 5 orbits respectivelytheoryB\_followups\.py[Theorem4\.8](https://arxiv.org/html/2608.10420#S4.Thmtheorem8)\(abstract family\)zero\-factor familyΦ=\{\(c1,c2\)∈\{0,…,m−1\}2:c1​c2=0\}\\Phi=\\\{\(c\_\{1\},c\_\{2\}\)\\in\\\{0,\\dots,m\-1\\\}^\{2\}:c\_\{1\}c\_\{2\}=0\\\}, exact enumeration atm=3,4,5m=3,4,5deg1⁡\(0\)=m\\deg\_\{1\}\(0\)=m,deg1⁡\(v\)=1\\deg\_\{1\}\(v\)=1forv≠0v\\neq 0in every case; non\-transitive at all three values ofmmtheoryB\_mechanisms\_D\_E\_verify\.py[Theorem4\.8](https://arxiv.org/html/2608.10420#S4.Thmtheorem8)\(additive control\)additive control familyc1\+c2=kc\_\{1\}\+c\_\{2\}=kover\{0,…,m−1\}\\\{0,\\dots,m\-1\\\}, two tested configurations \(no absorbing element\)constant degree at every value; transitive in both configurationstheoryB\_mechanisms\_D\_E\_verify\.py[Theorem4\.8](https://arxiv.org/html/2608.10420#S4.Thmtheorem8)\(random battery\)619 random instances built from equality/inequality atoms \(ambient group order budget≤2,000\\leq 2\{,\}000\)0 false positives, 0 true positivestheoryB\_mechanisms\_D\_E\_verify\.py[Theorem4\.11](https://arxiv.org/html/2608.10420#S4.Thmtheorem11)\(\(H\-count\) necessity\)parametrized family,r∈\{2,3,4,5\}r\\in\\\{2,3,4,5\\\}branches, free\-slot sizenCn\_\{C\}swept above and below the thresholdr−1r\-1\(14 exhaustive configurations\)5/5 configurations withnC\>r−1n\_\{C\}\>r\-1preserve branches; 5 further configurations with2≤nC≤r−12\\leq n\_\{C\}\\leq r\-1also preserve branches \(hypothesis fails, conclusion still holds\); 4 configurations atnC=1n\_\{C\}=1\(all four values ofrr\): branches merge, transitivetheoryB2\_free\_slot\_lemma\_generalization\.py[Lemma4\.10](https://arxiv.org/html/2608.10420#S4.Thmtheorem10)\(pair\-richness and exact groups\)order\-3 Latin squares,4×44\\times 4Sudoku with2×22\\times 2boxes, order\-4 Latin squares without boxes; full solution enumeration \(\|Φ\|=12\|\\Phi\|=12,288288,576576\)pair\-richness holds for every same\-row and same\-column position pair in all three instances; exact componentwise groups by backtracking have orders 6, 24, 24 with every element diagonal;\|Φ\|\>\|Aut\|\|\\Phi\|\>\|\\mathrm\{Aut\}\|in all threetheoryE\_latin\_diagonal\_collapse\.py[Theorem5\.3](https://arxiv.org/html/2608.10420#S5.Thmtheorem3)\(gap pressure test\)pressure test, 400 random smallunsat\-reduction instances \(varyingkk, clause count, 3\-CNF\)108/400 \(27%\) satisfiableχ\\chiyield a full\-instance nontrivial automorphism fromχ\\chi’s own accidental symmetrytheoryA4\_leadA\_flipbit\_decomposition\.py[Corollary5\.7](https://arxiv.org/html/2608.10420#S5.Thmtheorem7)\(both directions\)k=4,…,10k=4,\\dots,10, fresh random 3\-CNF instances plus an adversarial battery with a chosen internal symmetry, plusχ=\\chi=paritynatural false\-positive rate18%18\\%–30%30\\%acrossk=4\.\.8k=4\.\.8\(reproducing the 27% figure above\); isolation success rate tracks the predictedΘ​\(1/\(k\+1\)\)\\Theta\(1/\(k\{\+\}1\)\)rate \(8\.7%8\.7\\%vs\.9\.1%9\.1\\%reference atk=10k=10;9\.3%9\.3\\%vs\.11\.1%11\.1\\%atk=8k=8\); resultingχ′\\chi^\{\\prime\}symmetry independently confirmed trivial on every successful runtheoryA7\_corollary21\_isolation\_fix\_results\.json[Section6\.4](https://arxiv.org/html/2608.10420#S6.SS4)\(dual\-head control\)10 seeds×\\times2 tasks retrained with two independent perception networks; identical pools, pairs, eval set, orbit tables, hyperparameters; predictions pre\-specified in the script docstring before first executionproduct: 101 shortcuts \(72 same\-orbit, 29 diff\-orbit\), all aty∗=0y^\{\*\}\{=\}0, 10/10 seeds; all 29 diff\-orbit cases collapse into\{\(0,0\)\}\\\{\(0,0\)\\\}; 12 typed\-ambiguous levels zero across 12,000 evaluations;sum: one same\-orbit swap\(2,7\)→\(7,2\)\(2,7\)\\to\(7,2\)in 20,000realmodel\_mnadd\_dualhead\_pipeline\.py[2\.6](https://arxiv.org/html/2608.10420#S2.Thmtheorem6)\(bijective/general divide\),[Definition2\.7](https://arxiv.org/html/2608.10420#S2.Thmtheorem7)\(typed levels\),[Section6\.4](https://arxiv.org/html/2608.10420#S6.SS4)\(counting conventions\)the three\-solution counterexampleΦC=\{\(0,0\),\(0,1\),\(1,0\)\}\\Phi\_\{C\}=\\\{\(0,0\),\(0,1\),\(1,0\)\\\}exhaustively; 167 random bijective\-set instances for the same\-set embedding; exact typed orbits for every non\-singletonsumandproductlevel \(value\-support brute force; two size\-10 supports handled by verified explicit constructions\); all level and evaluation countsswap preservesΦCbij\\Phi\_\{C\}^\{\\mathrm\{bij\}\}but notΦC\\Phi\_\{C\}\(0 same\-set violations\); typed\-non\-transitive levels exactly\{2,4,…,16\}\\\{2,4,\\dots,16\\\}\(sum\) and\{0,4,9,16,36\}\\\{0,4,9,16,36\\\}\(product\); counts56=19\+3756=19\{\+\}37reachable,4949non\-singleton,40,000=34,800\+3,800\+1,40040\{,\}000=34\{,\}800\{\+\}3\{,\}800\{\+\}1\{,\}400,12,00012\{,\}000at the twelve typed\-ambiguous levelstheoryH\_review2\_checks\.py[Proposition5\.12](https://arxiv.org/html/2608.10420#S5.Thmtheorem12),[Proposition5\.13](https://arxiv.org/html/2608.10420#S5.Thmtheorem13)\(free action, coset classification,ρ\\rholaw\)372 random Boolean instances \(n=3\.\.6n=3\.\.6, mixed random subsets and random affine cosets\) plus all eight BDD\-OIA/SDD\-OIA rows of[Table2](https://arxiv.org/html/2608.10420#S3.T2)0 violations of free action, of transitive\-iff\-coset, and of the closed form; all eight table rows reproduced \(orbit count, max orbit,ρ\\rho\) to within10−910^\{\-9\}theoryG\_depth\_explorations\.py[Lemma5\.26](https://arxiv.org/html/2608.10420#S5.Thmtheorem26),[Theorem5\.27](https://arxiv.org/html/2608.10420#S5.Thmtheorem27)\(monotone package\)300 random monotone functions \(n=2\.\.5n=2\.\.5, upward closures\); 300 random 3\-CNFs \(m=2\.\.4m=2\.\.4\) through the double\-rail gadget, exhaustive dead/alive checks of every position ofhhL0=L\_\{0\}=span of dead flips in all 300; implication\-iff\-unsatin all 300; rails always alive,x∗x\_\{\*\}dead iff unsatisfiable,Nontriv\-Aut​\(h\)\\textup\{\{Nontriv\-Aut\}\}\(h\)iffunsatin all 300theoryG\_depth\_explorations\.py[Proposition5\.16](https://arxiv.org/html/2608.10420#S5.Thmtheorem16)\(levels over mixed domains\)40 random instances with domain sizes in\{2,3\}\\\{2,3\\\}\(n=2\.\.4n=2\.\.4positions\); 1,976 group elements checked against the fix\-every\-level criterion0 violations of dead\-iff\-absent, of the degree\-profile identity, and of the equivariance criteriontheoryG\_depth\_explorations\.py[Proposition5\.10](https://arxiv.org/html/2608.10420#S5.Thmtheorem10)\(alive\-promise gadget\)500 random 3\-CNFφ\\varphioverm∈\{2,3,4\}m\\in\\\{2,3,4\\\}variables \(482 satisfiable, 18 unsatisfiable\), exhaustive dead/alive check of every position of the gadgeteverywjw\_\{j\}andttalive in all 500 instances;xix\_\{i\}dead on exactly the unsatisfiable ones \(0 violations in either direction\)theoryD\_deadvar\_alive\_promise\.pyRemark[5\.8](https://arxiv.org/html/2608.10420#S5.Thmtheorem8)\(single attempt\)pooledk=4,…,10k=4,\\dots,10, same battery, single run ofRRnontrivial on56%56\\%–67%67\\%of satisfiable instances pooled;60%60\\%–94%94\\%on the adversarial battery;45%45\\%–56%56\\%on natural instancestheoryA7\_corollary21\_isolation\_fix\_results\.jsonRemark[5\.8](https://arxiv.org/html/2608.10420#S5.Thmtheorem8)\(repetition\)same battery,ttindependent repetitions ofRRcorrected false\-positive rate falls to≤2%\\leq 2\\%byt=8t=8, to0%0\\%byt=16t=16at everykktested \(k=10k=10:56\.9%,35\.3%,21\.6%,2\.0%,0\.0%56\.9\\%,35\.3\\%,21\.6\\%,2\.0\\%,0\.0\\%att=1,2,4,8,16t=1,2,4,8,16\); Monte Carlo confirms the1−\(1−p\)t1\-\(1\-p\)^\{t\}law to within0\.00950\.0095absolute errortheoryA7\_corollary21\_isolation\_fix\_results\.jsonRemark[5\.9](https://arxiv.org/html/2608.10420#S5.Thmtheorem9)product\-structure check across all four trivial/nontrivial block combinations, plus the degenerate empty\-block case40/40 exact product\-structure matches; 20/20 exact full\-group matches \(degenerate empty block\)theoryA7\_corollary21\_isolation\_fix\_results\.json[Lemma5\.14](https://arxiv.org/html/2608.10420#S5.Thmtheorem14)288 instances, dimensions 2–7, four generating families \(uniform random truth tables, random clause conjunctions, affine functions, XORs of two random juntas\)definitionalAut​\(ΦC\)\\mathrm\{Aut\}\(\\Phi\_\{C\}\)and the Fourier\-support orthogonal complement agree exactly in every case \(also re\-confirms[Corollary5\.11](https://arxiv.org/html/2608.10420#S5.Thmtheorem11)on the same instances\)theoryA2\_equivalence\_check\.py[Lemma5\.17](https://arxiv.org/html/2608.10420#S5.Thmtheorem17)300 random pairs\(f,g\)\(f,g\),n=6n=6containment never fails; strict in 108/300 \(36%\); representative case\|L0​\(f\)\|=64\|L\_\{0\}\(f\)\|=64,\|L0​\(g\)\|=8\|L\_\{0\}\(g\)\|=8,\|L0​\(f\)∩L0​\(g\)\|=8\|L\_\{0\}\(f\)\\cap L\_\{0\}\(g\)\|=8,\|L0​\(f∧g\)\|=64\|L\_\{0\}\(f\\wedge g\)\|=64theoryA2\_equivalence\_check\.py[Proposition5\.18](https://arxiv.org/html/2608.10420#S5.Thmtheorem18)n=3,5,7,9n=3,5,7,9,aaset to the all\-ones vector \(largest Hamming weight\)exhaustive enumeration confirmsL0​\(f\)=\{0,a\}L\_\{0\}\(f\)=\\\{0,a\\\}exactly in all four cases; underlying inner\-product bent functions \(n−1=2,4,6,8n\{\-\}1=2,4,6,8\) independently confirmed to have no nonzero linear structuretheoryA2\_directionB\_hamming\_weight\.pyflip\-bit decomposition \([Section5\.4](https://arxiv.org/html/2608.10420#S5.SS4)\)600 instances, dimensions 1–6, four generating familiesNontriv\-Aut​\(f\)\\textup\{\{Nontriv\-Aut\}\}\(f\)and⋁iQi​\(f\)\\bigvee\_\{i\}Q\_\{i\}\(f\)agree in every casetheoryA4\_leadA\_flipbit\_decomposition\.pyQn=Dead\-Var​\(C,n\)Q\_\{n\}=\\textup\{\{Dead\-Var\}\}\(C,n\)identity \([Section5\.4](https://arxiv.org/html/2608.10420#S5.SS4)\)960 instances, dimensions 1–6, four generating familiesQnQ\_\{n\}identical to directDead\-Varcheck in all casestheoryA4\_leadA\_flipbit\_decomposition\.py[Proposition5\.19](https://arxiv.org/html/2608.10420#S5.Thmtheorem19)i=1,…,4i=1,\\dots,4,k=2,…,5k=2,\\dots,5, 5,048 instances total, including three adversarialχ\\chi\(constant\-true, constant\-false,χ=parity\\chi=\\mathrm\{parity\}\)QiQ\_\{i\}tracksunsatexactly in every one of the 5,048 trials, 0 mismatchestheoryA4\_leadA\_flipbit\_decomposition\.py[Lemma5\.21](https://arxiv.org/html/2608.10420#S5.Thmtheorem21)160 isomorphic pairs and 160 non\-isomorphic pairs, dimensions 2–5, checked exactly \(not by sampling\)distributional equality \(isomorphic case\) and orbit disjointness \(non\-isomorphic case\) each hold without exceptiontheoryA3\_val\_iso\_orbit\_uniformity\.py[Theorem5\.24](https://arxiv.org/html/2608.10420#S5.Thmtheorem24)\(canon∗\\mathrm\{canon\}^\{\*\}sub\-check\)69 instances \(dimensions 2–7, five generating families including a hand\-built copy of BDD\-OIA’s absorption structure\), generous tape budget; 32 further instances with tape budget deliberately tightened to force aborts69/69 exact orbit\-size match, zero aborts; representative set never exceeds the true orbit size on the tightened\-budget instances; amplifying the tape count recovers exact orbit sizes in all 32theoryA5\_orbit\_canon\_counting\_v2\_results\.json[Theorem5\.24](https://arxiv.org/html/2608.10420#S5.Thmtheorem24)\(end to end\)28 real instances, five generating families \(random, clause conjunctions, affine, constant, hand\-built BDD\-OIA absorption copy\); 3 trivial and 25 nontrivialAut​\(ΦC\)\\mathrm\{Aut\}\(\\Phi\_\{C\}\)laundered orbit\-representative set recovers the true orbit size exactly in 28/28 cases; single\-round trivial/nontrivial acceptance gap widens from a factor of about 4\.3 \(0\.410\.41vs\.0\.100\.10\) to about 31 \(0\.270\.27vs\.0\.0090\.009\) after nine rounds of majority votingtheoryA5\_setlowerbound\_on\_canon\_orbit\_v2\_results\.json
## References

- Agrawal and Thierauf \[2000\]Manindra Agrawal and Thomas Thierauf\.The formula isomorphism problem\.*SIAM Journal on Computing*, 30\(3\):990–1009, 2000\.A freely available 1996 preprint circulated under the title “The Boolean Isomorphism Problem\.”\.
- Babai and Moran \[1988\]László Babai and Shlomo Moran\.Arthur\-merlin games: A randomized proof system, and a hierarchy of complexity classes\.*Journal of Computer and System Sciences*, 36\(2\):254–276, 1988\.
- Barto and Kozik \[2017\]Libor Barto and Marcin Kozik\.Absorption in universal algebra and CSP\.In*The Constraint Satisfaction Problem: Complexity and Approximability*, volume 7 of*Dagstuhl Follow\-Ups*, pages 45–77\. Schloss Dagstuhl–Leibniz\-Zentrum für Informatik, 2017\.
- Beyersdorff et al\. \[2009\]Olaf Beyersdorff, Arne Meier, Michael Thomas, and Heribert Vollmer\.The complexity of propositional implication\.*Information Processing Letters*, 109\(18\):1071–1077, 2009\.arXiv:0811\.0959\.
- Böhler et al\. \[2012\]Elmar Böhler, Nadia Creignou, Matthias Galota, Steffen Reith, Henning Schnoor, and Heribert Vollmer\.Complexity classifications for different equivalence and audit problems for Boolean circuits\.*Logical Methods in Computer Science*, 8\(3:31\):1–25, 2012\.arXiv:1009\.1208\.
- Borchert et al\. \[1998\]Bernd Borchert, Desh Ranjan, and Frank Stephan\.On the computational complexity of some classical equivalence relations on Boolean functions\.*Theory of Computing Systems*, 31\(6\):679–693, 1998\.Preprint: Electronic Colloquium on Computational Complexity report TR96\-033 \(1996\)\.
- Bortolotti et al\. \[2024\]Samuele Bortolotti, Emanuele Marconato, Tommaso Carraro, Paolo Morettin, Emile van Krieken, Antonio Vergari, Stefano Teso, and Andrea Passerini\.A neuro\-symbolic benchmark suite for concept quality and reasoning shortcuts\.In*Advances in Neural Information Processing Systems 37 \(NeurIPS 2024\), Datasets and Benchmarks Track*, 2024\.
- Bshouty et al\. \[1996\]Nader H\. Bshouty, Richard Cleve, Ricard Gavaldà, Sampath Kannan, and Christino Tamon\.Oracles and queries that are sufficient for exact learning\.*Journal of Computer and System Sciences*, 52\(3\):421–433, 1996\.Electronic Colloquium on Computational Complexity report TR95\-015 \(1995\) is the freely available preprint\.
- Carlet \[2021\]Claude Carlet\.*Boolean Functions for Cryptography and Coding Theory*\.Cambridge University Press, 2021\.
- Cohen et al\. \[2006\]David A\. Cohen, Peter Jeavons, Christopher Jefferson, Karen E\. Petrie, and Barbara M\. Smith\.Constraint symmetry and solution symmetry\.In*Proceedings, The Twenty\-First National Conference on Artificial Intelligence and the Eighteenth Innovative Applications of Artificial Intelligence Conference, July 16\-20, 2006, Boston, Massachusetts, USA*, pages 1589–1592\. AAAI Press, 2006\.
- Crawford et al\. \[1996\]James M\. Crawford, Matthew L\. Ginsberg, Eugene M\. Luks, and Amitabha Roy\.Symmetry\-breaking predicates for search problems\.In*Proceedings of the Fifth International Conference on Principles of Knowledge Representation and Reasoning \(KR 1996\)*, pages 148–159\. Morgan Kaufmann, 1996\.
- Gent et al\. \[2006\]Ian P\. Gent, Karen E\. Petrie, and Jean\-François Puget\.Symmetry in constraint programming\.In Francesca Rossi, Peter van Beek, and Toby Walsh, editors,*Handbook of Constraint Programming*, chapter 10, pages 329–376\. Elsevier, 2006\.
- Goldwasser and Sipser \[1986\]Shafi Goldwasser and Michael Sipser\.Private coins versus public coins in interactive proof systems\.In*Proceedings of the Eighteenth Annual ACM Symposium on Theory of Computing \(STOC 1986\)*, pages 59–68\. ACM, 1986\.
- Manhaeve et al\. \[2018\]Robin Manhaeve, Sebastijan Dumančić, Angelika Kimmig, Thomas Demeester, and Luc De Raedt\.Deepproblog: Neural probabilistic logic programming\.In*Advances in Neural Information Processing Systems \(NeurIPS\)*, pages 3753–3763, 2018\.
- Marconato et al\. \[2023\]Emanuele Marconato, Stefano Teso, Antonio Vergari, and Andrea Passerini\.Not all neuro\-symbolic concepts are created equal: Analysis and mitigation of reasoning shortcuts\.In*Advances in Neural Information Processing Systems 36 \(NeurIPS 2023\)*, 2023\.
- McKay and Piperno \[2014\]Brendan D\. McKay and Adolfo Piperno\.Practical graph isomorphism, II\.*Journal of Symbolic Computation*, 60:94–112, 2014\.
- McKay et al\. \[2007\]Brendan D\. McKay, Alison Meynert, and Wendy Myrvold\.Small Latin squares, quasigroups, and loops\.*Journal of Combinatorial Designs*, 15\(2\):98–119, 2007\.
- Meier and Staffelbach \[1990\]Willi Meier and Othmar Staffelbach\.Nonlinearity criteria for cryptographic functions\.In*Advances in Cryptology – EUROCRYPT ’89*, volume 434 of*Lecture Notes in Computer Science*, pages 549–562\. Springer, 1990\.
- O’Donnell \[2014\]Ryan O’Donnell\.*Analysis of Boolean Functions*\.Cambridge University Press, 2014\.
- Puget \[2005\]Jean\-François Puget\.Automatic detection of variable and value symmetries\.In*Principles and Practice of Constraint Programming \(CP 2005\)*, volume 3709 of*Lecture Notes in Computer Science*, pages 475–489\. Springer, 2005\.
- Rothaus \[1976\]O\. S\. Rothaus\.On ‘bent’ functions\.*Journal of Combinatorial Theory, Series A*, 20\(3\):300–305, 1976\.
- Schaefer \[1978\]Thomas J\. Schaefer\.The complexity of satisfiability problems\.In*Proceedings of the Tenth Annual ACM Symposium on Theory of Computing \(STOC 1978\)*, pages 216–226\. ACM, 1978\.
- Schöning \[1988\]Uwe Schöning\.Graph isomorphism is in the low hierarchy\.*Journal of Computer and System Sciences*, 37\(3\):312–323, 1988\.
- Schöning \[1989\]Uwe Schöning\.Probabilistic complexity classes and lowness\.*Journal of Computer and System Sciences*, 39\(1\):84–100, 1989\.
- Stammer et al\. \[2021\]Wolfgang Stammer, Patrick Schramowski, and Kristian Kersting\.Right for the right concept: Revising neuro\-symbolic concepts by interacting with their explanations\.In*Proceedings of the IEEE/CVF Conference on Computer Vision and Pattern Recognition \(CVPR\)*, pages 3619–3629, 2021\.
- Takemura et al\. \[2026\]Akihiro Takemura, Katsumi Inoue, and Masaaki Nishino\.Constraint\-based analysis of reasoning shortcuts in neurosymbolic learning\.*arXiv preprint arXiv:2604\.23377*, 2026\.Accepted at the 23rd International Conference on Principles of Knowledge Representation and Reasoning \(KR 2026\); proceedings pagination not yet available at time of writing\.
- Valiant and Vazirani \[1986\]Leslie G\. Valiant and Vijay V\. Vazirani\.NP is as easy as detecting unique solutions\.*Theoretical Computer Science*, 47:85–93, 1986\.
- Xu et al\. \[2018\]Jingyi Xu, Zilu Zhang, Tal Friedman, Yitao Liang, and Guy Van den Broeck\.A semantic loss function for deep learning with symbolic knowledge\.In*Proceedings of the 35th International Conference on Machine Learning \(ICML 2018\)*, volume 80 of*Proceedings of Machine Learning Research*, pages 5502–5511, 2018\.