Introduction
Background
The Exponential Time Hypothesis (ETH) of Impagliazzo and Paturi [27 ] asserts that there is δ > 0 \delta> 0 δ > 0 n n n O ( 2 δ n ) O(2^{\delta n}) O ( 2 δ n ) [28 ] it underlies a large body of conditional lower bounds [33 , 18 ] . Among them is the statement that, unless ETH fails, Hamiltonian Cycle has no 2 o ( n + m ) 2^{o(n+m)} 2 o ( n + m ) n n n m m m [18 Ch. 14] (see also [33 Thm. 3.3] , stated there as the absence of a 2 o ( n ) 2^{o(n)} 2 o ( n )
In October 2026 two manuscripts appeared, by OpenAI [35 ] and by Anthropic [15 ] , each claiming a deterministic algorithm that counts the satisfying assignments of a k k k claimed results that are, at the time of writing, still under review by the community. We write [A] for the Anthropic manuscript [15 ] . Its Main Theorem gives one deterministic algorithm that counts the models of a k k k m m m n n n
2 O ( min { k m / log m , k 2 n log log n / log n } ) 2^{O(\min\{km/\sqrt{\log m},\, k^2n\log\log n/\sqrt{\log n}\})} 2 O ( m i n { k m / l o g m , k 2 n l o g l o g n / l o g n }) with an absolute constant in the O O O [35 ] that is machine-checked is 2 O k ( ρ ( n ) ) 2^{O_k(\rho(n))} 2 O k ( ρ ( n )) ρ ( N ) = N ( log log N ) 2 / log N \rho(N)=N(\log\log N)^2/\sqrt{\log N} ρ ( N ) = N ( log log N ) 2 / log N
A refutation of ETH does not by itself yield fast algorithms for connectivity problems. ETH lower bounds for Hamiltonicity come from linear-size reductions from 3-SAT to Hamiltonian Cycle; an algorithm needs the reverse direction, an encoding of Hamiltonicity as a counting problem on O ( n ) O(n) O ( n ) local problems.
Results
Throughout, G = ( V , E ) G=(V,E) G = ( V , E ) n = ∣ V ∣ n=|V| n = ∣ V ∣ m = ∣ E ∣ m=|E| m = ∣ E ∣ # H C ( G ) \#\mathrm{HC}(G) # HC ( G ) G G G # H C ( K 4 ) = 3 \#\mathrm{HC}(K_4)=3 # HC ( K 4 ) = 3 # H C ( G ) = 0 \#\mathrm{HC}(G)=0 # HC ( G ) = 0 n ≤ 2 n\le2 n ≤ 2
Our main results are corollaries of [A]: they are conditional on three results of [A], which we recall precisely in § 2 , and they inherit whatever doubt attaches to those results. If [A] is wrong, the theorems below lose their proofs.
Hypothesis (HA _A A The following statements of [A] hold as stated there: Lemma 8, case (i) (the reduction from general networks to cliques, Theorem 2.4); Theorem A(a), (b) (one algorithm for the ( K ℓ , λ ) (K_\ell,\lambda) ( K ℓ , λ ) ℓ \ell ℓ ( 1 / 2 , c ) (1/\sqrt{2},c) ( 1/ 2 , c )
For Theorem 1.1 it suffices to have the pieces of [A, Lemma 2] (parameter 11 / 12 11/12 11/12
Theorem 1.1 (Exact counting, fixed density). Assume (HA _A A δ > 0 \delta> 0 δ > 0 D ≥ 1 D \ge1 D ≥ 1 G G G n n n D n Dn D n # H C ( G ) \#\mathrm{HC}(G) # HC ( G ) O ( 2 δ n ) O(2^{\delta n}) O ( 2 δ n )
Theorem 1.2 (Exact counting, explicit rate). Assume ( H A ) (\mathrm{H}_{\mathrm{A}}) ( H A ) There are an absolute constant C ∗ C^{*} C ∗ and one deterministic algorithm that, given any graph G G G with n ≥ 2 n \ge2 n ≥ 2 vertices and m m m # H C ( G ) \#\mathrm{HC}(G) # HC ( G ) within 2 C ∗ max ( m , n ) / log n 2^{C^{*}\max(m,n)/\sqrt{\log n}} 2 C ∗ m a x ( m , n ) / l o g n operations. In particular it runs in time 2 O ( D n / log n ) 2^{O(Dn/\sqrt{\log n})} 2 O ( D n / l o g n ) on graphs with m ≤ D n m \le Dn m ≤ D n where the O O O constant is absolute and D D D may depend on n n n
When the density grows with n n n d ˉ : = 2 m / n \bar d := 2m/n d ˉ := 2 m / n Δ \Delta Δ
Theorem 1.3 (Exact counting, maximum/average degree; machine-checked). Assume ( H A ) (\mathrm{H}_{\mathrm{A}}) ( H A ) There are an absolute constant C ♯ C^{\sharp} C ♯ and one deterministic algorithm that, given any graph G G G with n ≥ 2 n \ge2 n ≥ 2 vertices, average degree d ˉ \bar d d ˉ and maximum degree Δ \Delta Δ outputs # H C ( G ) \#\mathrm{HC}(G) # HC ( G ) within
2 C ♯ n log ( 2 e max ( d ˉ , 2 ) ) / log n ≤ 2 C ♯ n log ( 2 e max ( Δ , 2 ) ) / log n 2^{C^{\sharp} n\log(2e\max(\bar d,2))/\sqrt{\log n}} \le2^{C^{\sharp} n\log(2e\max(\Delta,2))/\sqrt{\log n}} 2 C ♯ n l o g ( 2 e m a x ( d ˉ , 2 )) / l o g n ≤ 2 C ♯ n l o g ( 2 e m a x ( Δ , 2 )) / l o g n operations. In particular it runs in time 2 o ( n ) 2^{o(n)} 2 o ( n ) whenever log d ˉ = o ( log n ) \log\bar d=o(\sqrt{\log n}) log d ˉ = o ( log n ) for example for d ˉ = ( log n ) O ( 1 ) \bar d=(\log n)^{O(1)} d ˉ = ( log n ) O ( 1 ) or d ˉ = 2 ( log n ) 0.49 \bar d=2^{(\log n)^{0.49}} d ˉ = 2 ( l o g n ) 0.49
Theorem 1.3 is machine-checked: the Lean theorem theorem3 gives one Turing machine that outputs # H C ( G ) \#\mathrm{HC}(G) # HC ( G ) ⌊ C ⋅ 2 C n log 2 ( 2 m / n + 2 ) / log 2 ( n + 2 ) ⌋ \left\lfloor C\cdot2^{Cn\log_2(2m/n+2)/\sqrt{\log_2(n+2)}}\right\rfloor ⌊ C ⋅ 2 C n l o g 2 ( 2 m / n + 2 ) / l o g 2 ( n + 2 ) ⌋ G G G n n n m m m theorem3\_maxdeg gives the same with log 2 ( Δ + 2 ) \log_2(\Delta+2) log 2 ( Δ + 2 ) § 12 ). For bounded d ˉ \bar d d ˉ 2 O ( n / log n ) 2^{O(n/\sqrt{\log n})} 2 O ( n / l o g n ) d ˉ → ∞ \bar d\to\infty d ˉ → ∞ set of used crossing edges between them, rank-encoded, and the labels of those edges, so the total number of shared bits is about 2 n log ( 2 e d ˉ ) 2n\log(2e\bar d) 2 n log ( 2 e d ˉ ) 2 log 2 5 ⋅ m ≈ 2.32 d ˉ n 2\log_2 5\cdot m\approx2.32\bar d n 2 log 2 5 ⋅ m ≈ 2.32 d ˉ n d ˉ = Θ ( n ) \bar d=\Theta(n) d ˉ = Θ ( n ) 2 O ( n log n ) 2^{O(n\sqrt{\log n})} 2 O ( n l o g n ) 2 n 2^n 2 n § 1.6 ).
Corollary 1.4 (Decision, search and paths; machine-checked). Assume ( H A ) (\mathrm{H}_{\mathrm{A}}) ( H A ) C C C G G G n ≥ 2 n\ge2 n ≥ 2 n 2 + 1 n^2+1 n 2 + 1 G G G G G G
In Lean these are decision\_TM, search\_TM (fixed density) and decision\_TM\_rate, search\_TM\_rate (rate form), and for paths hamPaths\_count\_TM, hamPaths\_decision\_TM, hamPaths\_search\_TM and their \_rate versions, with the bijection card\_hamPaths\_eq; all use the standard axioms only.
The weighted version is the sparse travelling-salesman problem; it is machine-checked as well.
Theorem 1.5 (Sparse TSP; machine-checked). Assume ( H A ) (\mathrm{H}_{\mathrm{A}}) ( H A ) For every real δ > 0 \delta>0 δ > 0 and every D ≥ 1 D\ge1 D ≥ 1 there are a deterministic algorithm and a constant C C C such that, given a graph G G G with $n vertices and at most D n Dn D n edges and integer edge weights w : E → { 0 , … , W } w:E\to\{0,\ldots,W\} w : E → { 0 , … , W } the algorithm outputs within C ⋅ 2 δ n ( W + 2 ) C ∗ s t e p s t h e i n t e g e r ∗ C\cdot2^{\delta n}(W+2)^C *steps the integer* C ⋅ 2 δ n ( W + 2 ) C ∗ s t e p s t h e in t e g er ∗ b = n 2 + n b=n^2+n b = n 2 + n the sum running over the Hamiltonian cycles H H H of G G G digit j j j is n n n times the number of tours of weight exactly j j j the minimum tour weight is the position of the lowest non-zero digit, and the number of optimal tours is that digit divided by n n n In particular the sparse TSP is solved exactly, with its optimum counted, in time 2 δ n poly ( W ) 2^{\delta n}\operatorname{poly}(W) 2 δ n poly ( W ) for every δ > 0 \delta>0 δ > 0 subexponential for all weights W = 2 o ( n ) W=2^{o(n)} W = 2 o ( n )
In Lean this is theoremTSP and theoremTSP\_decode, built on [A]’s development with the standard axioms only (§ 12 ). What it does not give is as important: the running time grows with the number of edges, so dense and metric instances (complete graphs, Euclidean TSP) are untouched, and the O ∗ ( 2 n ) O^{*}(2^n) O ∗ ( 2 n ) [3 , 26 ] remains essentially the record there (improved only to 2 n − Ω ( n / log ( n W ) ) poly ( W ) 2^{n-\Omega(\sqrt{n/\log(nW)})}\operatorname{poly}(W) 2 n − Ω ( n / l o g ( nW ) ) poly ( W ) W W W [5 ] , and, for bipartite instances, to O ( 1.9999 n ) O(1.9999^n) O ( 1.999 9 n ) [34 ] ); and weights W = 2 Θ ( n ) W = 2^{\Theta(n)} W = 2 Θ ( n ) § 1.6 ). The identity behind the theorem is the Kronecker substitution z = 2 b z = 2^b z = 2 b n n n ∑ H z w ( H ) = ∑ X z w ( X ) κ ( X ) \sum_H z^{w(H)} = \sum_X z^{w(X)}\kappa(X) ∑ H z w ( H ) = ∑ X z w ( X ) κ ( X ) Theorem 5.7 .
The next two results are weaker but depend only on the top-level theorems of the labs, which are themselves machine-checked; the first is machine-checked end to end on top of them.
Theorem 1.6 (Parity; machine-checked). There is one deterministic algorithm that, for every graph G G G n ≥ 2 n \ge2 n ≥ 2 m m m # H C ( G ) m o d 2 \#\mathrm{HC}(G) \bmod2 # HC ( G ) mod 2 2 O ( ( m + n ) / log ( m + n ) ) 2^{O((m+n)/\sqrt{\log(m+n)})} 2 O (( m + n ) / l o g ( m + n ) ) [35 ] , it does so in time 2 O ( ρ ( 5 m + 3 n ) ) 2^{O(\rho(5m+3n))} 2 O ( ρ ( 5 m + 3 n )) p r o p e x t \mathtt{propext} propext C l a s s i c a l . c h o i c e \mathtt{Classical.choice} Classical.choice Q u o t . s o u n d \mathtt{Quot.sound} Quot.sound
Theorem 1.7 (Randomized decision).
(a) (Machine-checked, assuming the Lean theorem of [35 ] .) For every Δ \Delta Δ δ > 0 \delta> 0 δ > 0 Δ \Delta Δ 2 δ n 2^{\delta n} 2 δ n
An earlier version also stated a part (b), a randomized 2 O D ( n ( log log n ) 2 / log n ) 2^{O_D(n(\log\log n)^2/\sqrt{\log n})} 2 O D ( n ( l o g l o g n ) 2 / l o g n ) ∣ E ∣ ≤ D n |E| \le Dn ∣ E ∣ ≤ D n Theorem 1.2 (deterministic, and faster) and is no longer claimed; see Theorem 10.3.
Theorem 1.6 and Theorem 1.7 (a) are from an earlier stage of this work and are superseded, as statements, by Theorems 1.1 and 1.4 ; we include them because they rest on far less. In (a), Lean checks soundness, the success fraction and the machine; only the outer loop of independent trials is not modelled.
§ 11 records further consequences of the same template, for example directed Hamiltonian cycles, TSP with polynomial weights, Steiner trees, feedback vertex sets and the Tutte polynomial on the line y = 1 y = 1 y = 1 not fully proved here.
1.3. Prior work. No subexponential algorithm for Hamiltonicity on general sparse graphs was known, consistent with ETH. Planar, bounded-genus and minor-free graphs admit 2 O ( n ) 2^{O(\sqrt{n})} 2 O ( n ) Table 1 lists the best previous bounds in the settings relevant here; all are of the form c n c^n c n c > 1 c > 1 c > 1 ( 2 − ε ) n (2-\varepsilon)^n ( 2 − ε ) n ε → 0 \varepsilon\to0 ε → 0 O ∗ ( 1.657 n ) O^*(1.657^n) O ∗ ( 1.65 7 n ) [4 ] does not depend on the degree. The bound of [8 ] is for TSP (hence decision), by a trimmed Bellman–Held–Karp dynamic programme [3 , 26 ] ; it is not stated for counting. For small fixed degree, unconditional counting is much faster than ( 2 − ε ) n (2-\varepsilon)^n ( 2 − ε ) n O ( 2 3 n / 8 ) O(2^{3n/8}) O ( 2 3 n /8 ) [24 ] , or in 6 n / 6 + o ( n ) 6^{n/6+o(n)} 6 n /6 + o ( n ) p w ≤ n / 6 + o ( n ) \mathrm{pw} \le n/6+o(n) pw ≤ n /6 + o ( n ) [25 ] and the 6 p w 6^{\mathrm{pw}} 6 pw [10 ] .
Table 1. Previous bounds and the bounds of this paper (all of the latter conditional; see the text). Here ρ ( N ) = N ( log log N ) 2 / log N \rho(N)=N(\log\log N)^2/\sqrt{\log N} ρ ( N ) = N ( log log N ) 2 / log N
Two lines of earlier work are closely related to our technique. Cut&Count [20 ] reduces connectivity to counting modulo 2: a 2-factor X X X 2 cc ( X ) − 1 2^{\operatorname{cc}(X)-1} 2 cc ( X ) − 1 X X X Theorems 1.6 and 1.7 . Björklund’s determinant sums [4 ] pair cycle covers with determinants to enforce connectivity; the identity of Theorem 4.1 below is of the same folklore kind. The fermionic, or Grassmann, form of the matrix-tree theorem that we use is a special case of the generalisation of Kirchhoff’s theorem to non-Gaussian Grassmann integrals by Caracciolo, Jacobsen, Saleur, Sokal and Sportiello [14 ] . Rank bounds for the matchings-connectivity matrix (over F 2 \mathbb{F}_2 F 2 [19 ] , and over Q \mathbb{Q} Q [17 ] , building on Raz and Spieker’s bound for its bipartite variant [36 ] ) show that, across one cut, connectivity costs only O ( b ) O(b) O ( b ) Q \mathbb{Q} Q b log b b\log b b log b
On the hardness side, Dell, Husfeldt, Marx, Taslaman and Wahlén [22 ] and Curticapean [16 ] proved #ETH lower bounds for the permanent, perfect matchings and the Tutte polynomial on sparse graphs, and Brand, Dell and Roth [12 ] completed the #ETH dichotomy for the Tutte plane by treating the line y = 1 y=1 y = 1 y = 1 y=1 y = 1 § 11 .
Overview of the technique
§ 4 starts from the identity
n ⋅ # H C ( G ) = ∑ X a 2-factor of G κ ( V , X ) , (1) n\cdot\#\mathrm{HC}(G)=\sum_{X\text{ a 2-factor of }G}\kappa(V,X), \tag*{(1)} n ⋅ # HC ( G ) = X a 2-factor of G ∑ κ ( V , X ) , (1) where κ ( V , X ) \kappa(V,X) κ ( V , X ) ( V , X ) (V,X) ( V , X ) n n n 1 + q e 1+q_e 1 + q e log n \log n log n
We partition V V V g g g log 2 5 \log_2 5 log 2 5 Table 2 ). Moving the pieces of the crossing edges into blob order produces a sign. We show that this sign factors as a product of blob-local signs and an interleaving sign ( − 1 ) ∑ a < c < b < d π a b π c d (-1)^{\sum_{a<c<b<d}\pi_{ab}\pi_{cd}} ( − 1 ) ∑ a < c < b < d π ab π c d π a b \pi_{ab} π ab a a a ({xref}Theorems 5.3 and 5.5). The interleaving sign is paid for by $O(g^3)$ parity-copy bits ({xref}Theorem 5.6). The outcome is a network in the sense of [A] with arbitrary integer node tables and about $2\log_2 5\cdot m+g^3$ shared bits, whose value is $n\cdot\#\mathrm{HC}(G)$ ({xref}Theorem 6.3). [A]’s network theorem then evaluates it ({xref}Section 7`). One trap is that [A]’s cost depends on the largest number of bits at one node, so a vertex of degree Θ ( n ) \Theta(n) Θ ( n ) § 8 replaces the per-edge digits by a rank code of the set of used crossing edges between two blobs, which costs only logarithmically in the degree and needs no branching (Theorem 1.3 ).
Table 2. Labels of a crossing edge e k e_k e k s s s t t t
What is new here
Little of the above is new in isolation, and we want to be precise about the credits. The identity (1.1), matrix-tree on 2-factors, is folklore. The fermionic matrix-tree theorem, which writes the number of spanning trees as a Berezin integral of ∏ e ( 1 + q e ) \prod_e(1+q_e) ∏ e ( 1 + q e ) [14 ] . Partitioning the vertices into blobs and paying for connectivity across the cuts is the pattern of Cut&Count [20 ] . Björklund’s determinant sums [4 ] (FOCS 2010, SIAM J. Comput. 2014) pair cycle covers with determinants to enforce connectivity, a closely related pattern, though there the determinant is evaluated over a field of characteristic 2 and the aim is a randomized O ∗ ( 1.657 n ) O^*(1.657^n) O ∗ ( 1.65 7 n ) O ( 1 ) O(1) O ( 1 ) log 2 5 \log_2 5 log 2 5 O ( g 3 ) O(g^3) O ( g 3 ) g g g b log b b\log b b log b
Status of the results
The proofs of § 3 to § 7 and 9 are complete, conditional on ( H A ) (\mathrm{H}_A) ( H A ) ∑ a σ a χ a I a = n ⋅ # H C ( G ) \sum_a \sigma_a\chi_a I_a=n\cdot\#\mathrm{HC}(G) ∑ a σ a χ a I a = n ⋅ # HC ( G ) Theorems 5.7 and 6.3 and the parameter bounds of Theorem 6.4, with the network stated in [A]’s own Lean format. The blob-table procedure is formalised as well, and Theorems 1.1 and 1.2 are both formally verified in Lean end to end, as statements about Turing machines built on [A]’s Lean development [38 ] , with only the standard axioms (theorem1, theorem2); a fresh kernel replay with leanchecker has passed for both theorem1 and theorem2. The sparse TSP theorem (Theorem 1.5 ) is formally verified at the same level (theoremTSP, theoremTSP\_decode). Theorem 1.3 is the exception: its proof (§ 8 ) is written out and was checked numerically and by an independent AI referee, who found it sound, but it is not formalised. § 12 gives the details. The bounds are purely asymptotic: as for the SAT algorithms themselves, the crossover with brute force is astronomically large.
Limitations
The following should be read together with § 12 .
(a) Everything is conditional. The main theorems rest on the claimed ETH refutation of [A], through ( H A ) (\mathrm{H}_A) ( H A )
(b) The Lean proofs here were written and reviewed by AI. They were produced by AI agents and reviewed by an AI coordinator. No human has yet checked that the formal statements say what the printed theorems say. A human reader who wants to do so needs to read about five definitions: hamCycles (the set of Hamiltonian cycles being counted, and that it counts each cycle once as a subgraph); GraphProblems.code (the input encoding of a graph, and that it is the adjacency matrix); Outputs (what it means for the machine to output # H C ( G ) \#\mathrm{HC}(G) # HC ( G ) theorem1 and theorem2 themselves, in particular that the step bound is ⌈ C ⋅ 2 δ n ⌉ \lceil C\cdot2^{\delta n}\rceil ⌈ C ⋅ 2 δ n ⌉ ⌈ C ⋅ 2 C ( m + n ) / log 2 ( n + 2 ) ⌉ \lceil C\cdot2^{C(m+n)/\sqrt{\log_2(n+2)}}\rceil ⌈ C ⋅ 2 C ( m + n ) / l o g 2 ( n + 2 ) ⌉ C C C G G G 2.6 is assumed.
(c) Sparse graphs only. The network of § 6 has about 2 log 2 5 2\log_2 5 2 log 2 5 Theorem 1.2 beats 2 n 2^n 2 n m = o ( n log n ) m = o(n\sqrt{\log n}) m = o ( n log n ) § 8 has about 2 log ( 2 e d ˉ ) 2\log(2e\bar d) 2 log ( 2 e d ˉ ) Theorem 1.3 extends this, roughly, to average degree d ˉ = 2 o ( log n ) \bar d = 2^{o(\sqrt{\log n})} d ˉ = 2 o ( l o g n ) d ˉ ≈ Δ ≈ n \bar d \approx\Delta\approx n d ˉ ≈ Δ ≈ n Theorem 1.3 is 2 Θ ( n log n / log n ) 2^{\Theta(n\log n/\sqrt{\log n})} 2 Θ ( n l o g n / l o g n ) 2 n 2^n 2 n O ∗ ( 2 n ) O^*(2^n) O ∗ ( 2 n )
(d) “Previous algorithms were exponential” refers to general sparse graphs. Planar, bounded-genus, minor-free and bounded-treewidth graphs already had subexponential or single-exponential-in-treewidth algorithms, and on planar graphs the 2 O ( n ) 2^{O(\sqrt n)} 2 O ( n )
(e) Asymptotic only. The crossover with brute force is astronomically large; nothing here is of practical use.
(f) The extensions are sketched. § 11 is checked numerically on small instances and is not proved at the level of the rest of the paper.
(g) Citations. All citations were checked against the primary sources on 30 Oct 2026. In particular, the 6 p w n O ( 1 ) 6^{\mathrm{pwn}O(1)} 6 pwn O ( 1 ) Table 1 is O ~ ( 6 p w p w O ( 1 ) n 2 ) \widetilde O(6^{\mathrm{pwpw}O(1)}n^2) O ( 6 pwpw O ( 1 ) n 2 ) [10 Table 1] , and its SETH-tightness is [17 Thm. 1.1] ; the other constants in that table are as stated in the cited works.
(h) No systematic novelty search has been done. The credits in the previous subsection are to the works we know; a Grassmann-determinant encoding of connectivity in a bit-bounded model may well exist elsewhere, and we have not searched the literature systematically.
Organisation
§ 2 recalls the results of [A] that we use. § 3 collects facts about Grassmann algebras. § 4 proves the fermionic matrix-tree identity for Hamiltonian cycles. § 5 splits it over blobs and proves the sign rule. § 6 builds the network and bounds its parameters. § 7 proves Theorems 1.1 and 1.2 , § 8 proves Theorem 1.3 with a rank-encoded variant of the network, and § 9 proves Theorem 1.4 . § 10 treats the results that rest only on the top-level theorems. § 11 sketches extensions, § 12 describes the verification status, and § 13 lists open problems.
The network theorem of [A]
We recall the definitions and results of [A] that we use, in the notation of [A] except where a letter clashes with ours. Conventions of [A]: log = log 2 \log= \log_2 log = log 2 [ x = u ] ∈ { 0 , 1 } [x = u] \in\{0,1\} [ x = u ] ∈ { 0 , 1 } [ K ] = { 1 , … , K } [K] = \{1,\ldots,K\} [ K ] = { 1 , … , K }
Definition 2.1 ([A, Definition 1]). A function F : X × X ′ → Z F: X \times X' \to\mathbb{Z} F : X × X ′ → Z factors through c c c if there are f : X × { 0 , 1 } c → Z f: X \times\{0,1\}^c \to\mathbb{Z} f : X × { 0 , 1 } c → Z f ′ : X ′ × { 0 , 1 } c → Z f': X' \times\{0,1\}^c \to\mathbb{Z} f ′ : X ′ × { 0 , 1 } c → Z F ( z , z ′ ) = ∑ θ ∈ { 0 , 1 } c f ( z , θ ) f ′ ( z ′ , θ ) F(z,z') = \sum_{\theta\in\{0,1\}^c} f(z,\theta)f'(z',\theta) F ( z , z ′ ) = ∑ θ ∈ { 0 , 1 } c f ( z , θ ) f ′ ( z ′ , θ ) h : X → { 0 , 1 } c h: X \to\{0,1\}^c h : X → { 0 , 1 } c h ′ : X ′ → { 0 , 1 } c h': X' \to\{0,1\}^c h ′ : X ′ → { 0 , 1 } c [ h ( z ) = h ′ ( z ′ ) ] = ∑ θ [ h ( z ) = θ ] [ h ′ ( z ′ ) = θ ] [h(z) = h'(z')] = \sum_{\theta}[h(z) = \theta][h'(z') = \theta] [ h ( z ) = h ′ ( z ′ )] = ∑ θ [ h ( z ) = θ ] [ h ′ ( z ′ ) = θ ] c c c
Definition 2.2 ([A, Definition 2]). Let P , B , τ ≥ 1 P, B, \tau\ge1 P , B , τ ≥ 1 network on J J J parameters P , B , τ P, B, \tau P , B , τ J J J a a a S a S_a S a W a : S a → Z W_a: S_a \to\mathbb{Z} W a : S a → Z { a , b } \{a,b\} { a , b } Ψ a , b : S a × S b → Z \Psi_{a,b}: S_a \times S_b \to\mathbb{Z} Ψ a , b : S a × S b → Z Ψ a , b ( z b , z a ) = Ψ a , b ( z a , z b ) \Psi_{a,b}(z_b,z_a) = \Psi_{a,b}(z_a,z_b) Ψ a , b ( z b , z a ) = Ψ a , b ( z a , z b ) c a , b = c b , a ≥ 0 c_{a,b} = c_{b,a} \ge0 c a , b = c b , a ≥ 0 ( f a , b , f b , a ) (f_{a,b},f_{b,a}) ( f a , b , f b , a ) Ψ a , b \Psi_{a,b} Ψ a , b c a , b c_{a,b} c a , b a a a P a ≤ P P_a \le P P a ≤ P
(i) ∑ b ≠ a c a , b ≤ P \sum_{b \ne a} c_{a,b} \le P ∑ b = a c a , b ≤ P a ∈ J a \in J a ∈ J
(ii) all values of all W a W_a W a Ψ a , b \Psi_{a,b} Ψ a , b f a , b f_{a,b} f a , b 2 B 2^B 2 B
(iii) an algorithm receives P P P B B B P a P_a P a c a , b c_{a,b} c a , b S a S_a S a W a W_a W a Ψ a , b \Psi_{a,b} Ψ a , b f a , b f_{a,b} f a , b τ \tau τ
The value of the network is Z = ∑ z ∈ ∏ a S a ∏ a ∈ J W a ( z a ) ∏ { a , b } Ψ a , b ( z a , z b ) Z = \sum_{z \in\prod_a S_a} \prod_{a \in J} W_a(z_a) \prod_{\{a,b\}} \Psi_{a,b}(z_a,z_b) Z = ∑ z ∈ ∏ a S a ∏ a ∈ J W a ( z a ) ∏ { a , b } Ψ a , b ( z a , z b ) total is U = ∑ ( a , b ) : a ≠ b c a , b U = \sum_{(a,b):\,a \ne b} c_{a,b} U = ∑ ( a , b ) : a = b c a , b U ≤ ∣ J ∣ P U \le|J|P U ≤ ∣ J ∣ P
Definition 2.3 ([A, Definition 3]). Let K ≥ 2 K \ge2 K ≥ 2 λ , B ≥ 1 \lambda, B \ge1 λ , B ≥ 1 ( K , λ ) (K,\lambda) ( K , λ ) W 1 , … , W K W_1,\ldots,W_K W 1 , … , W K w w w ( z w ( w ′ ) ) w ′ ≠ w (z_w(w'))_{w'\ne w} ( z w ( w ′ ) ) w ′ = w λ \lambda λ c w , w ′ = λ c_{w,w'}=\lambda c w , w ′ = λ Ψ w , w ′ = [ z w ( w ′ ) = z w ′ ( w ) ] \Psi_{w,w'}=[z_w(w')=z_{w'}(w)] Ψ w , w ′ = [ z w ( w ′ ) = z w ′ ( w )] W w W_w W w ∣ W w ∣ < 2 B |W_w|<2^B ∣ W w ∣ < 2 B
Imported Lemma 2.4 ([A, Lemma 8, case (i)]). Let K ≥ 2 K \ge2 K ≥ 2 g = 3 K 8 g=3K^8 g = 3 K 8 ζ = 1 / ( 2 K ) \zeta=1/(2K) ζ = 1/ ( 2 K ) [ g ] [g] [ g ] P P P B B B τ \tau τ U U U
L = ⌈ U + g P / K K 2 ⌉ , B ′ = ⌈ 2 g P / K ⌉ + g 2 B . L=\left\lceil\frac{U+gP/K}{K^2}\right\rceil,\qquad B'=\lceil2gP/K\rceil+g^2B. L = ⌈ K 2 U + g P / K ⌉ , B ′ = ⌈ 2 g P / K ⌉ + g 2 B . If an algorithm outputs the value of every ( K , L ) (K,L) ( K , L ) ∣ W w ∣ < 2 B ′ |W_w|<2^{B'} ∣ W w ∣ < 2 B ′ T T T
( K g + T ⋅ 2 2 g P / K ⋅ τ ) ⋅ ( g ( P + B ) ) C 1 (2) \left(K^g+T\cdot2^{2gP/K}\cdot\tau\right)\cdot\left(g(P+B)\right)^{C_1} \tag*{(2)} ( K g + T ⋅ 2 2 g P / K ⋅ τ ) ⋅ ( g ( P + B ) ) C 1 (2) operations, by one procedure, for an absolute constant C 1 C_1 C 1
The bound (2.1) is weaker than the printed form of [A, Lemma 8] by at most a polynomial factor, which is irrelevant below; it is the form proved in the Lean development of {citep}[A]asExplicitCost.groupingExplicit`.
Imported Theorem 2.5 ([A, Theorem A]). Suppose there are pieces with parameters ( ρ , c ) (\rho,c) ( ρ , c ) α ′ = log ( 1 / ρ ) \alpha'=\log(1/\rho) α ′ = log ( 1/ ρ ) x 0 ≥ 18 x_0\ge18 x 0 ≥ 18 2 x 0 ≥ c + 5 2^{x_0}\ge c+5 2 x 0 ≥ c + 5
K 0 = 2 x 0 , ζ ℓ = 2 − ℓ − 5 , g ℓ = 2 3 ℓ + x 0 K ℓ , K ℓ + 1 = g ℓ 2 , e 0 = 1 2 , e ℓ + 1 = ( ρ + 3 ζ ℓ ) e ℓ + 3 K ℓ . K_0=2^{x_0},\qquad\zeta_\ell=2^{-\ell-5},\qquad g_\ell=2^{3\ell+x_0}K_\ell,\qquad K_{\ell+1}=g_\ell^2,\qquad e_0=\frac{1}{2},\qquad e_{\ell+1}=(\rho+3\zeta_\ell)e_\ell+\frac{3}{K_\ell}. K 0 = 2 x 0 , ζ ℓ = 2 − ℓ − 5 , g ℓ = 2 3 ℓ + x 0 K ℓ , K ℓ + 1 = g ℓ 2 , e 0 = 2 1 , e ℓ + 1 = ( ρ + 3 ζ ℓ ) e ℓ + K ℓ 3 . (a) log K ℓ = ( 3 x 0 + 6 ) 2 ℓ − 6 ℓ − 2 x 0 − 6 \log K_\ell=(3x_0+6)2^\ell-6\ell-2x_0-6 log K ℓ = ( 3 x 0 + 6 ) 2 ℓ − 6 ℓ − 2 x 0 − 6 K ℓ < K ℓ + 1 ≤ K ℓ 10 K_\ell<K_{\ell+1}\le K_\ell^{10} K ℓ < K ℓ + 1 ≤ K ℓ 10 1 2 ρ ℓ ≤ e ℓ ≤ 0.85 ρ ℓ \frac{1}{2}\rho^\ell\le e_\ell\le0.85\rho^\ell 2 1 ρ ℓ ≤ e ℓ ≤ 0.85 ρ ℓ ρ ℓ ≤ ( ( 3 x 0 + 6 ) / log K ℓ ) α ′ \rho^\ell\le((3x_0+6)/\log K_\ell)^{\alpha'} ρ ℓ ≤ (( 3 x 0 + 6 ) / log K ℓ ) α ′
(b) One deterministic algorithm, given ℓ ≥ 0 \ell\ge0 ℓ ≥ 0 λ \lambda λ B ≥ 1 B\ge1 B ≥ 1 ∣ W w ∣ < 2 B |W_w|<2^B ∣ W w ∣ < 2 B ( K ℓ , λ ) (K_\ell,\lambda) ( K ℓ , λ )
2 e ℓ K ℓ 2 λ ⋅ ( K ℓ ( λ + B ) ) C 0 K ℓ 2 (3) 2^{e_\ell K_\ell^2\lambda}\cdot\left(K_\ell(\lambda+B)\right)^{C_0K_\ell^2} \tag*{(3)} 2 e ℓ K ℓ 2 λ ⋅ ( K ℓ ( λ + B ) ) C 0 K ℓ 2 (3) operations, with C 0 C_0 C 0 c c c
Imported Theorem 2.6 ([A, Theorem B and Lemma 2]). There are pieces with parameters ( 1 / 2 , c ) (1/\sqrt{2},c) ( 1/ 2 , c ) c c c ( 11 / 12 , c ) (11/12,c) ( 11/12 , c ) c ≥ 8 c\ge8 c ≥ 8
Remark 2.7 (Alternative route for Theorem 1.1 ). [A, Lemma 1] states: if ( K , e ) (K,e) ( K , e ) g = 3 K 8 g=3K^8 g = 3 K 8 [ g ] [g] [ g ] C 1 2 e ( U + g P / K ) + 2 g P / K ( P + B ) C 1 τ C_1 2^{e(U+gP/K)+2gP/K}(P+B)^{C_1}\tau C 1 2 e ( U + g P / K ) + 2 g P / K ( P + B ) C 1 τ C 1 = C 1 ( K , e ) C_1=C_1(K,e) C 1 = C 1 ( K , e ) η > 0 \eta>0 η > 0 K K K ( K , η ) (K,\eta) ( K , η ) ( H A ) (H_{\mathrm A}) ( H A ) Theorem 1.1 .
Remark 2.8. [A]’s Lean development proves Theorem 2.4 and Theorem 2.5 (b) as ExplicitCost.groupingExplicit and ExplicitCost.recursionSolves, and Theorem 2.6 as PiecesCounted.halfPieces. There they are instantiated only for the networks that come from CNFs, and Lean’s machine model differs from the printed one (operations are polynomial-time steps or queries, memory is bounded, and K , g , P , B K,g,P,B K , g , P , B § 6 is done here on paper only; see § 12 .
Grassmann algebra
Let Γ \Gamma Γ generators with a total order ≺ \prec ≺ Λ ( Γ ) \Lambda(\Gamma) Λ ( Γ ) Z \mathbb{Z} Z Z \mathbb{Z} Z { e S : S ⊆ Γ } \{e_S:S\subseteq\Gamma\} { e S : S ⊆ Γ }
e S ⋅ e T = 0 if S ∩ T ≠ ∅ , e S ⋅ e T = ( − 1 ) # { ( s , t ) ∈ S × T : t ≺ s } e S ∪ T otherwise. e_S\cdot e_T=0\quad\text{if }S\cap T\ne\varnothing,\qquad e_S\cdot e_T=(-1)^{\#\{(s,t)\in S\times T:t\prec s\}}e_{S\cup T}\quad\text{otherwise.} e S ⋅ e T = 0 if S ∩ T = ∅ , e S ⋅ e T = ( − 1 ) # {( s , t ) ∈ S × T : t ≺ s } e S ∪ T otherwise. This is the exterior algebra of Z Γ \mathbb{Z}^{\Gamma} Z Γ [11 Ch. III, §7] ; it is associative with unit e ∅ = 1 e_{\varnothing}=1 e ∅ = 1 γ \gamma γ e { γ } e_{\{\gamma\}} e { γ } γ γ ′ = − γ ′ γ \gamma\gamma'=-\gamma'\gamma γ γ ′ = − γ ′ γ γ 2 = 0 \gamma^2=0 γ 2 = 0 e S e_S e S S S S ≺ \prec ≺ ≺ \prec ≺ ≺ \prec ≺ ≺ \prec ≺
Parity. Λ = Λ 0 ⊕ Λ 1 \Lambda=\Lambda^0\oplus\Lambda^1 Λ = Λ 0 ⊕ Λ 1 Λ p \Lambda^p Λ p e S e_S e S ∣ S ∣ ≡ p ( m o d 2 ) |S|\equiv p\pmod2 ∣ S ∣ ≡ p ( mod 2 ) Λ 0 ∪ Λ 1 \Lambda^0\cup\Lambda^1 Λ 0 ∪ Λ 1 homogeneous (so 0 0 0 Λ 0 \Lambda^0 Λ 0
Fact 3.1 (Graded commutativity). For x ∈ Λ p x\in\Lambda^p x ∈ Λ p y ∈ Λ q y\in\Lambda^q y ∈ Λ q x y = ( − 1 ) p q y x xy=(-1)^{pq}yx x y = ( − 1 ) pq y x Λ 0 \Lambda^0 Λ 0
Proof. For disjoint S , T S,T S , T S × T S\times T S × T # { t ≺ s } \#\{t\prec s\} # { t ≺ s } # { s ≺ t } \#\{s\prec t\} # { s ≺ t } e S e T = ( − 1 ) ∣ S ∣ ∣ T ∣ e T e S e_Se_T=(-1)^{|S||T|}e_Te_S e S e T = ( − 1 ) ∣ S ∣∣ T ∣ e T e S
Lemma 3.2 (Koszul sign rule). Let y 1 , … , y M y_1,\ldots,y_M y 1 , … , y M p 1 , … , p M p_1,\ldots,p_M p 1 , … , p M σ \sigma σ [ M ] [M] [ M ]
y σ ( 1 ) y σ ( 2 ) ⋯ y σ ( M ) = ( − 1 ) N ( σ ) y 1 y 2 ⋯ y M , N ( σ ) = ∑ s < t σ − 1 ( s ) > σ − 1 ( t ) p s p t . y_{\sigma(1)}y_{\sigma(2)}\cdots y_{\sigma(M)}=(-1)^{N(\sigma)}y_1y_2\cdots y_M,\qquad N(\sigma)=\sum_{\substack{s<t\\ \sigma^{-1}(s)>\sigma^{-1}(t)}}p_sp_t. y σ ( 1 ) y σ ( 2 ) ⋯ y σ ( M ) = ( − 1 ) N ( σ ) y 1 y 2 ⋯ y M , N ( σ ) = s < t σ − 1 ( s ) > σ − 1 ( t ) ∑ p s p t . the sum running over the pairs whose relative order σ \sigma σ
Proof. Induction on the number of reversed pairs. If σ ≠ id \sigma\ne\operatorname{id} σ = id j , j + 1 j,j+1 j , j + 1 σ ( j ) > σ ( j + 1 ) \sigma(j)>\sigma(j+1) σ ( j ) > σ ( j + 1 ) ( − 1 ) p σ ( j ) p σ ( j + 1 ) (-1)^{p_{\sigma(j)}p_{\sigma(j+1)}} ( − 1 ) p σ ( j ) p σ ( j + 1 ) { σ ( j ) , σ ( j + 1 ) } \{\sigma(j),\sigma(j+1)\} { σ ( j ) , σ ( j + 1 )}
Subalgebras and top coefficients. For Γ ′ ⊆ Γ \Gamma'\subseteq\Gamma Γ ′ ⊆ Γ Λ ( Γ ′ ) ⊆ Λ ( Γ ) \Lambda(\Gamma')\subseteq\Lambda(\Gamma) Λ ( Γ ′ ) ⊆ Λ ( Γ ) e S e_S e S S ⊆ Γ ′ S\subseteq\Gamma' S ⊆ Γ ′ ∣ Γ ′ ∣ |\Gamma'| ∣ Γ ′ ∣ ω = ± e Γ ′ \omega=\pm e_{\Gamma'} ω = ± e Γ ′ x ∈ Λ ( Γ ′ ) x\in\Lambda(\Gamma') x ∈ Λ ( Γ ′ ) [ ω ] ( x ) [\omega](x) [ ω ] ( x ) c c c x − c ω x-c\omega x − c ω e S e_S e S S ⊊ Γ ′ S\subsetneq\Gamma' S ⊊ Γ ′ x x x ω \omega ω
Lemma 3.3 (Block factorisation of the top coefficient). Let Γ = Γ 1 ⊔ ⋯ ⊔ Γ g \Gamma=\Gamma_1\sqcup\cdots\sqcup\Gamma_g Γ = Γ 1 ⊔ ⋯ ⊔ Γ g ∣ Γ a ∣ |\Gamma_a| ∣ Γ a ∣ ω a = ± e Γ a \omega_a=\pm e_{\Gamma_a} ω a = ± e Γ a Ω = ω 1 ω 2 ⋯ ω g \Omega=\omega_1\omega_2\cdots\omega_g Ω = ω 1 ω 2 ⋯ ω g x a ∈ Λ ( Γ a ) x_a\in\Lambda(\Gamma_a) x a ∈ Λ ( Γ a )
[ Ω ] ( x 1 x 2 ⋯ x g ) = ∏ a = 1 g [ ω a ] ( x a ) . [\Omega](x_1x_2\cdots x_g)=\prod_{a=1}^{g}[\omega_a](x_a). [ Ω ] ( x 1 x 2 ⋯ x g ) = a = 1 ∏ g [ ω a ] ( x a ) . Proof. Since Ω = ± e Γ \Omega=\pm e_{\Gamma} Ω = ± e Γ [ Ω ] ( ⋅ ) [\Omega](\mathord{\cdot}) [ Ω ] ( ⋅ ) x a = [ ω a ] ( x a ) ω a + r a x_a=[\omega_a](x_a)\omega_a+r_a x a = [ ω a ] ( x a ) ω a + r a r a r_a r a e S e_S e S S ⊊ Γ a S\subsetneq\Gamma_a S ⊊ Γ a r a r_a r a ∏ a [ ω a ] ( x a ) ⋅ Ω \prod_a[\omega_a](x_a)\cdot\Omega ∏ a [ ω a ] ( x a ) ⋅ Ω e S 1 ⋯ e S g e_{S_1}\cdots e_{S_g} e S 1 ⋯ e S g S b ⊆ Γ b S_b\subseteq\Gamma_b S b ⊆ Γ b b b b S a ⊊ Γ a S_a\subsetneq\Gamma_a S a ⊊ Γ a a a a 0 0 0 ± e ⋃ S b \pm e_{\bigcup S_b} ± e ⋃ S b ⋃ S b ≠ Γ \bigcup S_b\ne\Gamma ⋃ S b = Γ [ Ω ] ( ⋅ ) [\Omega](\mathord{\cdot}) [ Ω ] ( ⋅ )
Spanning trees and Hamiltonian cycles
Fix G = ( V , E ) G=(V,E) G = ( V , E ) n ≥ 3 n\ge3 n ≥ 3 r ∈ V r\in V r ∈ V X ⊆ E X\subseteq E X ⊆ E ( V , X ) (V,X) ( V , X ) κ ( V , X ) \kappa(V,X) κ ( V , X ) ( V , X ) (V,X) ( V , X )
Lemma 4.1. n ⋅ # H C ( G ) = ∑ X κ ( V , X ) n\cdot\#\mathrm{HC}(G)=\sum_X\kappa(V,X) n ⋅ # HC ( G ) = ∑ X κ ( V , X ) X X X G G G
Proof. A 2-factor X X X ( V , X ) (V,X) ( V , X ) V V V ( V , X ) (V,X) ( V , X ) n n n n n n κ ( V , X ) = n \kappa(V,X)=n κ ( V , X ) = n ( V , X ) (V,X) ( V , X ) κ ( V , X ) = 0 \kappa(V,X)=0 κ ( V , X ) = 0
Generators. Let Γ = { ψ ˉ v , ψ v : v ∈ V ∖ { r } } \Gamma= \{\bar{\psi}_v,\psi_v : v \in V \setminus\{r\}\} Γ = { ψ ˉ v , ψ v : v ∈ V ∖ { r }} ψ ˉ r = ψ r : = 0 \bar{\psi}_r = \psi_r := 0 ψ ˉ r = ψ r := 0 ω v : = ψ ˉ v ψ v ∈ Λ 0 \omega_v := \bar{\psi}_v\psi_v \in\Lambda^0 ω v := ψ ˉ v ψ v ∈ Λ 0 S ⊆ V S \subseteq V S ⊆ V e = { i , j } ∈ E e = \{i,j\} \in E e = { i , j } ∈ E
Ω S : = ∏ v ∈ S ∖ { r } ω v , q e : = ( ψ ˉ i − ψ ˉ j ) ( ψ i − ψ j ) ∈ Λ 0 . \Omega_S := \prod_{v \in S \setminus\{r\}} \omega_v,\qquad q_e := (\bar{\psi}_i-\bar{\psi}_j)(\psi_i-\psi_j) \in\Lambda^0. Ω S := v ∈ S ∖ { r } ∏ ω v , q e := ( ψ ˉ i − ψ ˉ j ) ( ψ i − ψ j ) ∈ Λ 0 . The order of the factors of Ω S \Omega_S Ω S Ω S = ± e Γ S \Omega_S = \pm e_{\Gamma_S} Ω S = ± e Γ S Γ S \Gamma_S Γ S S S S q e q_e q e e e e
Lemma 4.2 (Berezin form of Cauchy–Binet). Let N = n − 1 N = n-1 N = n − 1 b 1 , … , b N ∈ Z V ∖ { r } b_1,\ldots,b_N \in\mathbb{Z}^{V \setminus\{r\}} b 1 , … , b N ∈ Z V ∖ { r } θ ˉ ( b ) = ∑ u b ( u ) ψ ˉ u \bar{\theta}(b) = \sum_u b(u)\bar{\psi}_u θ ˉ ( b ) = ∑ u b ( u ) ψ ˉ u θ ( b ) = ∑ u b ( u ) ψ u \theta(b) = \sum_u b(u)\psi_u θ ( b ) = ∑ u b ( u ) ψ u
[ Ω V ] ( θ ˉ ( b 1 ) θ ( b 1 ) θ ˉ ( b 2 ) θ ( b 2 ) ⋯ θ ˉ ( b N ) θ ( b N ) ) = det ( B ) 2 , [\Omega_V]\bigl(\bar{\theta}(b_1)\theta(b_1)\bar{\theta}(b_2)\theta(b_2)\cdots\bar{\theta}(b_N)\theta(b_N)\bigr) = \det(\mathbf{B})^2, [ Ω V ] ( θ ˉ ( b 1 ) θ ( b 1 ) θ ˉ ( b 2 ) θ ( b 2 ) ⋯ θ ˉ ( b N ) θ ( b N ) ) = det ( B ) 2 , where B \mathbf{B} B N × N N \times N N × N b k b_k b k V ∖ { r } V \setminus\{r\} V ∖ { r } det ( B ) 2 \det(\mathbf{B})^2 det ( B ) 2
Proof. Enumerate V ∖ { r } V \setminus\{r\} V ∖ { r } u 1 , … , u N u_1,\ldots,u_N u 1 , … , u N
(1) By Theorem 3.2, moving each θ ˉ ( b k ) \bar{\theta}(b_k) θ ˉ ( b k ) θ ( b 1 ) , … , θ ( b k − 1 ) \theta(b_1),\ldots,\theta(b_{k-1}) θ ( b 1 ) , … , θ ( b k − 1 ) ∏ k θ ˉ ( b k ) θ ( b k ) = ( − 1 ) N ( N − 1 ) / 2 θ ˉ ( b 1 ) ⋯ θ ˉ ( b N ) ⋅ θ ( b 1 ) ⋯ θ ( b N ) \prod_k \bar{\theta}(b_k)\theta(b_k) = (-1)^{N(N-1)/2}\bar{\theta}(b_1)\cdots\bar{\theta}(b_N)\cdot\theta(b_1)\cdots\theta(b_N) ∏ k θ ˉ ( b k ) θ ( b k ) = ( − 1 ) N ( N − 1 ) /2 θ ˉ ( b 1 ) ⋯ θ ˉ ( b N ) ⋅ θ ( b 1 ) ⋯ θ ( b N )
(2) Expanding multilinearly, θ ˉ ( b 1 ) ⋯ θ ˉ ( b N ) = ∑ φ : [ N ] → [ N ] ∏ k b k ( u φ ( k ) ) ψ ˉ u φ ( 1 ) ⋯ ψ ˉ u φ ( N ) \bar{\theta}(b_1)\cdots\bar{\theta}(b_N) = \sum_{\varphi:[N]\to[N]} \prod_k b_k(u_{\varphi(k)})\,\bar{\psi}_{u_{\varphi(1)}}\cdots\bar{\psi}_{u_{\varphi(N)}} θ ˉ ( b 1 ) ⋯ θ ˉ ( b N ) = ∑ φ : [ N ] → [ N ] ∏ k b k ( u φ ( k ) ) ψ ˉ u φ ( 1 ) ⋯ ψ ˉ u φ ( N ) φ \varphi φ ψ ˉ u 2 = 0 \bar{\psi}_u^2 = 0 ψ ˉ u 2 = 0 ψ ˉ u φ ( 1 ) ⋯ ψ ˉ u φ ( N ) = sgn ( φ ) ψ ˉ u 1 ⋯ ψ ˉ u N \bar{\psi}_{u_{\varphi(1)}}\cdots\bar{\psi}_{u_{\varphi(N)}} = \operatorname{sgn}(\varphi)\bar{\psi}_{u_1}\cdots\bar{\psi}_{u_N} ψ ˉ u φ ( 1 ) ⋯ ψ ˉ u φ ( N ) = sgn ( φ ) ψ ˉ u 1 ⋯ ψ ˉ u N
θ ˉ ( b 1 ) ⋯ θ ˉ ( b N ) = det ( B ) ψ ˉ u 1 ⋯ ψ ˉ u N , θ ( b 1 ) ⋯ θ ( b N ) = det ( B ) ψ u 1 ⋯ ψ u N . \bar{\theta}(b_1)\cdots\bar{\theta}(b_N) = \det(\mathbf{B})\bar{\psi}_{u_1}\cdots\bar{\psi}_{u_N},\qquad\theta(b_1)\cdots\theta(b_N) = \det(\mathbf{B})\psi_{u_1}\cdots\psi_{u_N}. θ ˉ ( b 1 ) ⋯ θ ˉ ( b N ) = det ( B ) ψ ˉ u 1 ⋯ ψ ˉ u N , θ ( b 1 ) ⋯ θ ( b N ) = det ( B ) ψ u 1 ⋯ ψ u N . (3) Step (1) applied to the standard vectors gives
ψ ˉ u 1 ⋯ ψ ˉ u N ψ u 1 ⋯ ψ u N = ( − 1 ) N ( N − 1 ) / 2 ω u 1 ⋯ ω u N = ( − 1 ) N ( N − 1 ) / 2 Ω V . \bar{\psi}_{u_1}\cdots\bar{\psi}_{u_N}\psi_{u_1}\cdots\psi_{u_N} = (-1)^{N(N-1)/2}\omega_{u_1}\cdots\omega_{u_N} = (-1)^{N(N-1)/2}\Omega_V. ψ ˉ u 1 ⋯ ψ ˉ u N ψ u 1 ⋯ ψ u N = ( − 1 ) N ( N − 1 ) /2 ω u 1 ⋯ ω u N = ( − 1 ) N ( N − 1 ) /2 Ω V . The two signs cancel and the product equals det ( B ) 2 Ω V \det(\mathbf{B})^2\Omega_V det ( B ) 2 Ω V
Lemma 4.3 (Fermionic matrix-tree theorem [14 ] ). For every X ⊆ E X \subseteq E X ⊆ E
[ Ω V ] ( ∏ e ∈ X ( 1 + q e ) ) = κ ( V , X ) . [\Omega_V]\left(\prod_{e \in X}(1+q_e)\right) = \kappa(V,X). [ Ω V ] ( e ∈ X ∏ ( 1 + q e ) ) = κ ( V , X ) . Proof. The factors are even and commute, so ∏ e ∈ X ( 1 + q e ) = ∑ F ⊆ X ∏ e ∈ F q e \prod_{e \in X}(1+q_e) = \sum_{F \subseteq X}\prod_{e \in F}q_e ∏ e ∈ X ( 1 + q e ) = ∑ F ⊆ X ∏ e ∈ F q e F F F e S e_S e S ∣ S ∣ = 2 ∣ F ∣ |S| = 2|F| ∣ S ∣ = 2∣ F ∣ Ω V = ± e Γ \Omega_V = \pm e_\Gamma Ω V = ± e Γ ∣ Γ ∣ = 2 N |\Gamma| = 2N ∣Γ∣ = 2 N ∣ F ∣ = N |F| = N ∣ F ∣ = N e = { i , j } e = \{i,j\} e = { i , j } q e = θ ( b e ) θ ˉ ( b e ) q_e = \theta(b_e)\bar{\theta}(b_e) q e = θ ( b e ) θ ˉ ( b e ) b e = 1 i − 1 j b_e = \mathbf{1}_i-\mathbf{1}_j b e = 1 i − 1 j V ∖ { r } V \setminus\{r\} V ∖ { r } b e = 1 i b_e = \mathbf{1}_i b e = 1 i j = r j=r j = r F F F det ( B F ) 2 \det(\mathbf{B}_F)^2 det ( B F ) 2 B F \mathbf{B}_F B F F F F
If F F F ∣ F ∣ = n − 1 |F| = n-1 ∣ F ∣ = n − 1 ( V , F ) (V,F) ( V , F ) n n n n − 1 n-1 n − 1 C C C r ∉ C r \notin C r ∈ / C u ∈ C u \in C u ∈ C B F \mathbf{B}_F B F 0 0 0 C C C + 1 +1 + 1 − 1 -1 − 1 C C C det B F = 0 \det\mathbf{B}_F = 0 det B F = 0
If F F F det B F = ± 1 \det\mathbf{B}_F = \pm1 det B F = ± 1 n n n n = 1 n=1 n = 1 n ≥ 2 n \geq2 n ≥ 2 v ≠ r v \ne r v = r v v v ± 1 \pm1 ± 1 f f f det B F = ± det B F − f \det\mathbf{B}_F = \pm\det\mathbf{B}_{F-f} det B F = ± det B F − f F − f F-f F − f V − v V-v V − v
Hence the coefficient is the number of spanning trees F ⊆ X F \subseteq X F ⊆ X κ ( V , X ) \kappa(V,X) κ ( V , X )
By Cauchy–Binet, Theorem 4.3 is equivalent to Kirchhoff’s theorem κ ( V , X ) = det L X ( r ) \kappa(V,X) = \det L_X^{(r)} κ ( V , X ) = det L X ( r ) § 12 ).
Corollary 4.4.
n ⋅ # H C ( G ) = ∑ x ∈ { 0 , 1 } E ∏ v ∈ V [ deg x ( v ) = 2 ] ⋅ [ Ω V ] ( ∏ e : x e = 1 ( 1 + q e ) ) . n \cdot\#\mathrm{HC}(G)=\sum_{x\in\{0,1\}^{E}}\prod_{v\in V}[\deg_x(v)=2]\cdot[\Omega_V]\left(\prod_{e:x_e=1}(1+q_e)\right). n ⋅ # HC ( G ) = x ∈ { 0 , 1 } E ∑ v ∈ V ∏ [ deg x ( v ) = 2 ] ⋅ [ Ω V ] ( e : x e = 1 ∏ ( 1 + q e ) ) . Proof. Combine Theorems 4.1 and 4.3.
Blobs, pieces and the sign rule
Conventions
The following conventions are fixed once and for all.
Partition. ϕ : V → [ g ] \phi:V\to[g] ϕ : V → [ g ] blobs are V a = ϕ − 1 ( a ) V_a=\phi^{-1}(a) V a = ϕ − 1 ( a ) r r r 1 < 2 < ⋯ < g 1<2<\cdots<g 1 < 2 < ⋯ < g
Edges. An edge is internal to a a a V a V_a V a E i n t ( a ) E_{\mathrm{int}}(a) E int ( a ) crossing ; let m × m_\times m ×
Crossing order. The crossing edges are listed in an arbitrary but fixed total order e 1 , … , e m × e_1,\ldots,e_{m_\times} e 1 , … , e m × k < l k<l k < l e k e_k e k e l e_l e l
Ends. A crossing edge e k e_k e k low end s k s_k s k high end t k t_k t k a k : = ϕ ( s k ) < b k : = ϕ ( t k ) a_k:=\phi(s_k)<b_k:=\phi(t_k) a k := ϕ ( s k ) < b k := ϕ ( t k ) chord is { a k , b k } \{a_k,b_k\} { a k , b k }
Incidences. ∂ ( a ) : = { k : a ∈ { a k , b k } } \partial(a):=\{k:a\in\{a_k,b_k\}\} ∂ ( a ) := { k : a ∈ { a k , b k }} a a a a < b a<b a < b E ( a , b ) : = { k : ( a k , b k ) = ( a , b ) } E(a,b):=\{k:(a_k,b_k)=(a,b)\} E ( a , b ) := { k : ( a k , b k ) = ( a , b )} bundle of { a , b } \{a,b\} { a , b } m a b : = ∣ E ( a , b ) ∣ m_{ab}:=|E(a,b)| m ab := ∣ E ( a , b ) ∣ m b a : = m a b m_{ba}:=m_{ab} m ba := m ab
Algebras. Γ a \Gamma_a Γ a V a ∖ { r } V_a\setminus\{r\} V a ∖ { r } Λ a : = Λ ( Γ a ) \Lambda_a:=\Lambda(\Gamma_a) Λ a := Λ ( Γ a ) ω a : = Ω V a \omega_a:=\Omega_{V_a} ω a := Ω V a Ω V = ω 1 ⋯ ω g \Omega_V=\omega_1\cdots\omega_g Ω V = ω 1 ⋯ ω g Γ = ⨆ a Γ a \Gamma=\bigsqcup_a\Gamma_a Γ = ⨆ a Γ a
Labels and pieces
The label set is L = { N , 0 , 1 , 2 , 3 } \mathcal{L}=\{\mathrm{N},0,1,2,3\} L = { N , 0 , 1 , 2 , 3 } parity of a label is π ( ℓ ) : = [ ℓ ∈ { 2 , 3 } ] \pi(\ell):=[\ell\in\{2,3\}] π ( ℓ ) := [ ℓ ∈ { 2 , 3 }] e k e_k e k s = s k s=s_k s = s k t = t k t=t_k t = t k α ℓ ( k ) ∈ Λ a k \alpha_\ell(k)\in\Lambda_{a_k} α ℓ ( k ) ∈ Λ a k β ℓ ( k ) ∈ Λ b k \beta_\ell(k)\in\Lambda_{b_k} β ℓ ( k ) ∈ Λ b k Table 2 .
Remark 5.1 (Why five labels). For a used edge, 1 + q e = 1 + ψ ˉ s ψ s − ψ ˉ s ψ t − ψ ˉ t ψ s + ψ ˉ t ψ t 1+q_e=1+\bar{\psi}_s\psi_s-\bar{\psi}_s\psi_t-\bar{\psi}_t\psi_s+\bar{\psi}_t\psi_t 1 + q e = 1 + ψ ˉ s ψ s − ψ ˉ s ψ t − ψ ˉ t ψ s + ψ ˉ t ψ t 1 1 1 ψ ˉ t ψ t \bar{\psi}_t\psi_t ψ ˉ t ψ t 0 0 0 1 + ψ ˉ t ψ t 1+\bar{\psi}_t\psi_t 1 + ψ ˉ t ψ t log 2 5 \log_2 5 log 2 5 1 1 1
Lemma 5.2.
(a) α ℓ ( k ) \alpha_\ell(k) α ℓ ( k ) β ℓ ( k ) \beta_\ell(k) β ℓ ( k ) π ( ℓ ) \pi(\ell) π ( ℓ ) s = r s=r s = r t = r t=r t = r 0 0 0 1 1 1
(b) α N ( k ) β N ( k ) = 1 \alpha_{\mathrm{N}}(k)\beta_{\mathrm{N}}(k)=1 α N ( k ) β N ( k ) = 1 ∑ ℓ ∈ { 0 , 1 , 2 , 3 } α ℓ ( k ) β ℓ ( k ) = 1 + q e k \sum_{\ell\in\{0,1,2,3\}}\alpha_\ell(k)\beta_\ell(k)=1+q_{e_k} ∑ ℓ ∈ { 0 , 1 , 2 , 3 } α ℓ ( k ) β ℓ ( k ) = 1 + q e k
Proof. (a) Read off Table 2 . (b) By bilinearity q e = ψ ˉ s ψ s − ψ ˉ s ψ t − ψ ˉ t ψ s + ψ ˉ t ψ t q_e=\bar{\psi}_s\psi_s-\bar{\psi}_s\psi_t-\bar{\psi}_t\psi_s+\bar{\psi}_t\psi_t q e = ψ ˉ s ψ s − ψ ˉ s ψ t − ψ ˉ t ψ s + ψ ˉ t ψ t − ψ ˉ t ψ s = ψ s ψ ˉ t -\bar{\psi}_t\psi_s=\psi_s\bar{\psi}_t − ψ ˉ t ψ s = ψ s ψ ˉ t 1 + ψ ˉ t ψ t 1+\bar{\psi}_t\psi_t 1 + ψ ˉ t ψ t ψ ˉ s ψ s \bar{\psi}_s\psi_s ψ ˉ s ψ s − ψ ˉ s ψ t -\bar{\psi}_s\psi_t − ψ ˉ s ψ t ψ s ψ ˉ t \psi_s\bar{\psi}_t ψ s ψ ˉ t 1 + q e 1+q_e 1 + q e
For a labelling η ∈ L m × \eta\in\mathcal{L}^{m_\times} η ∈ L m × p k : = π ( η k ) p_k:=\pi(\eta_k) p k := π ( η k ) piece of k k k a a a γ k , a ( η ) : = α η k ( k ) \gamma_{k,a}(\eta):=\alpha_{\eta_k}(k) γ k , a ( η ) := α η k ( k ) a = a k a=a_k a = a k β η k ( k ) \beta_{\eta_k}(k) β η k ( k ) a = b k a=b_k a = b k a a a
R a ( η ) : = ∏ → k ∈ ∂ ( a ) γ k , a ( η ) ∈ Λ a R_a(\eta):=\overrightarrow{\prod}_{k\in\partial(a)}\gamma_{k,a}(\eta)\in\Lambda_a R a ( η ) := ∏ k ∈ ∂ ( a ) γ k , a ( η ) ∈ Λ a (factors in increasing crossing order k k k
Finally, let
r k l : = # { ( x , y ) ∈ { a k , b k } × { a l , b l } : y < x } , ε ( η ) : = ( − 1 ) ∑ k < l p k p l r k l . r_{kl}:=\#\{(x,y)\in\{a_k,b_k\}\times\{a_l,b_l\}:y<x\},\qquad\varepsilon(\eta):=(-1)^{\sum_{k<l}p_kp_lr_{kl}}. r k l := # {( x , y ) ∈ { a k , b k } × { a l , b l } : y < x } , ε ( η ) := ( − 1 ) ∑ k < l p k p l r k l . Proposition 5.3 (Sign rule). For every partition, every crossing order and every η ∈ L m × \eta\in\mathcal{L}^{m_\times} η ∈ L m ×
∏ k = 1 m × α η k ( k ) β η k ( k ) = ε ( η ) ⋅ R 1 ( η ) R 2 ( η ) ⋅ … R g ( η ) . (4) \prod_{k=1}^{m_\times}\alpha_{\eta_k}(k)\,\beta_{\eta_k}(k)=\varepsilon(\eta)\cdot R_1(\eta)R_2(\eta)\cdot\ldots R_g(\eta). \tag*{(4)} k = 1 ∏ m × α η k ( k ) β η k ( k ) = ε ( η ) ⋅ R 1 ( η ) R 2 ( η ) ⋅ … R g ( η ) . (4) Proof. The left side is the product of the sequence Y = ( α ( 1 ) , β ( 1 ) , α ( 2 ) , β ( 2 ) , … , α ( m × ) , β ( m × ) ) Y=(\alpha(1),\beta(1),\alpha(2),\beta(2),\ldots,\alpha(m_\times),\beta(m_\times)) Y = ( α ( 1 ) , β ( 1 ) , α ( 2 ) , β ( 2 ) , … , α ( m × ) , β ( m × )) α ( k ) \alpha(k) α ( k ) ( a k , k ) (a_k,k) ( a k , k ) β ( k ) \beta(k) β ( k ) ( b k , k ) (b_k,k) ( b k , k ) Y Y Y k k k R 1 ⋯ R g R_1\cdots R_g R 1 ⋯ R g
Two pieces of the same k k k In Y Y Y α ( k ) \alpha(k) α ( k ) a k < b k a_k<b_k a k < b k
A piece x x x k k k y y y l l l k < l k<l k < l In Y Y Y x x x ( blob ( x ) , k ) (\operatorname{blob}(x),k) ( blob ( x ) , k ) ( blob ( y ) , l ) (\operatorname{blob}(y),l) ( blob ( y ) , l ) k < l k<l k < l blob ( y ) < blob ( x ) \operatorname{blob}(y)<\operatorname{blob}(x) blob ( y ) < blob ( x ) p k p l p_kp_l p k p l r k l r_{kl} r k l
So R 1 ⋯ R g = ( − 1 ) ∑ k < l p k p l r k l ∏ k α ( k ) β ( k ) R_1\cdots R_g=(-1)^{\sum_{k<l}p_kp_lr_{kl}}\prod_k\alpha(k)\beta(k) R 1 ⋯ R g = ( − 1 ) ∑ k < l p k p l r k l ∏ k α ( k ) β ( k ) ε ( η ) = ± 1 \varepsilon(\eta)=\pm1 ε ( η ) = ± 1
Factorisation of the sign
Lemma 5.4. If { a k , b k } ∩ { a l , b l } = ∅ \{a_k,b_k\}\cap\{a_l,b_l\}=\varnothing { a k , b k } ∩ { a l , b l } = ∅ r k l ≡ I ( k , l ) ( m o d 2 ) r_{kl}\equiv I(k,l)\pmod2 r k l ≡ I ( k , l ) ( mod 2 )
I ( k , l ) : = [ a k < a l < b k < b l or a l < a k < b l < b k ] I(k,l):=[a_k<a_l<b_k<b_l\text{ or }a_l<a_k<b_l<b_k] I ( k , l ) := [ a k < a l < b k < b l or a l < a k < b l < b k ] indicates that the chords interleave. In particular r k l m o d 2 r_{kl}\bmod2 r k l mod 2
Proof. Put Y = { a l , b l } Y=\{a_l,b_l\} Y = { a l , b l } a k a_k a k b k b_k b k r k l = # { y ∈ Y : y < a k } + # { y ∈ Y : y < b k } = 2 # { y ∈ Y : y < a k } + # { y ∈ Y : a k < y < b k } r_{kl}=\#\{y\in Y:y<a_k\}+\#\{y\in Y:y<b_k\}=2\#\{y\in Y:y<a_k\}+\#\{y\in Y:a_k<y<b_k\} r k l = # { y ∈ Y : y < a k } + # { y ∈ Y : y < b k } = 2# { y ∈ Y : y < a k } + # { y ∈ Y : a k < y < b k } l l l a k a_k a k b k b_k b k
Two crossing edges k < l k<l k < l s ( k , l ) : = min ( { a k , b k } ∩ { a l , b l } ) s(k,l):=\min(\{a_k,b_k\}\cap\{a_l,b_l\}) s ( k , l ) := min ({ a k , b k } ∩ { a l , b l }) k , l ∈ ∂ ( s ( k , l ) ) k,l\in\partial(s(k,l)) k , l ∈ ∂ ( s ( k , l )) local signs and the bundle parities
σ a ( η ) : = ( − 1 ) ∑ k < l : chords meet s ( k , l ) = a p k p l r k l , π a b ( η ) : = ∑ k ∈ E ( a , b ) p k m o d 2 ( a < b ) . \sigma_a(\eta):=(-1)^{\sum_{\substack{k<l:\ \text{chords meet}\\s(k,l)=a}}p_kp_lr_{kl}},\qquad
\pi_{ab}(\eta):=\sum_{k\in E(a,b)}p_k\bmod2\quad(a<b). σ a ( η ) := ( − 1 ) ∑ k < l : chords meet s ( k , l ) = a p k p l r k l , π ab ( η ) := k ∈ E ( a , b ) ∑ p k mod 2 ( a < b ) . Thus σ a \sigma_a σ a η ∣ ∂ ( a ) \eta|_{\partial(a)} η ∣ ∂ ( a ) π a b \pi_{ab} π ab η ∣ E ( a , b ) \eta|_{E(a,b)} η ∣ E ( a , b )
Proposition 5.5 (Sign factorisation).
ε ( η ) = ∏ a = 1 g σ a ( η ) ⋅ ( − 1 ) ∑ a < c < b < d π a b ( η ) π c d ( η ) . \varepsilon(\eta)=\prod_{a=1}^{g}\sigma_a(\eta)\cdot(-1)^{\sum_{a<c<b<d}\pi_{ab}(\eta)\,\pi_{cd}(\eta)}. ε ( η ) = a = 1 ∏ g σ a ( η ) ⋅ ( − 1 ) ∑ a < c < b < d π ab ( η ) π c d ( η ) . Proof. Split ∑ k < l p k p l r k l \sum_{k<l}p_kp_l r_{kl} ∑ k < l p k p l r k l
Meeting chords. Each such pair has exactly one s ( k , l ) s(k,l) s ( k , l ) ∏ a σ a \prod_a \sigma_a ∏ a σ a
Disjoint chords. By Theorem 5.4 these pairs give, modulo 2, ∑ k < l : I ( k , l ) = 1 p k p l \sum_{k<l:\ I(k,l)=1}p_kp_l ∑ k < l : I ( k , l ) = 1 p k p l { k , l } \{k,l\} { k , l } { a , b } \{a,b\} { a , b } a < b a<b a < b { c , d } \{c,d\} { c , d } a < c < b < d a<c<b<d a < c < b < d a < c < b < d a<c<b<d a < c < b < d k ∈ E ( a , b ) k\in E(a,b) k ∈ E ( a , b ) l ∈ E ( c , d ) l\in E(c,d) l ∈ E ( c , d ) ∑ a < c < b < d ( ∑ k ∈ E ( a , b ) p k ) ( ∑ l ∈ E ( c , d ) p l ) = ∑ a < c < b < d π a b π c d \sum_{a<c<b<d}\left(\sum_{k\in E(a,b)}p_k\right)\left(\sum_{l\in E(c,d)}p_l\right)=\sum_{a<c<b<d}\pi_{ab}\pi_{cd} ∑ a < c < b < d ( ∑ k ∈ E ( a , b ) p k ) ( ∑ l ∈ E ( c , d ) p l ) = ∑ a < c < b < d π ab π c d
Parity copies. Let Q a : = { ( c , d ) : a < c < d ≤ g } Q_a:=\{(c,d):a<c<d\le g\} Q a := {( c , d ) : a < c < d ≤ g } ∣ Q a ∣ = ( g − a 2 ) |Q_a|=\binom{g-a}{2} ∣ Q a ∣ = ( 2 g − a ) y ∈ { 0 , 1 } Q a y\in\{0,1\}^{Q_a} y ∈ { 0 , 1 } Q a
χ a ( η , y ) : = ( − 1 ) ∑ ( c , d ) ∈ Q a y c d ∑ b : c < b < d π a b ( η ) , \chi_a(\eta,y):=(-1)^{\sum_{(c,d)\in Q_a}y_{cd}\sum_{b:\ c<b<d}\pi_{ab}(\eta)}, χ a ( η , y ) := ( − 1 ) ∑ ( c , d ) ∈ Q a y c d ∑ b : c < b < d π ab ( η ) , a function of η ∣ ∂ ( a ) \eta|_{\partial(a)} η ∣ ∂ ( a ) y y y
Lemma 5.6. If y c d ( a ) = π c d ( η ) y_{cd}^{(a)}=\pi_{cd}(\eta) y c d ( a ) = π c d ( η ) a a a ( c , d ) ∈ Q a (c,d)\in Q_a ( c , d ) ∈ Q a ∏ a χ a ( η , y ( a ) ) = ( − 1 ) ∑ a < c < b < d π a b π c d \prod_a\chi_a(\eta,y^{(a)})=(-1)^{\sum_{a<c<b<d}\pi_{ab}\pi_{cd}} ∏ a χ a ( η , y ( a ) ) = ( − 1 ) ∑ a < c < b < d π ab π c d
Proof. ∑ a ∑ a < c < d π c d ∑ c < b < d π a b = ∑ a < c < b < d π a b π c d \sum_a\sum_{a<c<d}\pi_{cd}\sum_{c<b<d}\pi_{ab}=\sum_{a<c<b<d}\pi_{ab}\pi_{cd} ∑ a ∑ a < c < d π c d ∑ c < b < d π ab = ∑ a < c < b < d π ab π c d
So every interleaving pair of chords { a , b } \{a,b\} { a , b } { c , d } \{c,d\} { c , d } a < c < b < d a<c<b<d a < c < b < d a a a π a b \pi_{ab} π ab a a a π c d \pi_{cd} π c d c c c { a , c } \{a,c\} { a , c }
Blob factorisation
For v ∈ V a v\in V_a v ∈ V a deg η ( v ) : = # { k ∈ ∂ ( a ) : v ∈ { s k , t k } , η k ≠ N } \deg_\eta(v):=\#\{k\in\partial(a):v\in\{s_k,t_k\},\eta_k\ne\mathsf{N}\} deg η ( v ) := # { k ∈ ∂ ( a ) : v ∈ { s k , t k } , η k = N } blob sums
I a ( η ) : = ∑ x ∈ { 0 , 1 } E i n t ( a ) ∏ v ∈ V a [ deg x ( v ) + deg η ( v ) = 2 ] ⋅ [ ω a ] ( F a ( x ) R a ( η ) ) , I_a(\eta):=\sum_{x\in\{0,1\}^{E_{\mathrm{int}}(a)}}\prod_{v\in V_a}[\deg_x(v)+\deg_\eta(v)=2]\cdot[\omega_a](F_a(x)R_a(\eta)), I a ( η ) := x ∈ { 0 , 1 } E int ( a ) ∑ v ∈ V a ∏ [ deg x ( v ) + deg η ( v ) = 2 ] ⋅ [ ω a ] ( F a ( x ) R a ( η )) , where
F a ( x ) : = ∏ e ∈ E i n t ( a ) : x e = 1 ( 1 + q e ) ∈ Λ a ∩ Λ 0 . F_a(x):=\prod_{e\in E_{\mathrm{int}}(a):\ x_e=1}(1+q_e)\in\Lambda_a\cap\Lambda^0. F a ( x ) := e ∈ E int ( a ) : x e = 1 ∏ ( 1 + q e ) ∈ Λ a ∩ Λ 0 . I a I_a I a η ∣ ∂ ( a ) \eta|_{\partial(a)} η ∣ ∂ ( a ) I a = 1 I_a=1 I a = 1 r r r
Theorem 5.7 (Blob factorisation). For every partition and every crossing order,
n ⋅ # H C ( G ) = ∑ η ∈ L × m ε ( η ) ∏ a = 1 g I a ( η ) = ∑ η ∈ L × m ∏ a = 1 g σ a ( η ) χ a ( η , π ( η ) ) I a ( η ) , n\cdot\#\mathrm{HC}(G)=\sum_{\eta\in\mathcal{L}^{m}_\times}\varepsilon(\eta)\prod_{a=1}^{g}I_a(\eta)=\sum_{\eta\in\mathcal{L}^{m}_\times}\prod_{a=1}^{g}\sigma_a(\eta)\chi_a(\eta,\pi(\eta))I_a(\eta), n ⋅ # HC ( G ) = η ∈ L × m ∑ ε ( η ) a = 1 ∏ g I a ( η ) = η ∈ L × m ∑ a = 1 ∏ g σ a ( η ) χ a ( η , π ( η )) I a ( η ) , where χ a ( η , π ( η ) ) \chi_a(\eta,\pi(\eta)) χ a ( η , π ( η )) χ a ( η , y ( a ) ) \chi_a(\eta,y^{(a)}) χ a ( η , y ( a ) ) y c d ( a ) = π c d ( η ) y_{cd}^{(a)}=\pi_{cd}(\eta) y c d ( a ) = π c d ( η )
Proof. The second equality is Theorem 5.5 together with Theorem 5.6. For the first:
Expanding ∏ a I a \prod_a I_a ∏ a I a x i n t ∈ { 0 , 1 } ⋃ a E i n t ( a ) x_{\mathrm{int}}\in\{0,1\}^{\bigcup_a E_{\mathrm{int}}(a)} x int ∈ { 0 , 1 } ⋃ a E int ( a ) ∏ a [ ω a ] ( F a R a ) \prod_a[\omega_a](F_aR_a) ∏ a [ ω a ] ( F a R a )
By Theorem 3.3, since F a R a ∈ Λ a F_aR_a\in\Lambda_a F a R a ∈ Λ a ∏ a [ ω a ] ( F a R a ) = [ Ω V ] ( ∏ a F a R a ) \prod_a[\omega_a](F_aR_a)=[\Omega_V](\prod_aF_aR_a) ∏ a [ ω a ] ( F a R a ) = [ Ω V ] ( ∏ a F a R a )
The F a F_a F a ∏ a ( F a R a ) = ( ∏ a F a ) ⋅ R 1 ⋯ R g \prod_a(F_aR_a)=(\prod_aF_a)\cdot R_1\cdots R_g ∏ a ( F a R a ) = ( ∏ a F a ) ⋅ R 1 ⋯ R g
By Theorem 5.3, ε ( η ) R 1 ⋯ R g = ∏ k α η k ( k ) β η k ( k ) \varepsilon(\eta)R_1\cdots R_g=\prod_k\alpha_{\eta_k}(k)\beta_{\eta_k}(k) ε ( η ) R 1 ⋯ R g = ∏ k α η k ( k ) β η k ( k )
Fix x i n t x_{\mathrm{int}} x int T : = { k : η k ≠ N } T:=\{k:\eta_k\ne\mathsf{N}\} T := { k : η k = N } x : = x i n t ∪ 1 T x:=x_{\mathrm{int}}\cup1_T x := x int ∪ 1 T T T T
By distributivity and Theorem 5.2(b), ∑ η : supp η = T ∏ k α η k ( k ) β η k ( k ) = ∏ k ∈ T ( 1 + q e k ) \sum_{\eta:\ \operatorname{supp}\eta=T}\prod_k\alpha_{\eta_k}(k)\beta_{\eta_k}(k)=\prod_{k\in T}(1+q_{e_k}) ∑ η : supp η = T ∏ k α η k ( k ) β η k ( k ) = ∏ k ∈ T ( 1 + q e k )
Hence ∑ η ∏ a I a = ∑ x ∈ { 0 , 1 } E [ x is a 2-factor ] [ Ω V ] ( ∏ x e = 1 ( 1 + q e ) ) = n ⋅ # H C ( G ) \sum_\eta\prod_a I_a=\sum_{x\in\{0,1\}^{E}}[x\text{ is a 2-factor}][\Omega_V]\left(\prod_{x_e=1}(1+q_e)\right)=n\cdot\#\mathrm{HC}(G) ∑ η ∏ a I a = ∑ x ∈ { 0 , 1 } E [ x is a 2-factor ] [ Ω V ] ( ∏ x e = 1 ( 1 + q e ) ) = n ⋅ # HC ( G )
:::
Table 4. Numerical checks (exact integers). Counts are for one run with 60 instances.
The network
Fix G G G r r r ϕ \phi ϕ § 5 . Let enc : L → { 0 , … , 4 } \operatorname{enc}\colon\mathcal{L} \to\{0,\ldots,4\} enc : L → { 0 , … , 4 } enc ( N ) = 0 \operatorname{enc}(\mathsf{N})=0 enc ( N ) = 0 enc ( j ) = j + 1 \operatorname{enc}(j)=j+1 enc ( j ) = j + 1 t ≥ 0 t\ge0 t ≥ 0 w ( t ) : = min { w ≥ 0 : 2 w ≥ 5 t } = ⌈ t log 5 ⌉ w(t):=\min\{w\ge0:2^w\ge5^t\}=\lceil t\log5\rceil w ( t ) := min { w ≥ 0 : 2 w ≥ 5 t } = ⌈ t log 5 ⌉ w a b : = w ( m a b ) w_{ab}:=w(m_{ab}) w ab := w ( m ab )
Definition 6.1 (The network N ( G , r , ϕ , order ) \mathcal{N}(G,r,\phi,\operatorname{order}) N ( G , r , ϕ , order ) [ g ] [g] [ g ]
Settings.: A setting of node a a a z a = ( η ( a ) , y ( a ) ) z_a=(\eta^{(a)},y^{(a)}) z a = ( η ( a ) , y ( a ) ) η ( a ) ∈ L ∂ ( a ) \eta^{(a)}\in\mathcal{L}^{\partial(a)} η ( a ) ∈ L ∂ ( a ) y ( a ) ∈ { 0 , 1 } Q a y^{(a)}\in\{0,1\}^{Q_a} y ( a ) ∈ { 0 , 1 } Q a
for each b ∈ [ g ] ∖ { a } b\in[g]\setminus\{a\} b ∈ [ g ] ∖ { a } block block b ( z a ) \operatorname{block}_b(z_a) block b ( z a ) w a b w_{ab} w ab ∑ j = 1 m a b enc ( η k j ( a ) ) 5 j − 1 \sum_{j=1}^{m_{ab}}\operatorname{enc}(\eta^{(a)}_{k_j})5^{j-1} ∑ j = 1 m ab enc ( η k j ( a ) ) 5 j − 1 k 1 < ⋯ < k m a b k_1<\cdots<k_{m_{ab}} k 1 < ⋯ < k m ab E ( min ( a , b ) , max ( a , b ) ) E(\min(a,b),\max(a,b)) E ( min ( a , b ) , max ( a , b ))
the bits y c d ( a ) y^{(a)}_{cd} y c d ( a ) ( c , d ) ∈ Q a (c,d)\in Q_a ( c , d ) ∈ Q a
Thus P a : = ∑ b ≠ a w a b + ∣ Q a ∣ P_a:=\sum_{b\ne a}w_{ab}+|Q_a| P a := ∑ b = a w ab + ∣ Q a ∣ S a S_a S a P a P_a P a < 5 m a b <5^{m_{ab}} < 5 m ab ∣ S a ∣ = 5 ∣ ∂ ( a ) ∣ 2 ∣ Q a ∣ |S_a|=5^{|\partial(a)|}2^{|Q_a|} ∣ S a ∣ = 5 ∣ ∂ ( a ) ∣ 2 ∣ Q a ∣
Node functions.: W a ( z a ) : = σ a ( η ( a ) ) ⋅ χ a ( η ( a ) , y ( a ) ) ⋅ I a ( η ( a ) ) W_a(z_a):=\sigma_a(\eta^{(a)})\cdot\chi_a(\eta^{(a)},y^{(a)})\cdot I_a(\eta^{(a)}) W a ( z a ) := σ a ( η ( a ) ) ⋅ χ a ( η ( a ) , y ( a ) ) ⋅ I a ( η ( a ) )
Edges.: For a < b a<b a < b
Ψ a , b ( z a , z b ) : = ∏ k ∈ E ( a , b ) [ η k ( a ) = η k ( b ) ] ⋅ ∏ d = b + 1 g [ y b d ( a ) = π b d ( η ( b ) ) ] . \Psi_{a,b}(z_a,z_b):=\prod_{k\in E(a,b)}[\eta^{(a)}_k=\eta^{(b)}_k]\cdot\prod_{d=b+1}^{g}[y^{(a)}_{bd}=\pi_{bd}(\eta^{(b)})]. Ψ a , b ( z a , z b ) := k ∈ E ( a , b ) ∏ [ η k ( a ) = η k ( b ) ] ⋅ d = b + 1 ∏ g [ y b d ( a ) = π b d ( η ( b ) )] . and Ψ b , a ( z b , z a ) : = Ψ a , b ( z a , z b ) \Psi_{b,a}(z_b,z_a):=\Psi_{a,b}(z_a,z_b) Ψ b , a ( z b , z a ) := Ψ a , b ( z a , z b ) c a , b = c b , a : = w a b + ( g − b ) c_{a,b}=c_{b,a}:=w_{ab}+(g-b) c a , b = c b , a := w ab + ( g − b ) f a , b ( z a , θ ) : = [ h a b ( z a ) = θ ] f_{a,b}(z_a,\theta):=[h_{ab}(z_a)=\theta] f a , b ( z a , θ ) := [ h ab ( z a ) = θ ] f b , a ( z b , θ ) : = [ h b a ( z b ) = θ ] f_{b,a}(z_b,\theta):=[h_{ba}(z_b)=\theta] f b , a ( z b , θ ) := [ h ba ( z b ) = θ ]
h a b ( z a ) : = ( block b ( z a ) , y b , b + 1 ( a ) , … , y b , g ( a ) ) ∈ { 0 , 1 } c a , b , h_{ab}(z_a):=(\operatorname{block}_b(z_a),y^{(a)}_{b,b+1},\ldots,y^{(a)}_{b,g})\in\{0,1\}^{c_{a,b}}, h ab ( z a ) := ( block b ( z a ) , y b , b + 1 ( a ) , … , y b , g ( a ) ) ∈ { 0 , 1 } c a , b , h b a ( z b ) : = ( block a ( z b ) , π b , b + 1 ( η ( b ) ) , … , π b , g ( η ( b ) ) ) ∈ { 0 , 1 } c a , b . h_{ba}(z_b):=(\operatorname{block}_a(z_b),\pi_{b,b+1}(\eta^{(b)}),\ldots,\pi_{b,g}(\eta^{(b)}))\in\{0,1\}^{c_{a,b}}. h ba ( z b ) := ( block a ( z b ) , π b , b + 1 ( η ( b ) ) , … , π b , g ( η ( b ) )) ∈ { 0 , 1 } c a , b . In words: the w a b w_{ab} w ab { a , b } \{a,b\} { a , b } 5 5 5 V a V_a V a V b V_b V b Ψ \Psi Ψ a < b a<b a < b g − b g-b g − b { a , b } \{a,b\} { a , b } a a a π b d \pi_{bd} π b d d > b d>b d > b b b b E ( b , d ) E(b,d) E ( b , d )
Lemma 6.2. ( f a , b , f b , a ) (f_{a,b},f_{b,a}) ( f a , b , f b , a ) Ψ a , b \Psi_{a,b} Ψ a , b c a , b c_{a,b} c a , b
Proof. Both ends list E ( a , b ) E(a,b) E ( a , b ) 5 5 5 block b ( z a ) = block a ( z b ) \operatorname{block}_b(z_a)=\operatorname{block}_a(z_b) block b ( z a ) = block a ( z b ) η ( a ) \eta^{(a)} η ( a ) η ( b ) \eta^{(b)} η ( b ) E ( a , b ) E(a,b) E ( a , b ) h a b h_{ab} h ab h b a h_{ba} h ba Ψ a , b = [ h a b ( z a ) = h b a ( z b ) ] \Psi_{a,b}=[h_{ab}(z_a)=h_{ba}(z_b)] Ψ a , b = [ h ab ( z a ) = h ba ( z b )]
Theorem 6.3. The value of N ( G , r , ϕ , order ) \mathcal{N}(G,r,\phi,\operatorname{order}) N ( G , r , ϕ , order ) n ⋅ # HC ( G ) n\cdot\#\operatorname{HC}(G) n ⋅ # HC ( G ) n ≥ 3 n\ge3 n ≥ 3 ϕ : V → [ g ] \phi:V\to[g] ϕ : V → [ g ] r r r
Proof. The functions Ψ a , b \Psi_{a,b} Ψ a , b 0 / 1 0/1 0/1 ∏ a W a ∏ a < b Ψ a , b \prod_a W_a\prod_{a<b}\Psi_{a,b} ∏ a W a ∏ a < b Ψ a , b Ψ a , b \Psi_{a,b} Ψ a , b 1 1 1 η ∈ L m × \eta\in\mathcal{L}^{m\times} η ∈ L m × η ( a ) = η ∣ ∂ ( a ) \eta^{(a)}=\eta|_{\partial(a)} η ( a ) = η ∣ ∂ ( a ) a a a k k k ∂ ( a k ) \partial(a_k) ∂ ( a k ) ∂ ( b k ) \partial(b_k) ∂ ( b k ) Ψ a k , b k \Psi_{a_k,b_k} Ψ a k , b k k k k y c d ( a ) = π c d ( η ) y^{(a)}_{cd}=\pi_{cd}(\eta) y c d ( a ) = π c d ( η ) a < c < d a<c<d a < c < d Ψ a , c \Psi_{a,c} Ψ a , c π c d ( η c ) = π c d ( η ) \pi_{cd}(\eta^c)=\pi_{cd}(\eta) π c d ( η c ) = π c d ( η ) η ∈ L m × \eta\in\mathcal{L}^{m\times} η ∈ L m × z z z Z = ∑ η ∏ a σ a ( η ) χ a ( η , π ( η ) ) I a ( η ) = n ⋅ # H C ( G ) Z=\sum_\eta\prod_a\sigma_a(\eta)\chi_a(\eta,\pi(\eta))I_a(\eta)=n\cdot\#\mathrm{HC}(G) Z = ∑ η ∏ a σ a ( η ) χ a ( η , π ( η )) I a ( η ) = n ⋅ # HC ( G ) Theorem 5.7 .
Proposition 6.4 (Parameters). Let μ a : = ∑ v ∈ V a deg G ( v ) \mu_a:=\sum_{v\in V_a}\deg_G(v) μ a := ∑ v ∈ V a deg G ( v ) μ : = max a μ a \mu:=\max_a\mu_a μ := max a μ a G G G N ( G , r , ϕ , order ) \mathcal{N}(G,r,\phi,\operatorname{order}) N ( G , r , ϕ , order )
P : = w ( μ ) + g + g 2 , B : = 2 μ + 1 , τ : = 2 1.5 μ n C 2 ( C 2 absolute ) , P:=w(\mu)+g+g^2,\qquad B:=2\mu+1,\qquad\tau:=2^{1.5\mu}n^{C_2}\quad(C_2\text{ absolute}), P := w ( μ ) + g + g 2 , B := 2 μ + 1 , τ := 2 1.5 μ n C 2 ( C 2 absolute ) , U = 2 ∑ a < b w a b + 2 ( g 3 ) ≤ 2 log 5 ⋅ m × + g 2 + g 3 3 ≤ 2 log 5 ⋅ ∣ E ∣ + g 3 , U=2\sum_{a<b}w_{ab}+2\binom{g}{3}\le2\log5\cdot m_\times+g^2+\frac{g^3}{3}\le2\log5\cdot|E|+g^3, U = 2 a < b ∑ w ab + 2 ( 3 g ) ≤ 2 log 5 ⋅ m × + g 2 + 3 g 3 ≤ 2 log 5 ⋅ ∣ E ∣ + g 3 , where τ \tau τ P ≤ log 5 ⋅ μ + 2 g 2 P\le\log5\cdot\mu+2g^2 P ≤ log 5 ⋅ μ + 2 g 2 g P ≤ log 5 ⋅ g μ + 2 g 3 gP\le\log5\cdot g\mu+2g^3 g P ≤ log 5 ⋅ g μ + 2 g 3
Proof. Counting. Each crossing edge at a a a V a V_a V a 2 ∣ E i n t ( a ) ∣ + ∣ ∂ ( a ) ∣ = μ a 2|E_{\mathrm{int}}(a)|+|\partial(a)|=\mu_a 2∣ E int ( a ) ∣ + ∣ ∂ ( a ) ∣ = μ a w ( t ) ≤ t log 5 + [ t > 0 ] w(t)\le t\log5+[t>0] w ( t ) ≤ t log 5 + [ t > 0 ] w ( t ) ≥ t log 5 w(t)\ge t\log5 w ( t ) ≥ t log 5 ∑ b ≠ a w a b ≤ ∣ ∂ ( a ) ∣ log 5 + ( g − 1 ) ≤ w ( μ ) + g − 1 \sum_{b\ne a}w_{ab}\le|\partial(a)|\log5+(g-1)\le w(\mu)+g-1 ∑ b = a w ab ≤ ∣ ∂ ( a ) ∣ log 5 + ( g − 1 ) ≤ w ( μ ) + g − 1
P a ≤ P P_a\le P P a ≤ P P a = ∑ b w a b + ( g − a 2 ) ≤ w ( μ ) + g − 1 + g 2 / 2 ≤ P P_a=\sum_b w_{ab}+\binom{g-a}{2}\le w(\mu)+g-1+g^2/2\le P P a = ∑ b w ab + ( 2 g − a ) ≤ w ( μ ) + g − 1 + g 2 /2 ≤ P
Condition (i). The copy bits on pairs at a a a ∑ b > a ( g − b ) + ∑ b < a ( g − a ) = ( g − a 2 ) + ( a − 1 ) ( g − a ) ≤ g 2 \sum_{b>a}(g-b)+\sum_{b<a}(g-a)=\binom{g-a}{2}+(a-1)(g-a)\le g^2 ∑ b > a ( g − b ) + ∑ b < a ( g − a ) = ( 2 g − a ) + ( a − 1 ) ( g − a ) ≤ g 2 ∑ b ≠ a c a , b ≤ w ( μ ) + g − 1 + g 2 ≤ P \sum_{b\ne a}c_{a,b}\le w(\mu)+g-1+g^2\le P ∑ b = a c a , b ≤ w ( μ ) + g − 1 + g 2 ≤ P
The total. U = 2 ∑ a < b c a , b U=2\sum_{a<b}c_{a,b} U = 2 ∑ a < b c a , b ∑ a < b ( g − b ) = ∑ b ( b − 1 ) ( g − b ) = ( g 3 ) \sum_{a<b}(g-b)=\sum_b(b-1)(g-b)=\binom{g}{3} ∑ a < b ( g − b ) = ∑ b ( b − 1 ) ( g − b ) = ( 3 g ) # { a < b : m a b > 0 } ≤ g 2 / 2 \#\{a<b:m_{ab}>0\}\le g^2/2 # { a < b : m ab > 0 } ≤ g 2 /2 g 2 + g 3 / 3 ≤ g 3 g^2+g^3/3\le g^3 g 2 + g 3 /3 ≤ g 3 g ≥ 2 g\ge2 g ≥ 2
Condition (ii). Ψ \Psi Ψ f f f { 0 , 1 } \{0,1\} { 0 , 1 } ∣ σ a χ a ∣ = 1 |\sigma_a\chi_a|=1 ∣ σ a χ a ∣ = 1 I a I_a I a F a ( x ) R a ( η ) F_a(x)R_a(\eta) F a ( x ) R a ( η ) ∣ E i n t ( a ) ∣ |E_{\mathrm{int}}(a)| ∣ E int ( a ) ∣ ∣ ∂ ( a ) ∣ |\partial(a)| ∣ ∂ ( a ) ∣ 2 ∣ E i n t ( a ) ∣ 2^{|E_{\mathrm{int}}(a)|} 2 ∣ E int ( a ) ∣ x x x
∣ W a ∣ ≤ 10 ∣ E i n t ( a ) ∣ 2 ∣ ∂ ( a ) ∣ ≤ 2 log 10 2 ∣ E i n t ( a ) ∣ + ∣ ∂ ( a ) ∣ ≤ 2 1.67 μ a < 2 B . |W_a|\le10^{|E_{\mathrm{int}}(a)|}2^{|\partial(a)|}\le2^{\frac{\log10}{2}|E_{\mathrm{int}}(a)|+|\partial(a)|}\le2^{1.67\mu_a}<2^B. ∣ W a ∣ ≤ 1 0 ∣ E int ( a ) ∣ 2 ∣ ∂ ( a ) ∣ ≤ 2 2 l o g 10 ∣ E int ( a ) ∣ + ∣ ∂ ( a ) ∣ ≤ 2 1.67 μ a < 2 B . Condition (iii). The preparation stores the graph, ϕ \phi ϕ E ( a , b ) E(a,b) E ( a , b ) w a b w_{ab} w ab Q a Q_a Q a S a S_a S a h a b h_{ab} h ab Ψ \Psi Ψ f f f poly ( n + g ) \operatorname{poly}(n+g) poly ( n + g ) P P P P ≤ poly ( n ) P\le\operatorname{poly}(n) P ≤ poly ( n ) σ a \sigma_a σ a O ( ∣ ∂ ( a ) ∣ 2 ) O(|\partial(a)|^2) O ( ∣ ∂ ( a ) ∣ 2 ) χ a \chi_a χ a O ( g 3 ) O(g^3) O ( g 3 ) I a I_a I a 2 ∣ E i n t ( a ) ∣ ≤ 2 μ / 2 2^{|E_{\mathrm{int}}(a)|}\le2^{\mu/2} 2 ∣ E int ( a ) ∣ ≤ 2 μ /2 x x x μ \mu μ Λ a \Lambda_a Λ a 2 ∣ Γ a ∣ ≤ 4 ∣ V a ∣ ≤ 2 μ 2^{|\Gamma_a|}\le4^{|V_a|}\le2^\mu 2 ∣ Γ a ∣ ≤ 4 ∣ V a ∣ ≤ 2 μ B = O ( n ) B=O(n) B = O ( n ) ∣ V a ∣ ≤ μ a / 2 |V_a|\le\mu_a/2 ∣ V a ∣ ≤ μ a /2 τ ≤ 2 μ / 2 ⋅ 2 μ ⋅ poly ( n ) \tau\le2^{\mu/2}\cdot2^\mu\cdot\operatorname{poly}(n) τ ≤ 2 μ /2 ⋅ 2 μ ⋅ poly ( n )
Remark 6.5. Theorem 2.2 bounds the largest node , through P P P Θ ( n ) \Theta(n) Θ ( n ) 2 2 g P / K 2^{2gP/K} 2 2 g P / K (2) is not small. § 7 removes high-degree vertices first; the rank-encoded network of § 8 avoids the problem instead. Note also that the interleaving sign costs O ( g 3 ) O(g^3) O ( g 3 ) g 2 g^2 g 2
The algorithm and its running time
Preprocessing
Lemma 7.1 (Degree reduction). Let Θ ≥ 2 \Theta\ge2 Θ ≥ 2 H : = { v : deg ( v ) > Θ } H:=\{v:\deg(v)>\Theta\} H := { v : deg ( v ) > Θ } v = ( v ν ) v ∈ H v=(v_\nu)_{v\in H} v = ( v ν ) v ∈ H ν v \nu_v ν v v v v G ν G_\nu G ν G G G e e e v ∈ H v\in H v ∈ H e ∉ ν v e\notin\nu_v e ∈ / ν v
(a) # H C ( G ) = ∑ ν # H C ( G ν ) \#\mathrm{HC}(G)=\sum_\nu\#\mathrm{HC}(G_\nu) # HC ( G ) = ∑ ν # HC ( G ν )
(b) there are at most ∏ v ∈ H ( deg ( v ) 2 ) ≤ n 2 ∣ H ∣ \prod_{v\in H}\binom{\deg(v)}{2}\le n^{2|H|} ∏ v ∈ H ( 2 d e g ( v ) ) ≤ n 2∣ H ∣ ∣ H ∣ < 2 m / Θ |H|<2m/\Theta ∣ H ∣ < 2 m /Θ
(c) every G ν G_\nu G ν V V V m m m Θ \Theta Θ
Proof. Map a Hamiltonian cycle C C C G G G ν ( C ) : = ( E ( C ) ∩ δ ( v ) ) v ∈ H \nu(C):=(E(C)\cap\delta(v))_{v\in H} ν ( C ) := ( E ( C ) ∩ δ ( v ) ) v ∈ H δ ( v ) \delta(v) δ ( v ) v v v C C C G ν ( C ) G_{\nu(C)} G ν ( C ) C C C v ∈ H v\in H v ∈ H ν v ( C ) \nu_v(C) ν v ( C ) C C C G ν G_\nu G ν v ∈ H v\in H v ∈ H E ( C ) ∩ δ ( v ) E(C)\cap\delta(v) E ( C ) ∩ δ ( v ) δ G ν ( v ) ⊆ ν v \delta_{G_\nu}(v)\subseteq\nu_v δ G ν ( v ) ⊆ ν v ν = ν ( C ) \nu=\nu(C) ν = ν ( C ) ( ν , C ) (\nu,C) ( ν , C ) C C C G ν G_\nu G ν G G G ∑ v deg v = 2 m \sum_v\deg v=2m ∑ v deg v = 2 m H H H
Lemma 7.2 (Degree-balanced partition). List V V V v 1 , … , v n v_1,\ldots,v_n v 1 , … , v n S t : = ∑ s < t deg ( v s ) S_t:=\sum_{s<t}\deg(v_s) S t := ∑ s < t deg ( v s ) ϕ ( v t ) : = min ( g , ⌊ g S t / ( 2 m ) ⌋ + 1 ) \phi(v_t):=\min(g,\lfloor gS_t/(2m)\rfloor+1) ϕ ( v t ) := min ( g , ⌊ g S t / ( 2 m )⌋ + 1 ) μ a ≤ 2 m / g + Δ \mu_a\le2m/g+\Delta μ a ≤ 2 m / g + Δ Δ \Delta Δ
Proof. ϕ \phi ϕ t t t v t , … , v t ′ v_t,\ldots,v_{t'} v t , … , v t ′ a < g a<g a < g ( a − 1 ) ⋅ 2 m / g ≤ S t ≤ S t ′ < a ⋅ 2 m / g (a-1)\cdot2m/g\le S_t\le S_{t'}<a\cdot2m/g ( a − 1 ) ⋅ 2 m / g ≤ S t ≤ S t ′ < a ⋅ 2 m / g μ a = S t ′ − S t + deg ( v t ′ ) < 2 m / g + Δ \mu_a=S_{t'}-S_t+\deg(v_{t'})<2m/g+\Delta μ a = S t ′ − S t + deg ( v t ′ ) < 2 m / g + Δ a = g a=g a = g μ g = 2 m − S t ≤ 2 m / g \mu_g=2m-S_t\le2m/g μ g = 2 m − S t ≤ 2 m / g
The algorithm
On input G G G
Step 0. If n ≤ 2 n\le2 n ≤ 2
Step 1. Choose a level ℓ \ell ℓ § 7.3 and § 7.4 ). Put K : = K ℓ K:=K_\ell K := K ℓ g : = 3 K 8 g:=3K^8 g := 3 K 8
Step 2. Apply Theorem 7.1 with Θ : = max ( 2 , ⌈ n / g ⌉ ) \Theta:=\max(2,\lceil n/g\rceil) Θ := max ( 2 , ⌈ n / g ⌉) G ν G_\nu G ν G ν G_\nu G ν
Step 3. Take ϕ \phi ϕ Theorem 7.2 , any root r r r N ( G ν , r , ϕ , order ) \mathcal{N}(G_\nu,r,\phi,\text{order}) N ( G ν , r , ϕ , order ) P P P B B B P a P_a P a c a , b c_{a,b} c a , b
Step 4. Run the procedure of Theorem 2.4 on this network, with the algorithm of Theorem 2.5 (b) at level ℓ \ell ℓ ( K , L ) (K,L) ( K , L ) B ′ B' B ′ B B B n n n
Step 5. Output the sum over the branches.
Correctness follows from Theorems 2.4, 2.5 , 6.3 and 7.1.
Checking the imported hypotheses
Theorem 2.4 needs a network on [ g ] [g] [ g ] P P P B B B τ ≥ 1 \tau\ge1 τ ≥ 1 U U U g = 3 K 8 g=3K^8 g = 3 K 8 ( K , L ) (K,L) ( K , L ) ∣ W ∣ < 2 B ′ |W|<2^{B'} ∣ W ∣ < 2 B ′ Theorem 2.5 (b) at level ℓ \ell ℓ λ = L \lambda=L λ = L B = B ′ B=B' B = B ′ T = 2 e ℓ K 2 L ( K ( L + B ′ ) ) C 0 K 2 T=2e_\ell K^2L(K(L+B'))^{C_0K^2} T = 2 e ℓ K 2 L ( K ( L + B ′ ) ) C 0 K 2 λ , B ≥ 1 \lambda,B\ge1 λ , B ≥ 1 P ≥ 1 P\ge1 P ≥ 1 Theorem 2.5 needs pieces, supplied by Theorem 2.6 . Nothing in the clique algorithm depends on the graph, which reaches it only through the tables that Theorem 2.4 builds from the W a W_a W a f a , b f_{a,b} f a , b K g K^g K g 2 g / K 2g/K 2 g / K L L L
Bounds for one branch
Write m : = ∣ E ( G ) ∣ m:=|E(G)| m := ∣ E ( G ) ∣ ∣ E ( G ν ) ∣ ≤ m |E(G_\nu)|\le m ∣ E ( G ν ) ∣ ≤ m G ν G_\nu G ν Theorem 7.2 , Δ ≤ Θ ≤ n / g + 2 \Delta\le\Theta\le n/g+2 Δ ≤ Θ ≤ n / g + 2 μ ≤ ( 2 m + n ) / g + 2 \mu\le(2m+n)/g+2 μ ≤ ( 2 m + n ) / g + 2 log 5 ≤ 2.33 \log5\le2.33 log 5 ≤ 2.33 g ≥ 3 g\ge3 g ≥ 3
g P ≤ 2.33 ( 2 m + n ) + 3 g 3 , U ≤ 4.65 m + g 3 , B ≤ 2 ( 2 m + n ) / g + 5 , log τ ≤ 1.5 ( 2 m + n ) / g + 3 + C 2 log n , L ≤ g P + 1 , B ′ ≤ 2 g P + 1 + g 2 B . (5) \begin{aligned}
gP&\le2.33(2m+n)+3g^3, & U&\le4.65m+g^3, & B&\le2(2m+n)/g+5,\\
\log\tau&\le1.5(2m+n)/g+3+C_2\log n, & L&\le gP+1, & B'&\le2gP+1+g^2B. \tag*{(5)}
\end{aligned} g P log τ ≤ 2.33 ( 2 m + n ) + 3 g 3 , ≤ 1.5 ( 2 m + n ) / g + 3 + C 2 log n , U L ≤ 4.65 m + g 3 , ≤ g P + 1 , B B ′ ≤ 2 ( 2 m + n ) / g + 5 , ≤ 2 g P + 1 + g 2 B . (5) By (2) and (3) , with e : = e ℓ ≤ 1 e:=e_\ell\le1 e := e ℓ ≤ 1 K 2 L ≤ U + g P / K + K 2 K^2L\le U+gP/K+K^2 K 2 L ≤ U + g P / K + K 2 2 X 2^X 2 X
X ≤ 1 + max { g log K , e ( U + g P K + K 2 ) + C 0 K 2 log ( K ( L + B ′ ) ) + 2 g P K + log τ } + C 1 log ( g ( P + B ) ) + O ( log n ) . (6) X\le1+\max\left\{g\log K,\ e\left(U+\frac{gP}{K}+K^2\right)+C_0K^2\log\left(K(L+B')\right)+\frac{2gP}{K}+\log\tau\right\}
+\ C_1\log\left(g(P+B)\right)+O(\log n). \tag*{(6)} X ≤ 1 + max { g log K , e ( U + K g P + K 2 ) + C 0 K 2 log ( K ( L + B ′ ) ) + K 2 g P + log τ } + C 1 log ( g ( P + B ) ) + O ( log n ) . (6) There are at most n 2 ∣ H ∣ ≤ n 4 m g / n n^{2|H|}\le n^{4mg/n} n 2∣ H ∣ ≤ n 4 m g / n ∣ H ∣ < 2 m / Θ ≤ 2 m g / n |H|<2m/\Theta\le2mg/n ∣ H ∣ < 2 m /Θ ≤ 2 m g / n
Proof of Theorem 1.1
Proof of Theorem 1.1. Let D ≥ 1 D \ge1 D ≥ 1 δ ∈ ( 0 , 1 ] \delta\in(0,1] δ ∈ ( 0 , 1 ] m ≤ D n m \le Dn m ≤ D n 2 m + n ≤ 3 D n 2m+n \le3Dn 2 m + n ≤ 3 D n Theorem 2.5 (a), e ℓ → 0 e_\ell\to0 e ℓ → 0 K ℓ → ∞ K_\ell\to\infty K ℓ → ∞ ℓ \ell ℓ ( δ , D ) (\delta,D) ( δ , D ) e : = e ℓ ≤ δ / ( 40 D ) e := e_\ell\le\delta/(40D) e := e ℓ ≤ δ / ( 40 D ) K : = K ℓ ≥ 60 D / δ K := K_\ell\ge60D/\delta K := K ℓ ≥ 60 D / δ g = 3 K 8 g=3K^8 g = 3 K 8 (5) , the terms of (6) satisfy
e U ≤ δ 40 D ( 4.65 D n + g 3 ) ≤ 0.12 δ n + g 3 , eU \le\frac{\delta}{40D}(4.65Dn+g^3) \le0.12\delta n+g^3, e U ≤ 40 D δ ( 4.65 D n + g 3 ) ≤ 0.12 δ n + g 3 , ( e + 2 ) g P / K ≤ 3 ( 2.33 ⋅ 3 D n + 3 g 3 ) / K ≤ 21 D n / K + 9 g 3 ≤ 0.35 δ n + 9 g 3 , (e+2)gP/K \le3(2.33\cdot3Dn+3g^3)/K \le21Dn/K+9g^3 \le0.35\delta n+9g^3, ( e + 2 ) g P / K ≤ 3 ( 2.33 ⋅ 3 D n + 3 g 3 ) / K ≤ 21 D n / K + 9 g 3 ≤ 0.35 δ n + 9 g 3 , log τ ≤ 4.5 D n / g + O ( log n ) ≤ 0.075 δ n + O ( log n ) , \log\tau\le4.5Dn/g+O(\log n) \le0.075\delta n+O(\log n), log τ ≤ 4.5 D n / g + O ( log n ) ≤ 0.075 δ n + O ( log n ) , and the remaining terms are O δ , D ( log n ) O_{\delta,D}(\log n) O δ , D ( log n ) g g g K K K L L L B ′ B' B ′ P P P B B B O δ , D ( n ) O_{\delta,D}(n) O δ , D ( n ) 2 0.55 δ n + O δ , D ( log n ) 2^{0.55\delta n+O_{\delta,D}(\log n)} 2 0.55 δ n + O δ , D ( l o g n ) n 4 D g = n O δ , D ( 1 ) n^{4Dg}=n^{O_{\delta,D}(1)} n 4 D g = n O δ , D ( 1 ) 2 0.55 δ n + O δ , D ( log n ) = O ( 2 δ n ) 2^{0.55\delta n+O_{\delta,D}(\log n)}=O(2^{\delta n}) 2 0.55 δ n + O δ , D ( l o g n ) = O ( 2 δ n )
The alternative route of Theorem 2.7 gives the same bound: with ( K , e ) (K,e) ( K , e ) e ≤ δ / ( 40 D ) e\le\delta/(40D) e ≤ δ / ( 40 D ) K ≥ 60 D / δ K\ge60D/\delta K ≥ 60 D / δ C 1 2 e ( U + g P / K ) + 2 g P / K ( P + B ) C 1 τ C_1 2^{e(U+gP/K)+2gP/K}(P+B)C_1\tau C 1 2 e ( U + g P / K ) + 2 g P / K ( P + B ) C 1 τ
Proof of Theorem 1.2
Proof of Theorem 1.2. Use the pieces of Theorem 2.6 with ρ = 1 / 2 \rho=1/\sqrt{2} ρ = 1/ 2 α ′ = 1 / 2 \alpha'=1/2 α ′ = 1/2 c c c x 0 x_0 x 0 n < n 0 : = K 30 0 n<n_0:=K_{30}^0 n < n 0 := K 30 0 O ( 1 ) O(1) O ( 1 ) n ≤ 2 n\le2 n ≤ 2 m ≥ n m\ge n m ≥ n
For n ≥ n 0 n\ge n_0 n ≥ n 0 ℓ \ell ℓ K ℓ 30 ≤ n K_\ell^{30}\le n K ℓ 30 ≤ n K ℓ K_\ell K ℓ Theorem 2.5 (a). Then K ℓ + 1 > n 1 / 30 K_{\ell+1}>n^{1/30} K ℓ + 1 > n 1/30 K ℓ + 1 ≤ K ℓ 10 K_{\ell+1}\le K_\ell^{10} K ℓ + 1 ≤ K ℓ 10 n 1 / 300 < K : = K ℓ ≤ n 1 / 30 n^{1/300}<K:=K_\ell\le n^{1/30} n 1/300 < K := K ℓ ≤ n 1/30 g = 3 K 8 ∈ [ 3 n 8 / 300 , 3 n 8 / 30 ] g=3K^8\in[3n^{8/300},3n^{8/30}] g = 3 K 8 ∈ [ 3 n 8/300 , 3 n 8/30 ] Theorem 2.5 (a)
e = e ℓ ≤ 0.85 ( 3 x 0 + 6 log K ) 1 / 2 ≤ 0.85 ( 300 ( 3 x 0 + 6 ) ) 1 / 2 log n = : c e log n . e=e_\ell\le0.85\left(\frac{3x_0+6}{\log K}\right)^{1/2}
\le\frac{0.85(300(3x_0+6))^{1/2}}{\sqrt{\log n}}
=:\frac{c_e}{\sqrt{\log n}}. e = e ℓ ≤ 0.85 ( log K 3 x 0 + 6 ) 1/2 ≤ log n 0.85 ( 300 ( 3 x 0 + 6 ) ) 1/2 =: log n c e . With 2 m + n ≤ 3 m 2m+n\le3m 2 m + n ≤ 3 m (6) and the branching satisfy
e U ≤ c e ( 4.65 m + 27 n 0.8 ) / log n , eU\le c_e(4.65m+27n^{0.8})/\sqrt{\log n}, e U ≤ c e ( 4.65 m + 27 n 0.8 ) / log n , ( e + 2 ) g P / K ≤ 3 ( 7 m + 81 n 0.8 ) / n 1 / 300 = O ( m n − 1 / 300 ) , (e+2)gP/K\le3(7m+81n^{0.8})/n^{1/300}=O(mn^{-1/300}), ( e + 2 ) g P / K ≤ 3 ( 7 m + 81 n 0.8 ) / n 1/300 = O ( m n − 1/300 ) , log τ ≤ 4.5 m / g + O ( log n ) = O ( m n − 8 / 300 ) , \log\tau\le4.5m/g+O(\log n)=O(mn^{-8/300}), log τ ≤ 4.5 m / g + O ( log n ) = O ( m n − 8/300 ) , e K 2 + C 0 K 2 log ( K ( L + B ′ ) ) = O ( n 1 / 15 log n ) ( L , B ′ ≤ poly ( n ) , as m ≤ n 2 ) , eK^2+C_0K^2\log(K(L+B'))=O(n^{1/15}\log n)
\qquad(L,B'\le\operatorname{poly}(n),\text{ as }m\le n^2), e K 2 + C 0 K 2 log ( K ( L + B ′ )) = O ( n 1/15 log n ) ( L , B ′ ≤ poly ( n ) , as m ≤ n 2 ) , g log K = O ( n 8 / 30 log n ) , C 1 log ( g ( P + B ) ) = O ( log n ) , g\log K=O(n^{8/30}\log n),\qquad C_1\log(g(P+B))=O(\log n), g log K = O ( n 8/30 log n ) , C 1 log ( g ( P + B )) = O ( log n ) , log ( # branches ) ≤ 4 ( m / n ) g log n = O ( m n 8 / 30 − 1 log n ) . \log(\#\text{branches})\le4(m/n)g\log n=O(mn^{8/30-1}\log n). log ( # branches ) ≤ 4 ( m / n ) g log n = O ( m n 8/30 − 1 log n ) . Every term except the first is O ( m / log n ) O(m/\sqrt{\log n}) O ( m / log n ) m ≥ n m\ge n m ≥ n n 0.8 n^{0.8} n 0.8 n 1 / 15 log n n^{1/15}\log n n 1/15 log n n 8 / 30 log n n^{8/30}\log n n 8/30 log n o ( n / log n ) o(n/\sqrt{\log n}) o ( n / log n ) 2 C ∗ m / log n 2^{C^*m/\sqrt{\log n}} 2 C ∗ m / l o g n C ∗ C^* C ∗
Remark 7.3. We record four comments on these bounds.
(a) The requirement g = 3 K 8 ≤ n 8 / 30 g=3K^8\le n^{8/30} g = 3 K 8 ≤ n 8/30 g 3 g^3 g 3 n O ( D g ) n^{O(Dg)} n O ( D g ) o ( n / log n ) o(n/\sqrt{\log n}) o ( n / log n ) K ≥ n 1 / 300 K\ge n^{1/300} K ≥ n 1/300 e ℓ = O ( 1 / log n ) e_\ell=O(1/\sqrt{\log n}) e ℓ = O ( 1/ log n )
(b) With the pieces of [A, Lemma 2] only (ρ = 11 / 12 \rho=11/12 ρ = 11/12 2 O ( m / ( log n ) 0.125 ) 2^{O(m/(\log n)^{0.125})} 2 O ( m / ( l o g n ) 0.125 )
(c) The leading term is e ℓ U ≈ e ℓ ⋅ 4.64 ∣ E ∣ e_\ell U\approx e_\ell\cdot4.64|E| e ℓ U ≈ e ℓ ⋅ 4.64∣ E ∣ e ℓ e_\ell e ℓ Theorem 2.5 , for example from better pieces, transfers verbatim.
(d) Like the bounds of [A], these are purely asymptotic. Theorem 1.2 beats 2 n 2^n 2 n e ℓ ⋅ 4.64 m < n e_\ell\cdot4.64m<n e ℓ ⋅ 4.64 m < n log n \log n log n m = 2 n m=2n m = 2 n
Counting with logarithmic cost in the degree
This section proves Theorem 1.3 . The proof is formalised in Lean (theorem3, theorem3_maxdeg; files Unrank, PairCode, VertexBalanced, RankNetwork, RankProcs, DegTableProc, RankWordProcs, Theorem3, DPackage). It reuses Theorem 5.7 verbatim and changes only the network of § 6 : the pair { a , b } \{a,b\} { a , b } every crossing edge of E ( a , b ) E(a,b) E ( a , b ) E ( a , b ) E(a,b) E ( a , b ) deg ( v ) \deg(v) deg ( v ) v v v 2 log deg ( v ) 2\log\deg(v) 2 log deg ( v ) log 2 5 \log_2 5 log 2 5 G G G n ≥ 3 n\geq3 n ≥ 3 m ≥ n m\geq n m ≥ n d ˉ ≥ 2 \bar d\geq2 d ˉ ≥ 2 r r r ϕ \phi ϕ § 5 . Put n a : = ∣ V a ∣ n_a:=|V_a| n a := ∣ V a ∣ n ˉ : = max a n a \bar n:=\max_a n_a n ˉ := max a n a λ Δ : = log ( 2 e Δ ) \lambda_\Delta:=\log(2e\Delta) λ Δ := log ( 2 e Δ ) λ d ˉ : = log ( 2 e d ˉ ) \lambda_{\bar d}:=\log(2e\bar d) λ d ˉ := log ( 2 e d ˉ ) log ( 4 e ) > 3.4 \log(4e)>3.4 log ( 4 e ) > 3.4
Profiles and the rank-encoded network
A profile is an integer vector ξ = ( ξ a b ) a < b \xi=(\xi_{ab})_{a<b} ξ = ( ξ ab ) a < b 0 ≤ ξ a b ≤ m a b 0\leq\xi_{ab}\leq m_{ab} 0 ≤ ξ ab ≤ m ab ξ b a : = ξ a b \xi_{ba}:=\xi_{ab} ξ ba := ξ ab ξ a : = ∑ b ≠ a ξ a b \xi_a:=\sum_{b\neq a}\xi_{ab} ξ a := ∑ b = a ξ ab ∣ ξ ∣ : = ∑ a < b ξ a b |\xi|:=\sum_{a<b}\xi_{ab} ∣ ξ ∣ := ∑ a < b ξ ab η ∈ L m × \eta\in\mathcal{L}^{m\times} η ∈ L m × ξ ( η ) a b : = # { k ∈ E ( a , b ) : η k ≠ N } \xi(\eta)_{ab}:=\#\{k\in E(a,b):\eta_k\neq\mathrm{N}\} ξ ( η ) ab := # { k ∈ E ( a , b ) : η k = N } ξ a ≤ 2 n a \xi_a\leq2n_a ξ a ≤ 2 n a a a a 0 ≤ s ≤ t 0\leq s\leq t 0 ≤ s ≤ t { u 1 < ⋯ < u s } ↦ ∑ i = 1 s ( u i i ) \{u_1<\cdots<u_s\}\mapsto\sum_{i=1}^s\binom{u_i}{i} { u 1 < ⋯ < u s } ↦ ∑ i = 1 s ( i u i ) s s s { 0 , … , t − 1 } \{0,\ldots,t-1\} { 0 , … , t − 1 } { 0 , … , ( t s ) − 1 } \{0,\ldots,\binom{t}{s}-1\} { 0 , … , ( s t ) − 1 } t t t cw ( t , s ) : = ⌈ log ( t s ) ⌉ \operatorname{cw}(t,s):=\lceil\log\binom{t}{s}\rceil cw ( t , s ) := ⌈ log ( s t ) ⌉
Definition 8.1 (The network N ξ \mathcal{N}_\xi N ξ [ g ] [g] [ g ] ξ \xi ξ a a a z a = ( η ( a ) , y ( a ) ) z_a=(\eta^{(a)},y^{(a)}) z a = ( η ( a ) , y ( a ) ) η ( a ) ∈ L ∂ ( a ) \eta^{(a)}\in\mathcal{L}^{\partial(a)} η ( a ) ∈ L ∂ ( a ) # { k ∈ E ( a , b ) : η k ( a ) ≠ N } = ξ a b \#\{k\in E(a,b):\eta^{(a)}_k\neq\mathrm{N}\}=\xi_{ab} # { k ∈ E ( a , b ) : η k ( a ) = N } = ξ ab b ≠ a b\neq a b = a y ( a ) ∈ { 0 , 1 } Q a y^{(a)}\in\{0,1\}^{Q_a} y ( a ) ∈ { 0 , 1 } Q a
for each b ≠ a b\neq a b = a block b ( z a ) \operatorname{block}_b(z_a) block b ( z a ) c a b ′ : = cw ( m a b , ξ a b ) + 2 ξ a b c'_{ab}:=\operatorname{cw}(m_{ab},\xi_{ab})+2\xi_{ab} c ab ′ := cw ( m ab , ξ ab ) + 2 ξ ab k 1 < ⋯ < k m a b k_1<\cdots<k_{m_{ab}} k 1 < ⋯ < k m ab { a , b } \{a,b\} { a , b } T a b : = { i : η k i ( a ) ≠ N } T_{ab}:=\{i:\eta^{(a)}_{k_i}\neq\mathrm{N}\} T ab := { i : η k i ( a ) = N } T a b T_{ab} T ab cw ( m a b , ξ a b ) \operatorname{cw}(m_{ab},\xi_{ab}) cw ( m ab , ξ ab ) η k i ( a ) ∈ { 0 , 1 , 2 , 3 } \eta^{(a)}_{k_i}\in\{0,1,2,3\} η k i ( a ) ∈ { 0 , 1 , 2 , 3 } i ∈ T a b i\in T_{ab} i ∈ T ab
the bits y c d ( a ) y^{(a)}_{cd} y c d ( a ) ( c , d ) ∈ Q a (c,d)\in Q_a ( c , d ) ∈ Q a
S a S_a S a P a : = ∑ b ≠ a c a b ′ + ∣ Q a ∣ P_a:=\sum_{b\neq a}c'_{ab}+|Q_a| P a := ∑ b = a c ab ′ + ∣ Q a ∣ < ( m a b ξ a b ) <\binom{m_{ab}}{\xi_{ab}} < ( ξ ab m ab ) W a = σ a χ a I a W_a=\sigma_a\chi_a I_a W a = σ a χ a I a Ψ a , b \Psi_{a,b} Ψ a , b c a , b : = c a b ′ + ( g − max ( a , b ) ) c_{a,b}:=c'_{ab}+(g-\max(a,b)) c a , b := c ab ′ + ( g − max ( a , b )) h a b h_{ab} h ab h b a h_{ba} h ba f a , b f_{a,b} f a , b f b , a f_{b,a} f b , a
Lemma 8.2. The encoding is a bijection from the settings of a a a S a S_a S a block b ( z a ) = block a ( z b ) \operatorname{block}_b(z_a)=\operatorname{block}_a(z_b) block b ( z a ) = block a ( z b ) η ( a ) \eta^{(a)} η ( a ) η ( b ) \eta^{(b)} η ( b ) { a , b } \{a,b\} { a , b } Ψ a , b = [ h a b ( z a ) = h b a ( z b ) ] \Psi_{a,b}=[h_{ab}(z_a)=h_{ba}(z_b)] Ψ a , b = [ h ab ( z a ) = h ba ( z b )] ( f a , b , f b , a ) (f_{a,b},f_{b,a}) ( f a , b , f b , a ) Ψ a , b \Psi_{a,b} Ψ a , b c a , b c_{a,b} c a , b
Proof. Both ends list the bundle in the same order and use the same ξ a b \xi_{ab} ξ ab T a b T_{ab} T ab η ( a ) \eta^{(a)} η ( a ) ξ a b \xi_{ab} ξ ab ( m a b ξ a b ) \binom{m_{ab}}{\xi_{ab}} ( ξ ab m ab ) □ \square □
Theorem 8.3. ∑ ξ a d m i s s i b l e value ( N ξ ) = n ⋅ # H C ( G ) \sum_{\xi\ \mathrm{admissible}}\operatorname{value}(\mathcal{N}_\xi)=n\cdot\#\mathrm{HC}(G) ∑ ξ admissible value ( N ξ ) = n ⋅ # HC ( G ) value ( N ξ ) = 0 \operatorname{value}(\mathcal{N}_\xi)=0 value ( N ξ ) = 0
Proof. As in the proof of Theorem 6.3 , a nonzero term of value ( N ξ ) \operatorname{value}(\mathcal{N}_\xi) value ( N ξ ) η ∈ L m × \eta\in\mathcal{L}^{m\times} η ∈ L m × Theorem 8.1 that η \eta η ξ ( η ) = ξ \xi(\eta)=\xi ξ ( η ) = ξ η \eta η z z z value ( N ξ ) = ∑ η : ξ ( η ) = ξ ∏ a σ a χ a ( η , π ( η ) ) \operatorname{value}(\mathcal{N}_\xi)=\sum_{\eta:\xi(\eta)=\xi}\prod_a\sigma_a\chi_a(\eta,\pi(\eta)) value ( N ξ ) = ∑ η : ξ ( η ) = ξ ∏ a σ a χ a ( η , π ( η )) L m × \mathcal{L}^{m\times} L m × n ⋅ # H C ( G ) n\cdot\#\mathrm{HC}(G) n ⋅ # HC ( G ) Theorem 5.7 . If ξ a > 2 n a \xi_a>2n_a ξ a > 2 n a η \eta η ξ ( η ) = ξ \xi(\eta)=\xi ξ ( η ) = ξ ∑ v ∈ V a deg η ( v ) = ξ a > 2 n a \sum_{v\in V_a}\deg_\eta(v)=\xi_a>2n_a ∑ v ∈ V a deg η ( v ) = ξ a > 2 n a a a a V a V_a V a v ∈ V a v\in V_a v ∈ V a deg η ( v ) ≥ 3 \deg_\eta(v)\geq3 deg η ( v ) ≥ 3 I a ( η ) I_a(\eta) I a ( η ) □ \square □
Proposition 8.4 (Parameters). Let ξ \xi ξ N ξ \mathcal{N}_\xi N ξ
P : = ⌈ 2 n ˉ λ Δ ⌉ + g + g 2 , B : = ⌈ 2 n ˉ λ Δ ⌉ + 1 , τ : = 2 2 n ˉ λ Δ n C 2 ( C 2 absolute ) , P:=\lceil2\bar n\lambda_\Delta\rceil+g+g^2,\qquad B:=\lceil2\bar n\lambda_\Delta\rceil+1,\qquad\tau:=2^{2\bar n\lambda_\Delta}nC_2\quad(C_2\ \text{absolute}), P := ⌈ 2 n ˉ λ Δ ⌉ + g + g 2 , B := ⌈ 2 n ˉ λ Δ ⌉ + 1 , τ := 2 2 n ˉ λ Δ n C 2 ( C 2 absolute ) , τ \tau τ
U = 2 ∑ a < b c a b ′ + 2 ( g 3 ) ≤ 2 n log ( 2 e d ˉ ) + g 3 . U = 2\sum_{a<b}c'_{ab}+2\binom{g}{3}\le2n\log(2e\bar d)+g^3. U = 2 a < b ∑ c ab ′ + 2 ( 3 g ) ≤ 2 n log ( 2 e d ˉ ) + g 3 . P P P B B B ξ \xi ξ
Proof. We use ( N M ) ≤ ( e N / M ) M \binom{N}{M}\le(eN/M)^M ( M N ) ≤ ( e N / M ) M ∏ i ( N i M i ) ≤ ( ∑ N i ∑ M i ) \prod_i\binom{N_i}{M_i}\le\binom{\sum N_i}{\sum M_i} ∏ i ( M i N i ) ≤ ( ∑ M i ∑ N i ) ∑ i [ x i ] ≤ ∑ i x i + # { i : x i > 0 } \sum_i[x_i]\le\sum_i x_i+\#\{i:x_i>0\} ∑ i [ x i ] ≤ ∑ i x i + # { i : x i > 0 } F N ( M ) : = M log ( e N / M ) + 2 M F_N(M):=M\log(eN/M)+2M F N ( M ) := M log ( e N / M ) + 2 M [ 0 , N ] [0,N] [ 0 , N ] log ( N / M ) + 2 \log(N/M)+2 log ( N / M ) + 2
Per node. Let N a : = ∣ ∂ ( a ) ∣ ≤ Δ n a N_a:=|\partial(a)|\le\Delta n_a N a := ∣ ∂ ( a ) ∣ ≤ Δ n a ξ a ≤ min ( 2 n a , N a ) \xi_a\le\min(2n_a,N_a) ξ a ≤ min ( 2 n a , N a ) ∑ b ≠ a c a b ′ ≤ log ( N a ξ a ) + 2 ξ a + g − 1 ≤ F N a ( ξ a ) + g − 1 \sum_{b\ne a}c'_{ab}\le\log\binom{N_a}{\xi_a}+2\xi_a+g-1\le F_{N_a}(\xi_a)+g-1 ∑ b = a c ab ′ ≤ log ( ξ a N a ) + 2 ξ a + g − 1 ≤ F N a ( ξ a ) + g − 1 2 n a ≤ N a 2n_a\le N_a 2 n a ≤ N a F N a ( ξ a ) ≤ F N a ( 2 n a ) ≤ 2 n a log ( e Δ / 2 ) + 4 n a = 2 n a λ Δ F_{N_a}(\xi_a)\le F_{N_a}(2n_a)\le2n_a\log(e\Delta/2)+4n_a=2n_a\lambda_\Delta F N a ( ξ a ) ≤ F N a ( 2 n a ) ≤ 2 n a log ( e Δ/2 ) + 4 n a = 2 n a λ Δ F N a ( ξ a ) ≤ ( log e + 2 ) N a < 2 n a log ( 4 e ) ≤ 2 n a λ Δ F_{N_a}(\xi_a)\le(\log e+2)N_a<2n_a\log(4e)\le2n_a\lambda_\Delta F N a ( ξ a ) ≤ ( log e + 2 ) N a < 2 n a log ( 4 e ) ≤ 2 n a λ Δ P a ≤ P P_a\le P P a ≤ P ∑ b ≠ a c a , b ≤ 2 n a λ Δ + g − 1 + g 2 / 2 ≤ P \sum_{b\ne a}c_{a,b}\le2n_a\lambda_\Delta+g-1+g^2/2\le P ∑ b = a c a , b ≤ 2 n a λ Δ + g − 1 + g 2 /2 ≤ P
Total. U = 2 ∑ a < b c a b ′ + 2 ( g 3 ) U=2\sum_{a<b}c'_{ab}+2\binom{g}{3} U = 2 ∑ a < b c ab ′ + 2 ( 3 g ) ∑ a < b c a b ′ ≤ log ( m × ∣ ξ ∣ ) + 2 ∣ ξ ∣ + ( g 2 ) \sum_{a<b}c'_{ab}\le\log\binom{m_\times}{|\xi|}+2|\xi|+\binom{g}{2} ∑ a < b c ab ′ ≤ log ( ∣ ξ ∣ m × ) + 2∣ ξ ∣ + ( 2 g ) 2 ∣ ξ ∣ = ∑ a ξ a ≤ 2 n 2|\xi|=\sum_a\xi_a\le2n 2∣ ξ ∣ = ∑ a ξ a ≤ 2 n ∣ ξ ∣ ≤ m × ≤ m |\xi|\le m_\times\le m ∣ ξ ∣ ≤ m × ≤ m n ≤ m × n\le m_\times n ≤ m × log ( m × ∣ ξ ∣ ) + 2 ∣ ξ ∣ ≤ F m × ( n ) ≤ n log ( e m / n ) + 2 n \log\binom{m_\times}{|\xi|}+2|\xi|\le F_{m_\times}(n)\le n\log(em/n)+2n log ( ∣ ξ ∣ m × ) + 2∣ ξ ∣ ≤ F m × ( n ) ≤ n log ( e m / n ) + 2 n m × < n m_\times<n m × < n ( log e + 2 ) m × < n log ( 4 e ) ≤ n log ( 4 e m / n ) (\log e+2)m_\times<n\log(4e)\le n\log(4em/n) ( log e + 2 ) m × < n log ( 4 e ) ≤ n log ( 4 e m / n ) m ≥ n m\ge n m ≥ n n log ( 4 e m / n ) = n log ( 2 e d ˉ ) n\log(4em/n)=n\log(2e\bar d) n log ( 4 e m / n ) = n log ( 2 e d ˉ ) U ≤ 2 n log ( 2 e d ˉ ) + g 2 + 2 ( g 3 ) ≤ 2 n log ( 2 e d ˉ ) + g 3 U\le2n\log(2e\bar d)+g^2+2\binom{g}{3}\le2n\log(2e\bar d)+g^3 U ≤ 2 n log ( 2 e d ˉ ) + g 2 + 2 ( 3 g ) ≤ 2 n log ( 2 e d ˉ ) + g 3
Condition (ii). Ψ \Psi Ψ f f f 0 / 1 0/1 0/1 ∣ σ a χ a ∣ = 1 |\sigma_a\chi_a|=1 ∣ σ a χ a ∣ = 1 I a ( η ) I_a(\eta) I a ( η ) x x x deg x ( v ) = 2 − deg η ( v ) \deg_x(v)=2-\deg_\eta(v) deg x ( v ) = 2 − deg η ( v ) v ∈ V a v\in V_a v ∈ V a x ↦ ( x ∩ δ ( v ) ) v ∈ V a x\mapsto(x\cap\delta(v))_{v\in V_a} x ↦ ( x ∩ δ ( v ) ) v ∈ V a ∏ v ∈ V a ( 1 + deg v + ( deg v 2 ) ) ≤ Δ 2 n a \prod_{v\in V_a}(1+\deg v+\binom{\deg v}{2})\le\Delta^{2n_a} ∏ v ∈ V a ( 1 + deg v + ( 2 d e g v ) ) ≤ Δ 2 n a 1 + d + ( d 2 ) ≤ d 2 1+d+\binom d2\le d^2 1 + d + ( 2 d ) ≤ d 2 d ≥ 2 d\ge2 d ≥ 2 ∣ x ∣ ≤ n a |x|\le n_a ∣ x ∣ ≤ n a ℓ 1 \ell^1 ℓ 1 F a ( x ) R a ( η ) F_a(x)R_a(\eta) F a ( x ) R a ( η ) 5 ∣ x ∣ 2 ξ a ≤ 20 n a 5^{|x|}2^{\xi_a}\le20^{n_a} 5 ∣ x ∣ 2 ξ a ≤ 2 0 n a ℓ 1 \ell^1 ℓ 1 0 , ± 1 0,\pm1 0 , ± 1 1 + q e 1+q_e 1 + q e 5 5 5 2 2 2 log ∣ W a ∣ ≤ 2 n a ( log Δ + 2.17 ) < B \log|W_a|\le2n_a(\log\Delta+2.17)<B log ∣ W a ∣ ≤ 2 n a ( log Δ + 2.17 ) < B
Condition (iii). The preparation stores the graph, ϕ \phi ϕ ( m a b ) (m_{ab}) ( m ab ) h a b h_{ab} h ab Ψ \Psi Ψ f f f poly ( n ) \operatorname{poly}(n) poly ( n ) σ a \sigma_a σ a χ a \chi_a χ a I a I_a I a ( x v ) v ∈ V a (x_v)_{v\in V_a} ( x v ) v ∈ V a x v x_v x v 2 − deg η ( v ) 2-\deg_\eta(v) 2 − deg η ( v ) v v v ± ω a \pm\omega_a ± ω a Δ 2 n a ⋅ 20 n a ⋅ poly ( n ) ≤ 2 2 n a λ Δ n C 2 \Delta^{2n_a}\cdot20^{n_a}\cdot\operatorname{poly}(n)\le2^{2n_a\lambda_\Delta}n^{C_2} Δ 2 n a ⋅ 2 0 n a ⋅ poly ( n ) ≤ 2 2 n a λ Δ n C 2 poly ( n ) \operatorname{poly}(n) poly ( n )
There are at most ∏ a < b ( min ( m a b , 2 n ˉ ) + 1 ) ≤ ( 2 n ˉ + 1 ) ( g 2 ) \prod_{a<b}(\min(m_{ab},2\bar n)+1)\le(2\bar n+1)^{\binom{g}{2}} ∏ a < b ( min ( m ab , 2 n ˉ ) + 1 ) ≤ ( 2 n ˉ + 1 ) ( 2 g )
The algorithm and the proof of Theorem 1.3
Step 0. If n ≤ 2 n\le2 n ≤ 2 2 2 2 0 0 0
Step 1. Choose the level ℓ \ell ℓ K : = K ℓ K:=K_\ell K := K ℓ q : = 3 K 8 q:=3K^8 q := 3 K 8 § 7.4 .
Step 2. List V V V v 1 , … , v n v_1,\ldots,v_n v 1 , … , v n ϕ ( v t ) : = [ t q / n ] \phi(v_t):=[tq/n] ϕ ( v t ) := [ tq / n ] n a ≤ ⌈ n / q ⌉ n_a\le\lceil n/q\rceil n a ≤ ⌈ n / q ⌉ n / q n/q n / q Theorem 8.4 .
Step 3. For each admissible profile ξ \xi ξ N ξ \mathcal{N}_\xi N ξ Theorem 2.5 (b) at level ℓ \ell ℓ
Step 4. Output the sum of the results divided by n n n
There is no degree reduction and no degree-balanced partition. Correctness follows from Theorems 2.4, 2.5 and 8.3; the imported hypotheses are checked as in § 7 , with Theorem 8.4 in place of Theorem 6.4, and Theorem 2.4 is applied to each N ξ \mathcal{N}_\xi N ξ U U U ξ \xi ξ
Proof of Theorem 1.3 . For n < n 0 n < n_0 n < n 0 n ≥ n 0 n \ge n_0 n ≥ n 0 § 7.4 , n 1 / 300 < K ≤ n 1 / 30 n^{1/300} < K \le n^{1/30} n 1/300 < K ≤ n 1/30 g ∈ [ 3 n 8 / 300 , 3 n 8 / 30 ] g \in[3n^{8/300},3n^{8/30}] g ∈ [ 3 n 8/300 , 3 n 8/30 ] e : = e ℓ ≤ c e / log n e := e_\ell\le c_e/\sqrt{\log n} e := e ℓ ≤ c e / log n n ˉ ≤ n / g + 1 \bar{n} \le n/g + 1 n ˉ ≤ n / g + 1 λ Δ ≤ log ( 2 e n ) ≤ 2 log n \lambda_\Delta\le\log(2en) \le2\log n λ Δ ≤ log ( 2 e n ) ≤ 2 log n Δ < n \Delta< n Δ < n Theorem 8.4 ,
U ≤ 2 n λ d ˉ + g 3 , g P ≤ 2 ( n + g ) λ Δ + 3 g 3 , log τ ≤ 2 n ˉ λ Δ + C 2 log n , U \le2n\lambda_{\bar{d}}+g^3,\qquad gP \le2(n+g)\lambda_\Delta+3g^3,\qquad\log\tau\le2\bar{n}\lambda_\Delta+C_2\log n, U ≤ 2 n λ d ˉ + g 3 , g P ≤ 2 ( n + g ) λ Δ + 3 g 3 , log τ ≤ 2 n ˉ λ Δ + C 2 log n , and L ≤ U + g P + 1 L \le U+gP+1 L ≤ U + g P + 1 B ′ ≤ 2 g P + 1 + g 2 B B' \le2gP+1+g^2B B ′ ≤ 2 g P + 1 + g 2 B poly ( n ) \operatorname{poly}(n) poly ( n ) 2 X 2^X 2 X X X X (6) , whose terms satisfy
e U ≤ c e ( 2 n λ d ˉ + 27 n 0.8 ) / log n , eU \le c_e\left(2n\lambda_{\bar{d}}+27n^{0.8}\right)/\sqrt{\log n}, e U ≤ c e ( 2 n λ d ˉ + 27 n 0.8 ) / log n , ( e + 2 ) g P / K ≤ 3 ( 4 ( n + g ) log n + 3 g 3 ) / n 1 / 300 = O ( n 1 − 1 / 300 log n ) , (e+2)gP/K \le3(4(n+g)\log n+3g^3)/n^{1/300}=O(n^{1-1/300}\log n), ( e + 2 ) g P / K ≤ 3 ( 4 ( n + g ) log n + 3 g 3 ) / n 1/300 = O ( n 1 − 1/300 log n ) , log τ ≤ 4 ( n / g + 1 ) log n + C 2 log n = O ( n 1 − 8 / 300 log n ) , \log\tau\le4(n/g+1)\log n+C_2\log n=O(n^{1-8/300}\log n), log τ ≤ 4 ( n / g + 1 ) log n + C 2 log n = O ( n 1 − 8/300 log n ) , e K 2 + C 0 K 2 log ( K ( L + B ′ ) ) = O ( n 1 / 15 log n ) , g log K = O ( n 8 / 30 log n ) , eK^2+C_0K^2\log(K(L+B'))=O(n^{1/15}\log n),\qquad g\log K=O(n^{8/30}\log n), e K 2 + C 0 K 2 log ( K ( L + B ′ )) = O ( n 1/15 log n ) , g log K = O ( n 8/30 log n ) , and C 1 log ( g ( P + B ) ) = O ( log n ) C_1\log(g(P+B))=O(\log n) C 1 log ( g ( P + B )) = O ( log n ) ( 2 n / g + 3 ) g 2 / 2 = 2 O ( n 16 / 30 log n ) (2n/g+3)^{g^2/2}=2^{O(n^{16/30}\log n)} ( 2 n / g + 3 ) g 2 /2 = 2 O ( n 16/30 l o g n ) o ( n / log n ) o(n/\sqrt{\log n}) o ( n / log n ) Δ ≤ n \Delta\le n Δ ≤ n λ d ˉ > 3.4 \lambda_{\bar{d}}>3.4 λ d ˉ > 3.4 2 C ♯ n λ d ˉ / log n 2^{C^\sharp n\lambda_{\bar{d}}/\sqrt{\log n}} 2 C ♯ n λ d ˉ / l o g n C ♯ C^\sharp C ♯ d ˉ ≤ Δ \bar{d}\le\Delta d ˉ ≤ Δ
Remark 8.5.
(a) The degree enters in two ways. The total U U U d ˉ \bar{d} d ˉ Δ \Delta Δ ⌈ n / g ⌉ \lceil n/g\rceil ⌈ n / g ⌉ n − 1 n-1 n − 1 O ( ( n / g ) log n ) O((n/g)\log n) O (( n / g ) log n ) 2 g P / K 2gP/K 2 g P / K (2) , which forced the degree reduction of § 7 (Theorem 6.5), is o ( n / log n ) o(n/\sqrt{\log n}) o ( n / log n ) Δ \Delta Δ
(b) The leading term is e ℓ U ≈ 2 e ℓ n log ( 2 e d ˉ ) e_\ell U \approx2e_\ell n\log(2e\bar{d}) e ℓ U ≈ 2 e ℓ n log ( 2 e d ˉ ) e ℓ ⋅ 2 log 2 5 ⋅ m ≈ 2.32 e ℓ d ˉ n e_\ell\cdot2\log_2 5\cdot m\approx2.32e_\ell\bar{d}n e ℓ ⋅ 2 log 2 5 ⋅ m ≈ 2.32 e ℓ d ˉ n Theorem 1.2 ; the new term is the smaller one for d ˉ ≥ 4 \bar{d}\ge4 d ˉ ≥ 4
(c) The self-reductions of Theorem 1.4 delete edges, which does not increase d ˉ \bar{d} d ˉ d ˉ \bar{d} d ˉ Theorem 1.3 times n 2 + 1 n^2+1 n 2 + 1
(d) With a fixed level, as in § 7.3 , the same computation gives O ( 2 δ n ) O(2^{\delta n}) O ( 2 δ n ) Δ 0 \Delta_0 Δ 0 e ≤ δ / ( 8 log ( 2 e Δ 0 ) ) e\le\delta/(8\log(2e\Delta_0)) e ≤ δ / ( 8 log ( 2 e Δ 0 )) K ≥ 24 log ( 2 e Δ 0 ) / δ K\ge24\log(2e\Delta_0)/\delta K ≥ 24 log ( 2 e Δ 0 ) / δ e ≤ δ / ( 40 D ) e\le\delta/(40D) e ≤ δ / ( 40 D ) Theorem 1.1 when D D D g P / K ≈ 2 n λ Δ / K gP/K\approx2n\lambda_\Delta/K g P / K ≈ 2 n λ Δ / K O ( δ n ) O(\delta n) O ( δ n ) Δ \Delta Δ
Decision, search and paths
Proof of Theorem 1.4 . Decision. G G G # HC ( G ) > 0 \#\operatorname{HC}(G)>0 # HC ( G ) > 0 Theorem 1.1 or Theorem 1.2 suffices.
Search, by self-reduction. Let H : = G H:=G H := G e e e G G G # HC ( H − e ) > 0 \#\operatorname{HC}(H-e)>0 # HC ( H − e ) > 0 H : = H − e H:=H-e H := H − e # HC ( H ) > 0 \#\operatorname{HC}(H)>0 # HC ( H ) > 0 C C C H H H H H H C C C f f f H H H C C C f f f H − f H-f H − f C C C f f f H H H C C C n 2 n^2 n 2 n 2 + 1 n^2+1 n 2 + 1 n n n m m m
Hamiltonian paths. Let G + G^+ G + G G G w w w V V V n > 2 n>2 n > 2 G G G G + G^+ G + # HP ( G ) = # HC ( G + ) \#\operatorname{HP}(G)=\#\operatorname{HC}(G^+) # HP ( G ) = # HC ( G + ) G + G^+ G + n + 1 n+1 n + 1 m + n ≤ ( D + 1 ) ( n + 1 ) m+n\le(D+1)(n+1) m + n ≤ ( D + 1 ) ( n + 1 ) w w w n n n Theorem 1.2 handles directly; for the fixed-density form the Lean proof applies Theorem 1.1 to G + G^+ G + D + 1 D+1 D + 1 D D D s s s t t t s s s t t t
Results that rest only on the top-level theorems
This section concerns Theorems 1.6 and 1.7 . Unlike Theorem 1.1 , they use the labs’ #SAT theorems only as black boxes, through CNF encodings.
The Cut&Count identity
Let r ∈ V r \in V r ∈ V cut ( G , r ) \operatorname{cut}(G,r) cut ( G , r ) x e x_e x e e ∈ E e \in E e ∈ E c v c_v c v v ∈ V v \in V v ∈ V v v v x e x_e x e e ∋ v e \ni v e ∋ v u w uw u w x u w → ( c u ↔ c w ) x_{uw} \to(c_u \leftrightarrow c_w) x u w → ( c u ↔ c w ) c r = f a l s e c_r = \mathrm{false} c r = false
Lemma 10.1 (Cut&Count [20 ] ). The number of models of cut ( G , r ) \operatorname{cut}(G,r) cut ( G , r ) ∑ X 2 cc ( X ) − 1 \sum_X 2^{\operatorname{cc}(X)-1} ∑ X 2 cc ( X ) − 1 X X X G G G cc ( X ) \operatorname{cc}(X) cc ( X ) ( V , X ) (V,X) ( V , X ) # H C ( G ) \#\mathrm{HC}(G) # HC ( G )
Proof. A model is a pair ( X , c ) (X,c) ( X , c ) X X X c : V → { 0 , 1 } c \colon V \to\{0,1\} c : V → { 0 , 1 } ( V , X ) (V,X) ( V , X ) c ( r ) = 0 c(r)=0 c ( r ) = 0 2 cc ( X ) − 1 2^{\operatorname{cc}(X)-1} 2 cc ( X ) − 1 c c c X X X
For unbounded degree, the vertex constraint is replaced by a sequential counter (two bits per prefix of the incident edges), giving a 5-CNF on 5 m + 3 n 5m+3n 5 m + 3 n count_cutCNF, count_cutCNF_mod_two, count_bigCNF).
Proof of Theorem 1.6 . Feed the 5-CNF to the respective #SAT algorithm. With [A], the formula has N = 5 m + 3 n N=5m+3n N = 5 m + 3 n 85 m + 11 n + 2 85m+11n+2 85 m + 11 n + 2 2 C ⋅ 5 m ′ / log m ′ 2^{C\cdot5m'/\sqrt{\log m'}} 2 C ⋅ 5 m ′ / l o g m ′ N ≤ m ′ ≤ 85 m + 11 n + 2 N \le m' \le85m+11n+2 N ≤ m ′ ≤ 85 m + 11 n + 2 hamParity_allGraphs_anthropic, whose hypothesis MainResults.MainTheorem is discharged by [A]’s Lean proof (§ 12 ). With [35 ] , the Lean theorem hamParity_allGraphs gives one machine with time C ( L + 1 ) d 2 A ρ ( 5 m + 3 n ) C(L+1)^{d2^{A\rho(5m+3n)}} C ( L + 1 ) d 2 A ρ ( 5 m + 3 n ) L L L exact_count_and_sat is discharged by OpenAI’s Lean proof. The directed version uses one selected out-arc and in-arc per vertex (dirHamParity_subexponential). Building the CNF from G G G
Why colourings do not give exact counts
Cut&Count extracts [ X c o n n e c t e d ] [X\ \mathrm{connected}] [ X connected ]
Proposition 10.2 (machine-checked: colouring\_barrier\_graph). Work over a field of characteristic 0. Suppose that weights z 0 , … , z q − 1 z_0,\ldots,z_{q-1} z 0 , … , z q − 1 q q q C ∌ r C \not\ni r C ∋ r h ( C ) = ∑ j z j ∣ C ∣ h(C)=\sum_j z_j^{\lvert C\rvert} h ( C ) = ∑ j z j ∣ C ∣ # H C ( G ) \#\mathrm{HC}(G) # HC ( G ) G G G n n n q ≥ n − 4 q \ge n-4 q ≥ n − 4
Proof. We have z 0 ≠ 0 z_0 \ne0 z 0 = 0 z 0 = 1 z_0=1 z 0 = 1 k ∈ { 3 , … , n − 3 } k \in\{3,\ldots,n-3\} k ∈ { 3 , … , n − 3 } C n − k − 3 ▹ r C_{n-k-3} \mathbin{\triangleright} r C n − k − 3 ▹ r C k C_k C k ∑ j = 0 q − 1 z j k = 0 \sum_{j=0}^{q-1} z_j^k=0 ∑ j = 0 q − 1 z j k = 0 k = 3 , … , n − 3 k=3,\ldots,n-3 k = 3 , … , n − 3 z j z_j z j λ i \lambda_i λ i q q q n − 5 n-5 n − 5 n − 5 ≥ q n-5 \ge q n − 5 ≥ q λ = 1 \lambda=1 λ = 1
Conversely q = n − 2 q=n-2 q = n − 2 z j = ζ j z_j=\zeta^j z j = ζ j ζ \zeta ζ ( n − 2 ) (n-2) ( n − 2 ) log n \log n log n
Randomized decision
Proof of Theorem 1.7 (a). Add to cut ( G , r ) \operatorname{cut}(G,r) cut ( G , r ) H \mathcal{H} H 2 2 2 # { X ∈ HC ( G ) : H ( 1 X ) } \#\{X \in\operatorname{HC}(G) : \mathcal{H}(\mathbf{1}_X)\} # { X ∈ HC ( G ) : H ( 1 X )} count_cutCNFWith_mod_two); it is even if G G G H \mathcal{H} H H \mathcal{H} H [13 ] . Their isolation lemma [13 Lemma 3] is stated for solution sets of k k k S ⊆ { 0 , 1 } N S \subseteq\{0,1\}^{N} S ⊆ { 0 , 1 } N isolation_count), together with the entropy estimate needed to make the isolating fraction at least exp ( − δ N ) \exp(-\delta N) exp ( − δ N ) δ > 0 \delta> 0 δ > 0 isolation_fraction). With S = HC ( G ) S = \operatorname{HC}(G) S = HC ( G ) N = ∣ E ∣ ≤ Δ n / 2 N = |E| \leq\Delta n/2 N = ∣ E ∣ ≤ Δ n /2 decision_sound), the success fraction (hamDecision_fraction) and one machine for all hashes (hamDecision_subexponential). Repeating t exp ( δ ∣ E ∣ ) t\exp(\delta|E|) t exp ( δ ∣ E ∣ ) e − t e^{-t} e − t
Remark 10.3 (The superseded part (b); not claimed). Let P G ( w ) = ∑ H ∈ HC ( G ) ∏ e ∈ H w e P_G(w) = \sum_{H\in\operatorname{HC}(G)} \prod_{e\in H} w_e P G ( w ) = ∑ H ∈ HC ( G ) ∏ e ∈ H w e 0 / 1 0/1 0/1 F p E \mathbb{F}_p^E F p E G G G [1 ] , a polynomial of degree d d d A 1 × ⋯ × A N A_1 \times\cdots\times A_N A 1 × ⋯ × A N min { ∏ y i : 1 ≤ y i ≤ ∣ A i ∣ , ∑ y i ≥ ∑ ∣ A i ∣ − d } \min\{\prod y_i : 1 \leq y_i \leq|A_i|,\ \sum y_i \geq\sum|A_i| - d\} min { ∏ y i : 1 ≤ y i ≤ ∣ A i ∣ , ∑ y i ≥ ∑ ∣ A i ∣ − d } A i = F p A_i = \mathbb{F}_p A i = F p d = n d = n d = n w w w P G ( w ) ≠ 0 P_G(w) \neq0 P G ( w ) = 0 p − n / ( p − 1 ) − 1 p^{-n/(p-1)-1} p − n / ( p − 1 ) − 1 P G ( w ) m o d p P_G(w) \bmod p P G ( w ) mod p p p p p p p ⌈ log p ⌉ \lceil\log p\rceil ⌈ log p ⌉ 0 0 0 x e → ( c u = c v ) x_e \to(c_u = c_v) x e → ( c u = c v ) z e z_e z e x e = 0 ⇒ z e = 0 x_e = 0 \Rightarrow z_e = 0 x e = 0 ⇒ z e = 0 x e = 1 ⇒ z e < w e x_e = 1 \Rightarrow z_e < w_e x e = 1 ⇒ z e < w e ∑ X p cc ( X ) − 1 ∏ e ∈ X w e ≡ P G ( w ) ( m o d p ) \sum_X p^{\operatorname{cc}(X)-1}\prod_{e\in X} w_e \equiv P_G(w) \pmod p ∑ X p cc ( X ) − 1 ∏ e ∈ X w e ≡ P G ( w ) ( mod p ) O ( ∣ E ∣ log p ) O(|E|\log p) O ( ∣ E ∣ log p ) O ( log p ) O(\log p) O ( log p ) k k k 2 O ( ∣ E ∣ log 2 p / log ∣ E ∣ ) 2^{O(|E|\log^2 p/\sqrt{\log|E|})} 2 O ( ∣ E ∣ l o g 2 p / l o g ∣ E ∣ ) p ≈ log n p \approx\sqrt{\log n} p ≈ log n p n / ( p − 1 ) + 1 ⋅ t p^{n/(p-1)+1}\cdot t p n / ( p − 1 ) + 1 ⋅ t e − t e^{-t} e − t 2 O D ( n ( log log n ) 2 / log n ) 2^{O_D(n(\log\log n)^2/\sqrt{\log n})} 2 O D ( n ( l o g l o g n ) 2 / l o g n )
Extensions (sketched)
This section is not at the level of rigour of the rest of the paper. The identities below were checked exactly by brute force on small instances, and the blob networks were evaluated on random partitions; the algorithmic consequences are sketched, and all of them are conditional on ( H A ) (\mathrm{H}_A) ( H A ) Theorem 1.1 .
The template
All problems below fit one template:
Z = ∑ s , ξ ∏ v C v ( s v , ξ ∣ δ ( v ) ) ⋅ [ Ω ] ( ∏ v M v ( s v ) ∏ e = u v F e ( s u , s v , ξ e ) ) (7) Z = \sum_{s,\xi} \prod_v C_v(s_v,\xi|_{\delta(v)}) \cdot[\Omega]\left(\prod_v M_v(s_v)\prod_{e=uv}F_e(s_u,s_v,\xi_e)\right) \tag*{(7)} Z = s , ξ ∑ v ∏ C v ( s v , ξ ∣ δ ( v ) ) ⋅ [ Ω ] ( v ∏ M v ( s v ) e = uv ∏ F e ( s u , s v , ξ e ) ) (7) where s v s_v s v ξ e \xi_e ξ e δ ( v ) \delta(v) δ ( v ) v v v C v C_v C v M v M_v M v v v v 1 + w ψ ˉ v ψ v 1+w\bar{\psi}_v\psi_v 1 + w ψ ˉ v ψ v ψ ˉ v ψ v \bar{\psi}_v\psi_v ψ ˉ v ψ v v v v F e F_e F e e e e z w e z^{w_e} z w e log 2 ( # labels ) \log_2(\#\text{labels}) log 2 ( # labels ) F e F_e F e § 5 applies unchanged, at a cost of O ( g 3 ) O(g^3) O ( g 3 ) B B B det ( L X 1 + L X 2 ) \det(LX_1+LX_2) det ( L X 1 + L X 2 )
Machine-checked rows. For directed Hamiltonian cycles and for ATSP the statement below is proved in Lean, without the degree hypothesis and also in rate form for #DHC, by splitting every vertex into an in-, a middle and an out-copy and applying Theorems 1.1 , 1.2 and 1.5 to the resulting undirected graph (theoremDHC, theoremDHC_rate, theoremATSP, theoremATSP_decode; standard axioms only). The directed identity of the table is formalised as well (card_dirHamCycles_eq_sum, dblob_factorisation_w). For all other rows the proposition is a sketch and is not claimed.
Proposition 11.1 (Sketch; not claimed except for the machine-checked rows). Assume (HA), and let P \mathcal{P} P Table 3 , on graphs with ∣ E ∣ ≤ D n |E|\le Dn ∣ E ∣ ≤ D n δ > 0 \delta>0 δ > 0 κ \kappa κ 2 δ n 2^{\delta n} 2 δ n
Table 3. Problems fitting the template (7) . All identities were checked exactly on small instances (brute force = determinant identity = blob network on random partitions with 2–4 blobs). “Labels” is the number of labels per crossing edge.
Proof sketch. The identity in the table is an instance of (7) ; the blob network is built as in § 6 , with U ≈ 2 log 2 ( # labels ) ⋅ ∣ E ∣ + O ( g 3 ) U\approx2\log_2(\#\text{labels})\cdot|E|+O(g^3) U ≈ 2 log 2 ( # labels ) ⋅ ∣ E ∣ + O ( g 3 ) P ≈ U / g + g 2 P\approx U/g+g^2 P ≈ U / g + g 2 § 7 applies verbatim. The identities have been checked numerically; the uniform statements of the bit bounds, and the hub-handling, have not been written out in full. □
Remark 11.2 (Hubs). A vertex of degree Θ ( n ) \Theta(n) Θ ( n ) P P P O ( log d ) O(\log d) O ( log d ) forced edges (factor q e q_e q e 1 + q e 1+q_e 1 + q e
The Tutte polynomial on the line y = 1 y=1 y = 1
On the line y = 1 y=1 y = 1 T G ( x , 1 ) = ∑ F ( x − 1 ) r ( E ) − ∣ F ∣ T_G(x,1)=\sum_{F}(x-1)^{r(E)-|F|} T G ( x , 1 ) = ∑ F ( x − 1 ) r ( E ) − ∣ F ∣ F ⊆ E F\subseteq E F ⊆ E r ( E ) = n − cc ( G ) r(E)=n-\operatorname{cc}(G) r ( E ) = n − cc ( G ) T G ( x , 1 ) T_G(x,1) T G ( x , 1 )
Lemma 11.3 (Forest indicator; written proof, not machine-checked, not claimed). Let H H H S S S X X X deg H \deg_H deg H H H H
[ z ∣ S ∣ − ∣ X ∣ ] det ( L H + z diag ( 2 − deg H ) ) = { 2 ∣ S ∣ − ∣ X ∣ if H is a forest , 0 otherwise . [z^{|S|-|X|}]\det(L_H+z\operatorname{diag}(2-\deg_H))=
\begin{cases}
2^{|S|-|X|} & \text{if }H\text{ is a forest},\\
0 & \text{otherwise}.
\end{cases} [ z ∣ S ∣ − ∣ X ∣ ] det ( L H + z diag ( 2 − deg H )) = { 2 ∣ S ∣ − ∣ X ∣ 0 if H is a forest , otherwise . Proof. By the matrix-forest theorem, det ( L H + diag ( d ) ) = ∑ F ∏ T ∈ F ( ∑ v ∈ T d v ) \det(L_H+\operatorname{diag}(d))=\sum_F\prod_{T\in F}(\sum_{v\in T}d_v) det ( L H + diag ( d )) = ∑ F ∏ T ∈ F ( ∑ v ∈ T d v ) F F F H H H T T T F F F d v = z ( 2 − deg H v ) d_v=z(2-\deg_H v) d v = z ( 2 − deg H v ) j j j z j z^j z j cc ( H ) ≥ ∣ S ∣ − ∣ X ∣ \operatorname{cc}(H)\ge|S|-|X| cc ( H ) ≥ ∣ S ∣ − ∣ X ∣ H H H F = H F=H F = H H H H z ∣ S ∣ − ∣ X ∣ z^{|S|-|X|} z ∣ S ∣ − ∣ X ∣ 0 0 0 H H H F = H F=H F = H ∏ T ∑ v ∈ T ( 2 − deg T v ) = ∏ T ( 2 ∣ T ∣ − 2 ( ∣ T ∣ − 1 ) ) = 2 cc ( H ) = 2 ∣ S ∣ − ∣ X ∣ \prod_{T}\sum_{v\in T}(2-\deg_T v)=\prod_T(2|T|-2(|T|-1))=2^{\operatorname{cc}(H)}=2^{|S|-|X|} ∏ T ∑ v ∈ T ( 2 − deg T v ) = ∏ T ( 2∣ T ∣ − 2 ( ∣ T ∣ − 1 )) = 2 cc ( H ) = 2 ∣ S ∣ − ∣ X ∣
In Grassmann form the mass − z deg H ( v ) ψ ˉ v ψ v -z\deg_H(v)\bar{\psi}_v\psi_v − z deg H ( v ) ψ ˉ v ψ v (7) applies with four labels per crossing edge. Brand, Dell and Roth [12 ] showed that, under #ETH, for every real x ≠ 1 x\ne1 x = 1 ε > 0 \varepsilon>0 ε > 0 T G ( x , 1 ) T_G(x,1) T G ( x , 1 ) exp ( ε n ) \exp(\varepsilon n) exp ( ε n ) O ( n ) O(n) O ( n ) 2 δ n 2^{\delta n} 2 δ n T G ( x , 1 ) T_G(x,1) T G ( x , 1 ) [7 ] .
Remark 11.4 (Further problems). A more general version of the template allows a constant number of global predicates (connected, tree, path, single cycle, forest, minimum number of components, and directed analogues such as branchings and strong connectivity), each certified by a determinant that is positive exactly when the predicate holds. It covers, among others, connected feedback vertex set, connected odd cycle transversal, minimum cycle cover, k k k κ \kappa κ
Verification and formalisation status
We describe what has been checked, by what means, and what remains open. The aim is to make clear how much trust each statement deserves. All Lean sources, the axiom-audit files (lean/EthFollowup/Axioms.lean, lean/EthFollowup/AxiomsExtended.lean and lean-bridge-anthropic/bridge/EthFollowup/ExactHC/AuditAll.lean), build instructions and the numerical check scripts are in the public repository [38 ] , https://github.com/xennygrimmato/eth-hamiltonicity , Lean sources as of commit ca17a37.
Machine-checked in Lean
Parity and randomized decision (Theorems 1.6 and 1.7 (a)). The Cut&Count identities, the counter encoding for unbounded degree, the restriction by edge CNFs, the Calabro–Impagliazzo–Kabanets–Paturi isolation lemma for arbitrary finite sets, its entropy estimate, and the machine theorems are proved in Lean 4 [21 ] with Mathlib [37 ] , taking the labs’ top-level theorems as hypotheses.
Discharging the hypotheses. OpenAI’s development was built from source at a pinned commit (Lean v4.34.1; 11,492 build jobs, no sorry); #print axioms reports only propext, Classical.choice and Quot.sound for exact_count_and_sat. The instantiated theorems (hamParity_allGraphs_unconditional, hamDecision_unconditional, dirHamParity_unconditional, dirHamDecision_unconditional, and others) are closed statements with
the same three axioms, and a kernel replay with leanchecker of the full import closure succeeds. Anthropic’s development was likewise built from source (Lean v4.33.1; 9,768 jobs); MainResults.mainTheorem depends only on the three standard axioms, and so does hamParity_allGraphs_anthropic instantiated with it.
Exact-count formalisation. The mathematical content of Theorem 5.7 is machine-checked. The Lean theorem blob_factorisation states that, for every graph G G G r r r ϕ \phi ϕ ∑ ℓ ∏ a σ a ( ℓ ) χ a ( ℓ , P ( ℓ ) ) I a ( ℓ ) = n ⋅ # H C ( G ) \sum_{\ell}\prod_{a}\sigma_a(\ell)\chi_a(\ell,P(\ell))I_a(\ell)=n\cdot\#\mathrm{HC}(G) ∑ ℓ ∏ a σ a ( ℓ ) χ a ( ℓ , P ( ℓ )) I a ( ℓ ) = n ⋅ # HC ( G ) propext, Classical.choice and Quot.sound. Its proof formalises:
Theorem 4.1;
the Grassmann algebra of § 3 (Koszul rule, block factorisation, linear forms);
Theorem 4.2 and Theorem 4.3, including det ( B F ) 2 = [ F is a spanning tree ] \det(B_F)^2=[F\text{ is a spanning tree}] det ( B F ) 2 = [ F is a spanning tree ]
Theorem 5.3;
the sign combinatorics (Theorem 5.4, Theorem 5.5, Theorem 5.6);
the locality of the blob tables.
The network of § 6 is also formalised in [A]'s own Net format, inside [A]'s Lean environment. Its value is proved to equal n ⋅ # H C ( G ) n\cdot\#\mathrm{HC}(G) n ⋅ # HC ( G ) log 2 5 \log_2 5 log 2 5 7.2 ) are formalised. The streaming procedure for the blob tables is also formalised in [A]'s cost model. It is proved to compute σ a χ a I a \sigma_a\chi_a I_a σ a χ a I a 2 ⋅ 8 μ a 2\cdot8^{\mu_a} 2 ⋅ 8 μ a Theorem 1.1 at the level of Turing machines (theorem1_TM): for every δ > 0 \delta>0 δ > 0 D D D # H C ( G ) \#\mathrm{HC}(G) # HC ( G ) C ⋅ 2 δ n C\cdot2^{\delta n} C ⋅ 2 δ n ∣ E ∣ ≤ D n |E|\le Dn ∣ E ∣ ≤ D n Theorem 1.1 is formally verified in Lean end to end (theorem1). On input the adjacency matrix of G G G # H C ( G ) \#\mathrm{HC}(G) # HC ( G ) ⌊ C ⋅ 2 δ n ⌋ \lfloor C\cdot2^{\delta n}\rfloor ⌊ C ⋅ 2 δ n ⌋ ∣ E ∣ ≤ D n |E|\le Dn ∣ E ∣ ≤ D n Theorem 1.2 is formalised as well (theorem2): one machine, with the same axioms, outputs # H C ( G ) \#\mathrm{HC}(G) # HC ( G ) ⌊ C ⋅ 2 C ( m + n ) / log 2 ( n + 2 ) ⌋ \lfloor C\cdot2^{C(m+n)/\sqrt{\log_2(n+2)}}\rfloor ⌊ C ⋅ 2 C ( m + n ) / l o g 2 ( n + 2 ) ⌋ G G G m m m leanchecker of the full import closure has passed for both theorem1 and theorem2.
Degree bound, corollaries, directed graphs. Theorem 1.3 is theorem3 and theorem3\_maxdeg; Theorem 1.4 is decision\_TM, search\_TM, hamPaths\_count\_TM and the related machines; directed Hamiltonian cycles and ATSP are theoremDHC, theoremDHC\_rate, theoremATSP; Theorem 10.2 is colouring\_barrier graph. All use the standard axioms only.
Weighted layer (TSP). Theorem 1.5 is formally verified end to end (theoremTSP, theoremTSP\_decode): for every δ > 0 \delta>0 δ > 0 D D D M M M C C C tspCodeGWw (the graph, W W W n 2 n^2 n 2 M M M n ∑ H 2 b w ( H ) n\sum_H2^{b w(H)} n ∑ H 2 b w ( H ) ⌊ C ⋅ 2 δ n ( W + 2 ) C ⌋ \lfloor C\cdot2^{\delta n}(W+2)^C\rfloor ⌊ C ⋅ 2 δ n ( W + 2 ) C ⌋ ∣ E ∣ ≤ D n |E|\le Dn ∣ E ∣ ≤ D n W W W j j j n n n j j j n n n blob_factorisation_w, the decoding lemma kronecker_decode, the weighted network hcNetW_kron in [A]'s Net format, and a weighted table procedure. Standard axioms only; a fresh leanchecker replay of its closure has passed.
Lean guarantees that the labs’ proofs establish their formal statements; it does not guarantee that those statements formalise the printed theorems faithfully, which is a matter for expert review. [A] itself notes that its Lean proof was compared with the printed one by AI models, not mechanically.
Numerical verification
The check scripts are attached to this record as ancillary files in anc/ (run python3 anc/run_all.py; reference outputs, where recorded, in the matching .log files) and are also in the project repository [38 ] , directory research/scripts: proof_checks.py and proof_params.py (the identities and parameter bounds of § 3 to § 6 ), review_exact_count*.py and review_hc_blobs.py (the independent referee’s checks, including an ablation of the sign term), hc_degree_network.py (Theorem 1.3 , with regression and mutation tests), tsp_check.py and tsp_atsp.py (TSP and ATSP), and ext_*.py (the extensions of § 11 ). All identities of § 3 to § 6 were implemented literally and independently of the code used during discovery, in exact integer arithmetic: an exterior algebra over Z \mathbb{Z} Z randomised generator order; the pieces, ε \varepsilon ε σ a \sigma_a σ a π a b \pi_{ab} π ab χ a \chi_a χ a W W W Ψ \Psi Ψ f f f ∏ a S a \prod_a S_a ∏ a S a K = 2 K=2 K = 2 3 3 3 ϕ \phi ϕ g ∈ { 4 , 5 } g \in\{4,5\} g ∈ { 4 , 5 } Table 4 summarises one run (60 instances, n ≤ 12 n \le12 n ≤ 12
A second script checks Theorem 7.1 (on 109 random graphs and several thresholds), Theorem 7.2 in the exact form g μ a ≤ 2 m + g Δ g\mu_a \le2m+g\Delta g μ a ≤ 2 m + g Δ g ≤ 12 g \le12 g ≤ 12 Theorem 1.4 . These checks test the identities and the network algebra, sign included; they cannot test the asymptotic bookkeeping, which is checked by hand.
A third script checks the rank-encoded network of § 8 on top of the same library: the colex rank, Theorem 8.2 (exact count, injectivity, round trip, surjectivity on random strings), the factorisation of Ψ \Psi Ψ Theorem 8.4 per node and in total, the profile count, Theorem 8.3 (sum over admissible profiles equals n ⋅ # H C ( G ) n\cdot\#\mathrm{HC}(G) n ⋅ # HC ( G ) I a I_a I a n ≤ 9 n \le9 n ≤ 9 g ≤ 4 g \le4 g ≤ 4 n − 1 n-1 n − 1 g = 4 g=4 g = 4 n ∈ { 7 , 8 , 9 } n \in\{7,8,9\} n ∈ { 7 , 8 , 9 } χ a \chi_a χ a
12.3. Independent referee. An independent referee (an AI agent working from the one-paragraph claim) derived the sign rule on its own and wrote its own code before reading the write-up. It checked about 500 instances of “Berezin integral = determinant”, about 790 blob evaluations and 297 evaluations of a literal [A]-style network (with g ≤ 5 g \le5 g ≤ 5
12.4. What is pending.
Human expert review of this paper and, above all, of the labs’ manuscripts.
A human check that the formal statements of theorem1 and theorem2 say what Theorems 1.1 and 1.2 say (the definitions to read are listed in § 1.6 ); the proofs were written by AI agents and reviewed by an AI coordinator.
A full write-up of the extensions of § 11 other than TSP.
12.5. Dependence on [A]. If [A, Theorem A(b)] or [A, Lemma 8] failed, Theorems 1.1 to 1.4 would lose their proofs, while § 3 to § 6 would be unaffected. The uniformity in Theorem 1.2 uses the constant c c c Theorem 2.6 through x 0 x_0 x 0 c c c O ( n ) O(n) O ( n ) poly ( n ) \operatorname{poly}(n) poly ( n ) τ \tau τ
Open problems
13.1. Dense graphs. The network of § 6 has U ≈ 2 log 2 5 ⋅ ∣ E ∣ U \approx2\log_{2}5 \cdot|E| U ≈ 2 log 2 5 ⋅ ∣ E ∣ § 8 has U ≈ 2 n log ( 2 e d ˉ ) U \approx2n\log(2e\bar{d}) U ≈ 2 n log ( 2 e d ˉ ) Theorem 1.3 beats 2 n 2^n 2 n d ˉ = 2 o ( log n ) \bar{d}=2^{o(\sqrt{\log n})} d ˉ = 2 o ( l o g n ) O ∗ ( 2 n ) O^{*}(2^n) O ∗ ( 2 n ) [30 , 2 ] and its 2 n − Ω ( n / log n ) 2^{n-\Omega(\sqrt{n/\log n})} 2 n − Ω ( n / l o g n ) [5 ] . For d ˉ = Θ ( n ) \bar{d}=\Theta(n) d ˉ = Θ ( n ) 2 n log n 2n\log n 2 n log n ℓ e U \ell_e U ℓ e U Ω ( e ℓ n log n ) \Omega(e_\ell n\log n) Ω ( e ℓ n log n ) n n n e ℓ = o ( 1 / log n ) e_\ell=o(1/\log n) e ℓ = o ( 1/ log n ) # H C \#\mathrm{HC} # HC
13.2. Connected subgraphs and T ( 1 , 2 ) T(1,2) T ( 1 , 2 ) The determinant certificate is a weight, not a 0/1 test, for objects that are connected but not trees. Exact counts of connected spanning subgraphs (T G ( 1 , 2 ) T_G(1,2) T G ( 1 , 2 ) x = 1 x=1 x = 1 κ \kappa κ
13.3. Derandomization from the top-level theorems. Theorem 1.1 gives deterministic decision, but it uses [A]’s internal lemmas. Can deterministic decision be obtained from the top-level # S A T \#\mathrm{SAT} # SAT S = H C ( G ) ⊆ { 0 , 1 } N S=\mathrm{HC}(G)\subseteq\{0,1\}^{N} S = HC ( G ) ⊆ { 0 , 1 } N ∑ x ∈ S w i ( x ) m o d q i \sum_{x\in S}w_i(x)\bmod q_i ∑ x ∈ S w i ( x ) mod q i q i ≤ Q q_i\le Q q i ≤ Q w i w_i w i S = ∅ S=\varnothing S = ∅ S S S 2 N ≤ lcm ( 1 , … , Q ) ( 1 + F ln Q ) 2^N\le\operatorname{lcm}(1,\ldots,Q)(1+F\ln Q) 2 N ≤ lcm ( 1 , … , Q ) ( 1 + F ln Q ) F F F F ≥ 2 N − o ( N ) F\ge2^{N-o(N)} F ≥ 2 N − o ( N ) Q = 2 ( log N ) 1 / 2 Q=2^{(\log N)^{1/2}} Q = 2 ( l o g N ) 1/2 2 N 2^N 2 N [23 ] . On the other hand, a fixed list of 2 o ( n ) 2^{o(n)} 2 o ( n ) n n n 2 o ( n ) 2^{o(n)} 2 o ( n ) [29 ] , in the relativised form of [31 ] . So the question is one of explicit hitting sets. These statements have written proofs but are not formalised.
The exponent
The leading term of the exponent is e ℓ U e_\ell U e ℓ U e ℓ = Θ ( ρ ℓ ) e_\ell= \Theta(\rho^\ell) e ℓ = Θ ( ρ ℓ ) ρ < 1 / 2 \rho< 1/\sqrt{2} ρ < 1/ 2 1 / log n 1/\sqrt{\log n} 1/ log n ρ → 1 2 \rho\to\frac{1}{2} ρ → 2 1 2 O ( m / log m ) 2^{O(m/\log m)} 2 O ( m / l o g m ) 2 O ( n log d / log ˉ n ) 2^{O(n\log d/\bar{\log} n)} 2 O ( n l o g d / l o g ˉ n ) Theorem 1.3 . Can the log n \sqrt{\log n} log n
Planar and minor-free graphs
A bound of 2 δ n 2^{\delta n} 2 δ n 2 O ( n ) 2^{O(\sqrt{n})} 2 O ( n ) 2 o ( n ) 2^{o(\sqrt{n})} 2 o ( n )
Practicality
As in [A], the bounds are astronomically far from practical. A less asymptotic analysis, or a different evaluation engine, would be needed for any concrete gain.
Acknowledgements
This work was done with AI assistance (Claude Code, Anthropic): the construction, the proofs, the numerical verification scripts, the independent referee pass and the Lean developments were produced in sessions with Claude Code. The Lean components described in § 12 are machine-checked; everything else has been checked numerically and by an independent AI referee, but awaits human expert review. Responsibility for any errors rests with the author.
References 