HEXAGONbeta

Decomposable disjoint-union circuits for primitive words

Primarily AI-generated textHuman understanding: all partscs.FL — Formal Languages and Automata Theory

Contributed by Will Howe, Grant Huffman ↗, Jensen Kohlmeyer ↗, Liam Kruer ↗

Version 1 / Nov 10, 2026 / CC BY 4.0

Abstract

For every fixed finite alphabet AA with at least two letters, we construct smooth decomposable circuits representing the primitive words of each length nn. The gates are literals, Cartesian products on disjoint position sets, and disjoint unions on equal position sets. The total number of gates and wires is OA(n25ω(n))=n2+o(1)O_A(n^2 5^{\omega(n)})=n^{2+o(1)}, and the construction takes n2+o(1)n^{2+o(1)} bit operations. Prime periods are expressed as coordinate directions of independent rectangular grids. A recursion at the first nonconstant vertex computes the exact set of failed directions; sharing its continuations gives the size bound. This resolves the primitive-word instance of the circuit question posed by Amarilli, Monet, Raphael, and Salvati. It does not determine whether primitive words form a context-free or a poly-slicewise-unambiguous language. The same circuit bound holds for any union of exact power orders at a fixed length.

Author comments: First version. Addresses the complement-free primitive-word circuit question in STACS 2026, Section 6. The main circuit-size theorem has a locally compiled Lean proof; the running-time and optional exact-order claims are separate from that formal verification. Independent mathematical review and priority have not been established.

Provenance statement

The mathematical draft, exposition and formalization were developed with OpenAI Codex under the direction of the listed contributors. Substantial portions are AI-generated. The submitting contributor has stated that all parts have been checked and understood by a human. The paper credits the circuit framework of Amarilli, Monet, Raphael, and Salvati (STACS 2026). The formal verification covers the circuit construction and its size, rather than the separate bit-operation running-time statement or optional exact-order extension.

References

  1. Antoine Amarilli, Mikaël Monet, Paul Raphaël, and Sylvain Salvati, On the complexity of language membership for probabilistic words , in 43rd International Symposium on Theoretical Aspects of Computer Science (STACS 2026) , Leibniz International Proceedings in Informatics 364 (2026), article 5, 5:1--5:21. doi:10.4230/LIPIcs.STACS.2026.5 (https://doi.org/10.4230/LIPIcs.STACS.2026.5).DOI
  2. Antoine Amarilli, Mikaël Monet, Paul Raphaël, and Sylvain Salvati, On the complexity of language membership for probabilistic words , full version, arXiv:2510.08127v2, 22 June 2026. https://arxiv.org/abs/2510.08127v2.arXiv

Version history

  1. v1 · 7 pagesSubmitted by Jensen KohlmeyerFirst version. Addresses the complement-free primitive-word circuit question in STACS 2026, Section 6. The main circuit-size theorem has a locally compiled Lean proof; the running-time and optional exact-order claims are separate from that formal verification. Independent mathematical review and priority have not been established.CurrentNov 09, 2026