Unary Functions, Automorphisms, and Unlabeled First-Order Model Counting

Unary-function tractability

• Every fixed sentence in C^1_=[f], with one unary function and arbitrary finite relational vocabulary, has a model-counting sequence computable in polynomial time in n.The result exploits nested function terms but remains limited to one variable, one unary function, and bounded inspection of forward orbits.Source: §1 · p. 3

Hardness boundary

• Allowing either a second variable or a second unary function makes fixed model-counting functions #P_1-complete.Hardness holds in FO^2_=[f] without counting quantifiers and in constant-free universal FO^1_=[f, g] using only unary predicates besides the functions; unless FP = #P_1, tractability cannot extend to either language.Source: §1 · p. 3

Automorphism marking

• For a relational sentence φ, automorphism marking constructs φ_aut so that FOMC(φ_aut,n) = n!·UFOMC(φ,n).The added unary function is a relation-preserving permutation, and pairing each labeled model with one automorphism cancels the varying automorphism-group factor across isomorphism classes.Source: §1 · pp. 3–4

Unlabeled-to-labeled reductions

• For relational vocabularies of maximum arity k ≥ 2, eliminating the auxiliary function gives one-query reductions from unlabeled FO^k_= and C^k counting to labeled FO^{k+1}_= and C^{k+1} counting.The oracle is queried once at the same domain size, followed only by exact division by n!; for unary relational vocabularies, the construction remains within C2 and yields polynomial-time unlabeled counting for fixed C1.Source: §1 · p. 4

Scope and limitations

• The automorphism-marking reduction changes the counted objects rather than selecting canonical representatives, so it does not resolve the accepting-path complexity of unlabeled graph counting.Its exact reduction works by pairing each labeled representative with an automorphism and dividing the resulting labeled count by the known factor n!; it is distinct from symmetry breaking or canonical-form methods.Source: §1 · p. 4

2.1 Structures and Finite-Variable Fragments

• Structures use finite, nonempty labeled domains [n], with finite vocabularies, total functions, no constants, and finite-variable fragments such as C^1_=[f].Equality between nested unary-function terms is essential in the one-variable functional counting setting.Source: §2.1 · pp. 4–5

2.2 Labeled and Unlabeled Model Counting

• FOMC counts labeled n-element models of a fixed sentence, whereas UFOMC counts their isomorphism classes; every fixed-sentence FOMC function belongs to #P1.For graphs, FOMC(φgraph, n) = 2^(n choose 2), while UFOMC(φgraph, 3) = 4.Source: §2.2 · p. 5

2.3 Fixed-Sentence Oracle Reductions

• A fixed-sentence polynomial-time Turing reduction may query one unary oracle at an input-dependent domain size, with the target sentence fixed in advance.The reductions later used query at the same domain size and divide exactly by n!, an operation that is not parsimonious.Source: §2.3 · p. 6

2.4 Automorphisms and Labelings

• An n-element structure has n!/|Aut(B)| labeled copies, and each isomorphism class contributes exactly n! pairs of a labeled copy and one automorphism.This orbit–stabilizer consequence underlies the later connection between labeled and unlabeled enumeration.Source: §2.4 · p. 6

3 A Tractable One-Variable Fragment

• For every fixed one-variable sentence with counting quantifiers, one unary function, and arbitrary relation arities, model counting is computable in polynomial time in n.The result handles genuine nested terms, whose depth is bounded by the fixed sentence.Source: §3 · p. 6
• The algorithm summarizes bounded-depth orbit information with finitely many forward profiles, then uses truncated exponential generating functions for functional-digraph trees and cycles.Counting-quantifier classes retain cardinalities only up to fixed threshold-dependent bounds, making coefficient computation polynomial in n.Source: §3 · pp. 6–7
• Arbitrary-arity relation atoms reduce exactly to finitely many unary orbit-trace predicates, converting each fixed sentence to a monadic sentence with counts recoverable by exact powers-of-two arithmetic.The reduction supplies explicitly computable correction factors and preserves polynomial-time convertibility between the two model counts.Source: §3 · p. 7

3.1 Examples

• The tractability theorem covers endofunctions with prescribed 3-cycles, quasi-kernels, forbidden 2- and 3-cycles, and bounded-height two-coloured rooted forests.These examples demonstrate that nested-iterate constraints such as comparing f^3(x) with x remain tractable, including the normalized count for a prescribed quasi-kernel and the local colouring rule on height-bounded forests.Source: §3.1 · pp. 7–9
• The one-variable, one-function restriction is essential: a second variable or a second unary function yields hardness, although externally requiring f to be bijective preserves polynomial-time counting.The fragment cannot enforce bijectivity internally, but the algorithm applies when PERM(f) is supplied as an external axiom.Source: §3.1 · p. 9

4.1.1 The Graph Case

• In the graph case, permutation axioms force f to be a graph automorphism, so extended labeled models are exactly pairs consisting of a labeled graph and one of its automorphisms.This internally cancels varying automorphism-group sizes, an instance of Burnside’s lemma.Source: §4.1.1 · p. 10

4.1.2 The General Construction

• For every relational sentence φ, FOMC(φ_aut,n) = n!·UFOMC(φ,n), so unlabeled counting requires one labeled-counting query and exact division by n!.The automorphism-marking models correspond bijectively to pairs (A,π) with π an automorphism of A; each isomorphism class contributes exactly n! expansions.Source: §4.1.2 · p. 11
• For maximum arity k≥2, automorphism marking preserves FO^k_= and C^k variable width before relational elimination raises the bound to k+1.The assumption k≥2 is needed because expressing that the function is bijective requires two variables.Source: §4.1.2 · p. 11

4.2 Eliminating the Function Symbol

• The relational elimination encodes the permutation as a binary graph F and uses staged auxiliary relations, uniquely determined by the original relations and F, to avoid a 2r-variable preservation axiom.The resulting construction preserves the automorphism-marking count while using at most k+1 variables for vocabularies of arity at most k.Source: §4.2 · pp. 12–13
• For every fixed C1 sentence over a unary relational vocabulary, UFOMC(φ,n) is computable in polynomial time via a C2 relational encoding and division by n!.Over unary vocabularies, preserving all 1-types is equivalent to being an automorphism, enabling the sharper C1-to-C2 construction.Source: §4.2 · p. 13

5.1 A Second Variable

• Adding a second variable yields #P1-complete model counting, with unary-function successor shifts enabling a two-variable tableau construction.For each fixed linear order, accepting branches uniquely determine the tableau predicates; dividing out the n! order choices establishes hardness.Source: §5.1 · pp. 13–14
• The second-variable construction also yields only weighted equality-free hardness: it does not establish unweighted equality-free hardness or pure data-complexity hardness for one fixed weight assignment.Equality elimination requires polynomially many oracle queries for coefficient extraction with varying interpolation weights.Source: §5.1 · p. 14

5.2 A Second Unary Function

• With two unary functions, a fixed constant-free universal sentence using only unary predicates has a #P1-complete model-counting function.The proof encodes a finite family of unary functions into f and g, with explicit multiplicities that can be divided out exactly.Source: §5.2 · pp. 14, 16
• The two-function construction isolates computation on a distinguished odd cycle, uses local unary history to recover neighboring tape symbols, and obtains R_m = m! accU(n) before correcting extra components and cycles.A unary permutation supplies computation time points, while component and even-cycle inversions remove the additional structures allowed by universal sentences.Source: §5.2 · p. 15

Complexity boundary

• One variable with one unary function remains polynomial-time, but either a second variable or a second unary function suffices for hardness; in particular, [f,g]-FOMC is #P1-complete.The tractable case follows from bounded forward-orbit views and functional-digraph decompositions into cycles with rooted in-trees.Source: §6 · p. 16

Hardness mechanisms

• The two hardness proofs encode time and tape differently: two variables index both, whereas two functions use time elements and previous-visit functions, with the latter requiring a constant-factor domain expansion.The two-function construction also removes extra components by exact inversion.Source: §6 · p. 16

Automorphism marking

• Automorphism marking expresses the correction for orbit counting inside the logical specification, avoiding the incorrect naive division by n! while preserving the source sentence’s variable width.Without function symbols, encoding the permutation and its relational action requires one additional variable.Source: §6 · p. 16

Related tractability

• Bounded powers of a cyclic successor do not explain hardness: weighted C2 counting stays polynomial with linear orders and fixed predecessor relations, whereas function terms provide pair-shifting coupling.Replacing the shifted-pair constraint with predecessor relations would require more than two variables; these positive results are attributed to Tóth and Kuželka (2023) and Zou et al. (2025).Source: §6 · p. 16

Unlabeled counting

• The unlabeled reduction is not canonicalization: it uses one oracle query and division by n!, leaving accepting-path complexity and representative selection unresolved for many natural classes.For unlabeled graphs, Wilf (1982) conjectured non-polynomial-time computation, while Pak (2024) asks whether their counts belong to #P1; polynomial-size, efficiently computable automorphism groups can suffice for #P membership.Source: §6 · pp. 16–17

Open problems

• The main open problem is which finite-variable fragments support polynomial-time unlabeled counting rather than only reductions to labeled oracles.For labeled counting, tractability with one variable and one unary function persists under counting quantifiers and arbitrary relational arity, while complexity may depend on function-term nesting and relational occurrences.Source: §6 · p. 17

Scope

• The results concern ordinary model counting; extending the ideas to symmetric weighted model counting is possible with additional bookkeeping but is left for future work.Source: §6 · p. 17

Tractability context

• Prior lifted-inference work established polynomial-time data complexity for weighted model counting of fixed FO2 sentences (Van den Broeck, 2011; Van den Broeck et al., 2014; Beame et al., 2015).Source: §7 · p. 17
• Kuusisto and Lutz (2018, Theorems 3.8 and 4.7) prove related relational tractability results, but their methods do not cover genuine nested terms, span-three atoms, short-cycle equalities, or ordinary unweighted counting.Their functionality and U1 results are syntactically incomparable with this paper’s C1_= [f] theorem, which handles arbitrary relation arities and nested function terms.Source: §7 · p. 17

Positive extensions

• Theorem 1 combines prior positive extensions with exact unweighted counting for full one-variable counting logic C1_= [f], including genuinely nested unary-function terms and arbitrary relation arities.Related work extends tractability to counting quantifiers, semantic axioms, linear orders, and graph-polynomial methods (Kuželka, 2021; Tóth and Kuželka, 2023).Source: §7 · p. 18

Unary-function precedents

• Earlier unary-function work studied spectra, query evaluation, arithmetic history encodings, and vocabulary reductions, whereas this paper uses local profiles and exact multiplicities for model enumeration.Relevant antecedents include Durand et al. (1998), Durand and Olive (2006), Durand and More (2002), Grandjean (1990), and Lemma 19’s exact factor (rq)!q!.Source: §7 · p. 18

Hardness and symmetry

• The FO2_= [f] hardness proof adapts Beame et al. (2015)’s FO3 tableau encoding, using unary-function successor shifts to express local updates with two variables.Both constructions produce an n! labeling factor, while this paper isolates automorphism marking as a general reduction from unlabeled relational counting to fixed labeled model counting.Source: §7 · p. 18

Decidability and enumeration

• The results extend a sharp logical boundary: unary functions can make two-variable satisfiability undecidable with additional relations, while unary-predicate vocabularies remain decidable by Rabin’s tree theorem; group-action enumeration supplies the unlabeled perspective.This paper’s fixed-sentence, varying-domain-size hardness is a data-complexity analogue, and its automorphism-marking identity internalizes the classical quotient-counting mechanism (Pólya and Read, 1987; Pak, 2018, 2024).Source: §7 · pp. 18–19

• The section gives the full proofs of Theorems 1, 4, and 5.Source: §8 · p. 19

Section 8.2

• Section 8.2 fixes the source machine used in both hardness proofs.Source: §8 · p. 19

• The two logical encodings are proved separately.Source: §8 · p. 19

Appendix A

• Statements and proofs concerning bijectivity are collected in Appendix A.Source: §8 · p. 19

8.1 Proof of the One-Variable Tractability Theorem

• The unary-relation case of the one-variable theorem is polynomial-time computable, and the full proof later removes the unary-arity restriction.The argument proceeds through a unary-relation lemma before completing the theorem for arbitrary finite relational vocabularies.Source: §8.1 · p. 19

8.1.1 Technical Preliminaries

• Finite-dimensional monoid algebras and formal exponential generating functions track structure size and finitely capped logical summaries without analytic convergence.The variable x records domain size, while monoid-algebra basis elements combine capped counts across disjoint components.Source: §8.1.1 · pp. 19–20

8.1.2 The Monadic Core: Forward Profiles

• A d-profile is a complete satisfiable quantifier-free description of x,f(x),…,f^d(x), with finitely many computable profiles characterized by predicate types and equality patterns.The profile characterization uses an equivalence relation on positions compatible with applying f, ensuring realizability by a finite functional structure.Source: §8.1.2 · p. 21

8.1.3 Successor Compatibility and Visible Cycle Length

• Successor compatibility aligns overlapping profiles along function edges, while visible cycle length identifies cycles of length at most d and treats longer cycles as indistinguishable from transient vertices.These conditions characterize when profile assignments can be realized on functional digraphs, whose components are directed cycles with feeding trees.Source: §8.1.3 · pp. 22–23

8.1.4 Capped Cardinalities

• Because one-variable quantified subformulas depend only on profile classes, each relevant cardinality can be stored up to a fixed saturation threshold determined by the sentence.The resulting finite capped counters and Boolean acceptance map evaluate counting, existential, and universal quantifiers compositionally from the inside out.Source: §8.1.4 · pp. 23–24

8.1.5 Rooted In-Trees

• Rooted in-tree generating functions decorate vertices with compatible forward profiles and monoid-algebra weights, recording domain size and capped-cardinality states for later cycle assembly.Each functional-digraph component is built from a directed cycle whose vertices carry attached in-trees, with vertex weights combined by capped addition.Source: §8.1.5 · pp. 24–25
• Rooted in-tree series have uniquely determined coefficients and can be computed through degree n using polynomially many arithmetic operations.Only constantly many profile-indexed series are needed, and truncated addition, multiplication, exponentiation, and decoration operations remain polynomial in n.Source: §8.1.5 · p. 26

8.1.6 Directed Cycles and Components

• Functional digraphs are assembled from profile-compatible directed cycles and unordered components, yielding the capped-state model count; factorial-scaled coefficients have O(n log n) bits, so the full calculation is polynomial-time.Cycle traces remove the ℓ choices of origin, while the outer exponential forms the set of components; coefficient vectors are bounded by |Q|^n n^(n+1).Source: §8.1.6 · pp. 27, 29

8.1.7 Removing the Arity Restriction

• Higher-arity relation atoms are replaced by unary predicates over canonical orbit traces, with term depth at most 2d and an explicit multiplicity ratio preserving the model count.Canonical representatives prevent overlapping traces from duplicating tuples; constrained entries cancel, and the remaining free choices determine the ratio independently of f.Source: §8.1.7 · pp. 31–32
• The construction reduces apparently ternary information to unary predicate bits along function orbits, with each 3-cycle choosing one of two cyclic orientations.For n divisible by 3, the cycles contribute constrained orientation choices while all other tuples remain free; otherwise the count is zero.Source: §8.1.7 · pp. 32–33
• The final computation uses Lemmas 3 and 9, with exact division by fixed polynomial exponents and polynomial-bit-length integers.Nullary truth assignments add only constantly many computations, so the procedure runs in polynomial time for arbitrary finite relational vocabularies.Source: §8.1.7 · p. 33

• A fixed k-tape machine U has a #P_1-hard accepting-branch count on input 1^n, with every branch taking exactly an − 1 transitions.The machine uses distinguished finite-control states q0 and qacc, rather than logical constant symbols.Source: §8.2 · pp. 33, 35
• U converts a possibly variable-time source machine into equal-length branches by deterministic input copying, a fixed-state clock, simulation, and padding.The clock delays are implemented with finitely many control states, so no counter depending on n is required.Source: §8.2 · pp. 34–35
• The exact runtime is (2n + 1) + (pn − 2) = (p + 2)n − 1 = an − 1, where p is fixed and a := p + 2.Choosing p ≥ c + 3 provides enough clocked simulation steps for every source branch.Source: §8.2 · pp. 34–35
• The construction preserves a one-to-one correspondence between source-machine branches and branches of U, including acceptance status, because preprocessing, clocking, and padding add no nondeterministic choices.Thus U’s accepting-branch count retains the source machine’s #P_1-hardness.Source: §8.2 · p. 35
• Marked tape endpoints make the left boundary explicit, while choosing b ≥ max{a + 2, 3} ensures every head stays within the first bn cells.Mark preservation and omitted illegal left-moving rules do not change branch lengths or counts.Source: §8.2 · p. 35

8.3 Proof of the Two-Variable Hardness Theorem

• The construction adapts the FO3 tableau of Beame et al. (2015), following Trakhtenbrot’s encoding as presented by Libkin (2004, p. 167), while cyclic successor terms enable two-variable local constraints.The unary function f is forced to be a cyclic successor, allowing successor shifts to be expressed directly as nested terms.Source: §8.3 · p. 35

8.3.1 An Ordered Cyclic Successor

• CycSucc forces < to be a strict linear order with named minimum and maximum, f as its cyclic successor, and exactly n! labeled models on [n].Although transitivity is not axiomatized using only x and y, it follows on finite domains from the remaining axioms.Source: §8.3.1 · p. 36

8.3.2 Compiled Tableau Coordinates

• Fixed predicate families compile time and tape coordinates into rectangular grids, enforcing unique states, transitions, labels, one head per row, initialization, acceptance, and local updates for every n ≥1.The finite FO^2_= [f] sentence handles block boundaries, tape endpoints, position wraps, time wraps, and n = 1.Source: §8.3.2 · pp. 37, 41

8.3.3 Local Transitions

• Local control and update clauses are equivalent to applying the selected enabled transition, synchronizing all tapes and covering every nonfinal time and tape-cell case.The fixed sentence Φ uses only x and y; no transition clause is imposed after the final time.Source: §8.3.3 · p. 42

8.3.4 Correctness and Counting

• For each fixed cyclic-order model, satisfying tableau interpretations are in bijection with accepting computation branches of U on input 1^n, with no extra final-time multiplicity.Initial clauses determine the first configuration, local simulation determines each successor, and the final-state clause forces acceptance.Source: §8.3.4 · pp. 42–43
• FOMC_Φ is #P_1-complete: one query yields n!·acc_U(n), so exact division by n! recovers accepting-branch counts.Hardness follows from the tableau bijection and the n! cyclic-order skeletons; membership holds for every fixed first-order sentence.Source: §8.3.4 · pp. 42–43

8.4 Proof of the Two-Function Hardness Theorem

• Theorem 5 is proved by reducing the fixed source-machine computation to a constant-free one-variable construction with two unary functions.The proof uses the source machine fixed earlier and introduces structural predicates, functions, and machine-transition predicates as finite logical vocabulary.Source: §8.4 · p. 43

8.4.1 Slowing the common source machine

• The source machine is slowed to a fixed machine V with exactly 2an transitions on every branch, while marked first cells and transition restrictions preserve the intended simulation.Each original transition is replaced by two transitions through a private intermediate state, with deterministic no-op transitions added before and after.Source: §8.4.1 · p. 43

8.4.2 Rooted permutation components

• Parity predicates force every root cycle to have odd length and every satellite cycle to have even length, with unique root coloring but two satellite colorings.The alternation condition is exempted only on the distinguished root edge, yielding the stated parity separation.Source: §8.4.2 · p. 44
• The auxiliary bijections d and h isolate exactly the root cycle in each π-component by conjugating S with S^2 and comparing their cycle structures.An active satellite would contribute one cycle to S but two to S^2, so no satellite can remain active.Source: §8.4.2 · pp. 44–45
• For root length 4N+1, the uniquely determined inverse h identifies canonical quarter- and half-cycle markers, turning the root into a linear interval and logical time line.The marked points satisfy q1 = S^N(c), q2 = S^2N(c), and b = S^4N(c), after which the cycle is cut at b → c.Source: §8.4.2 · p. 45

8.4.3 Preparing the unary input on the root

• The root is partitioned into build, rewind, and machine phases of lengths an, an, and 2an transitions, using a modulo-a clock to trigger exactly n preparation moves in each prefix.The first interval writes 1^n, the second rewinds the input head, and the final interval has the length required for the machine simulation.Source: §8.4.3 · pp. 46–47
• At q2, the deterministic preparation yields precisely V’s initial configuration on input 1^n: the input head is at the marked first cell and work tapes are blank.The build writes one symbol at each Z0-point, while rewind makes exactly n left moves and preserves scanned symbols.Source: §8.4.3 · p. 48
• During the machine phase, predicates Dδ select named transitions of V, uniquely determine tape actions and control-state evolution, and enforce entry into the accepting state at the final point.Read consistency is deferred to previous-visit functions and clauses that compare each selected transition’s prescribed symbol with the symbol last written at the entered cell.Source: §8.4.3 · pp. 48–49

History construction

• Previous-visit functions record the latest earlier visits to the cells immediately left and right of each head position, sufficing to verify motion and tape contents.Because the head moves only between neighbouring cells, these unary maps reconstruct when destination cells were last visited and which symbols they contain.Source: §8.4.4 · p. 49

Read verification

• The read clauses preserve history across preparation, rewind, and machine phases, and the left-move legality condition prevents satisfying assignments from moving below the marked first tape cell.Machine-phase reads may therefore rely on symbols written during deterministic preparation, while every satisfying assignment describes a legal semi-infinite tape history.Source: §8.4.4 · pp. 49, 52

History construction

• The nearest-neighbour recurrence updates pointers by nested unary lookups: right moves set the new left pointer to the prior time, left moves use nested left lookups, and stays preserve both.The recurrence follows from the head’s local movement and the latest-visit semantics, including undefined right-neighbour history and the left endpoint.Source: §8.4.4 · p. 50

Unary encoding

• Totalizing undefined pointers with the current time as a fixed-point dummy value makes all updates expressible as unary terms in one variable and uniquely determines the functions along the root interval.The predicate Rτ abbreviates whether the right neighbour was visited, while off-root identity constraints fix otherwise unused values.Source: §8.4.4 · pp. 50–52

Branch–root correspondence

• For structural models of size m = 4an+1 whose domain is the active root cycle, computational expansions are in bijection with accepting branches of U on input 1^n.Each accepting branch determines exactly one expansion, and each satisfying expansion selects a state-consistent accepting transition sequence.Source: §8.4.4 · pp. 52–53

Exact root count

• R_r counts labeled models on r elements consisting of one π-component with no satellites, equivalently with the whole domain as the active root cycle.Source: §8.4.5 · p. 53
• At m = 4an + 1, Proposition 2 establishes the root multiplicity for these single-component models.Source: §8.4.5 · p. 53
• Fixing a directed m-cycle leaves the component root as the only choice, while π, P, E, A, d, h, phase predicates, and the modulo-a counter are uniquely determined; Lemma 18 then contributes accU(n) expansions.Source: §8.4.5 · p. 53
• The following section recovers R_m despite Θ allowing arbitrary sets of components and arbitrary even satellites within each component.Source: §8.4.5 · p. 53

SET inversion across components

• Because Θ preserves π-components and has universal one-variable clauses, its models are unordered collections of one-component models, yielding a recurrence that sequentially recovers K1,…,Kℓ from M1,…,Mℓ.The recurrence singles out the component containing label 1 and combines it with an arbitrary model on the remaining labels.Source: §8.4.6 · p. 54

Removing satellites from a one-component count

• Satellite structures exist only on an even number of labels and are counted by (2s)!/s! times the number of permutations of an s-element set.Even cycles of S admit two alternating E-assignments each, while the remaining structure is uniquely determined.Source: §8.4.6 · pp. 54–55
• Using the satellite count to relate one-component counts Kℓ to active-root-cycle counts Rr, equation (104) recovers Rℓ from M1,…,Mℓ.For odd ℓ, one chooses the root labels and an Rr structure, while the remaining labels contribute (ℓ−r)! satellite arrangements; comparing consecutive identities isolates the final term.Source: §8.4.6 · p. 55

8.4.7 Exact compression to two unary functions

• Lemma 19 effectively replaces any fixed finite family of unary functions by two functions f and g, while preserving the source model counts up to an explicit multiplier.The construction uses fresh unary layer predicates and remains constant-free; if the source is universal, the translation is universal as well.Source: §8.4.7 · p. 55
• The r layers are partitioned equally, f bijectively cycles between them, and source predicates are restricted to the base layer L0.Equal layer sizes force FOMC(Ψ♭, s) = 0 when r does not divide s.Source: §8.4.7 · pp. 55–56
• The translation recursively replaces source terms with f- and g-terms, restricts quantifiers to L0, and introduces no additional first-order variables.Thus the resulting sentence remains in FO1 with exactly the two unary functions f and g.Source: §8.4.7 · p. 56
• The second function g encodes all r source functions by preserving layers and transporting each source function through the f-induced bijections.Once the layers and f are fixed, choosing the source functions is equivalent to choosing a layer-preserving g, so g is uniquely determined.Source: §8.4.7 · p. 56

8.4.8 Completing the reduction

• The final reduction queries the fixed target counting function at domain sizes rk for 1 ≤ k ≤ m, with m = O(n), and recovers the needed values by exact division.All queried domain sizes are O(n), and the counts have O(n log n) bits, making the arithmetic polynomial-time.Source: §8.4.8 · p. 57
• The completed construction proves #P_1-hardness of N ↦ FOMC(Ξ, N), and together with membership establishes Theorem 5.The proof uses polynomial-time factorial multiplications, exact divisions, binomial coefficients, and recurrence computations.Source: §8.4.8 · p. 57

A Bijectivity and the Permutation Axiom

• No finite collection of unary predicates can provide a one-variable certificate equivalent to bijectivity for every finite endofunction.The proof rewires a sufficiently large directed cycle while preserving all bounded profiles and equality patterns, producing a nonbijective function that satisfies the same sentence.Source: A Bijectivity and the Permutation Axiom · pp. 57–58
• For every fixed φ ∈ C^1_=[f], counting models over finite relational vocabularies subject to the external permutation axiom is computable in polynomial time in n.On finite domains, bijectivity is exactly that f is a permutation, but the axiom itself uses two variables and is not in C^1_=[f].Source: §3 · p. 6, A Bijectivity and the Permutation Axiom · p. 58
• Under the permutation restriction, the generating-function method deletes transient tree decorations, leaving only directed-cycle components and preserving polynomial-time coefficient computation.For arbitrary relation arities, monadic trace compression and the same exact power-of-two correction extend the result beyond the monadic case.Source: A Bijectivity and the Permutation Axiom · pp. 58–59
• For every fixed q ≥ 1, a sentence in C^1_=[f] forces f to be a permutation whose cycle lengths all divide q.Thus the one-variable fragment cannot express unrestricted bijectivity, but it can define restricted classes of permutations.Source: A Bijectivity and the Permutation Axiom · p. 59