slug: campbell-2020-group-graph-reciprocal-pairs
bibkey: campbell2020reciprocal
doi: 10.48550/arXiv.2005.13566
url: https://arxiv.org/abs/2005.13566
triage: theorem
motivation_gids:
  - D5/S3/Combinatorics/ReciprocalPairs/GroupGraphReciprocalRefutation.result

Campbell’s classification of irreducible reciprocal pairs is false

Problem

Kirsty Campbell, Group-Graph Reciprocal Pairs, arXiv:2005.13566v1, Conjecture on page 3:

Conjecture: Let (Γ, G) be an irreducible reciprocal pair. Then one of the following hold:

1. (Γ, G) is one of the two trivial cases: (a) Γ is a null graph and G is any group with no odd permutations, (b) Γ is the complete graph with n vertices and G = Sn.
2. Γ is a 4-cycle and G ≅ Aut(Γ).
3. Γ is a k-star and G is defined in Theorem 1.

The source definitions and locators are in Campbell’s Library note. Cameron–Semeraro, The cycle polynomial of a permutation group, DOI 10.37236/7299, supplies the literature background. The quantified conventions and external Tier-1 settlement are preregistered in #16260.

Statement echo

Motivation

The settling GID is D5/S3/Combinatorics/ReciprocalPairs/GroupGraphReciprocalRefutation.result. Its counterexample is

$$\Gamma =3K_2\bigsqcup 2K_4,G=(S_2^3\times S_4^2)⋊S_3,$$

where the top $S_3$ permutes the three edge components naturally and permutes the two four-cliques through its sign. The graph has fourteen vertices. The full internal symmetric groups are permitted, but the two component layers share the parity of their top action.

Gap

The classification overlooks sign-coupled actions on disconnected graphs. Reciprocity need not force the action to split as a product of groups supported on the component layers. The conjecture with an added connectedness hypothesis is not settled by this example.

Route

The Lean module proves the counterexample without enumerating the group. Fixed maps are constant on SameCycle classes, so their number is a power of the number of colours. The cycle-factor decomposition gives the permutation sign. A nonproper colouring has an equal-colour edge; left multiplication by its transposition preserves fixedness and reverses sign, cancelling its signed contribution. Every group element fixing a proper colouring is even, so the remaining signed count is the proper fixed-colouring total.

A group generated by factors supported on separate parts preserves those parts. The action forces each clique layer into one part; every supported factor then has even top action. Such factors cannot generate the odd top element in the coupled group. For the other reducibility branch, graph isomorphisms force equal part sizes; the fixed-point-free edge mate makes each size even, while there are between two and five parts and fourteen vertices. These constraints are incompatible. An edge and a nonedge exclude the trivial graph classes, fourteen vertices exclude the four-cycle, and the absence of a universal vertex excludes every k-star.

Falsifier

The refutation would fail if the exhibited group did not preserve the graph, if the signed counting identity failed, if either conservative decomposition branch held, or if any listed graph condition held. The private proofs group_aut, reciprocal, irreducible and not_listed establish the corresponding facts on the live proof path of result.

Evidence

The sole public theorem is D5.S3.Combinatorics.ReciprocalPairs.GroupGraphReciprocalRefutation.result, with conclusion $\neg \mathrm{claim}$. The public surface also contains the eight source predicates and definitions; all construction and proof helpers are private. The axiom closure of every public declaration is contained in $\{\mathrm{propext},Classical.choice,Quot.sound\}$.

The public result is the designated refutation result (basis=refutes) and is exempt from four-slot escape registration (CLAUDE.md §3.9).

Experiment

Exact reciprocal-pair checks, pinned to commit e25f5648f110dcc641fb1bbd04bacdc6b6048d48, contain check.py, SHA-256 a7f8078c1c8134bcfa3a2871550a719cd32b512f29d4b848749c66cc44584814. The implementation seat reran the pinned script with python3 check.py, exit 0, ALL_OK. Run that command in the linked directory to reproduce the exact check.

The script enumerates the group and computes quotient chromatic polynomials by deletion–contraction, testing exactly $(a,b)=(2,4)$ and $(4,2)$. It gives $n=14$, $|G|=27648$ and reciprocity for $(2,4)$, and $n=16$, $|G|=331776$ and reciprocity for $(4,2)$. For $(2,4)$ the cycle-polynomial coefficients in increasing degree from zero to fourteen are

$$(0,0,0,1152,4656,7532,6392,3465,1859,1305,819,355,97,15,1).$$

These exact polynomial coefficients and group orders are computed data, not assertions of the Lean theorem.

Triage

What the settlement shows

1. Kernel-checked — mechanism at $(2,4)$. result, through private proper_fixed_sign, reciprocal, no_product_parts and irreducible, establishes the sign-coupled reciprocal pair outside the list. Proper fixed colourings force even permutations, while an odd top permutation obstructs generation by groups supported on separate parts. This is the failure mechanism of the classification.

2. Computed — two family members. The experiment above verifies reciprocity at exactly $(2,4)$ and $(4,2)$, with the stated command, exit code and script identity. Only $(2,4)$ is formalized. No computation over all distinct even parameters is claimed.

3. Proved in prose — the general family route. For distinct even $a,b\ge 2$, let $A(x)=x(x+1)\cdots (x+a-1)$ and $C(x)=x(x+1)\cdots (x+b-1)$. Summing the internal permutations over each component cycle gives

   $$F_G(x)=A(x{)}^{3}C(x{)}^2+3a!b!A(x{)}^{2}C(x)+2(a!{)}^{2}A(x)C(x{)}^2.$$

   The same cycle construction gives the proper-colouring total with rising factorials replaced by falling factorials: only the identity internal composite fixes a proper clique colouring. Since $a,b$ are even, both rising factors evaluated at $-c$ equal the corresponding falling factors, and $3a+2b$ is even. Thus this route gives reciprocity for every such pair. For a direct-product decomposition, every part is invariant under $G$ and therefore a union of its two vertex orbits, the two clique layers. Each proper supported factor fixes one layer, hence has even top action; their product misses the odd top action. For isomorphic parts, no cross-part edge allows each clique to remain whole. Equal part graphs would have the same numbers of $K_a$ and $K_b$ components, so the number of parts divides both three and two, and is one. The graph has an edge, a nonedge, no universal vertex and more than four vertices, excluding every listed graph class. This is a prose extension of the route in #16260, not a uniform Lean theorem or an experiment outside the two tested pairs.

4. Open — connected graphs. Whether Campbell’s conjecture holds after adding “connected $\Gamma$” is unresolved here. The witness is disconnected, so it provides no counterexample to that restriction.

5. Literature boundary — surviving source results. Campbell’s Theorem 1 on k-stars and the product and wreath-product constructions stated by Cameron–Semeraro remain independent proved source results. This refutation invalidates the claimed exhaustive classification, not those constructions. No classification of connected reciprocal pairs or of all disconnected coupled actions is established here.

The conservative reducibility test admits every source decomposition, and Listed admits every source-listed pair. Their combination makes claim a consequence of the source conjecture; its negation therefore suffices for the external settlement.

ASSUMED-UNVERIFIED

The source and literature screen in #16260 are attributed to the Claude Code orchestrator; the search seat’s screen is seat-reported. Literature exhaustiveness and publication priority remain ASSUMED-UNVERIFIED. The all-parameter family has the prose derivation above, but no uniform kernel-checked theorem in this delivery. The connected restriction remains open.