arXiv weekly literature review

Formal Proof Assistants and Type Theory · primary corpus · published 2026-09-07T06:39:49Z
Jeremy Lindsay, Cezary Kaliszyk, Christine Rizkallah
arXiv categories: cs.LO

Mathematical proofs vary in legibility. While most proof optimisation techniques seek to minimise proof size, the strategic reordering of inferences can reduce the working memory demand of proof checking without altering overall size. Metamath serves as a prime case study for this approach: its verification architecture requires proof steps to be ordered in a manner that prioritises algorithmic efficiency over readability. In this paper, we introduce algorithms to minimise both peak and cumulative memory consumption, applying the latter as a novel proxy for sustained human cognitive effort. We achieve this by representing proofs as directed acyclic graphs and modelling their execution as a pebbling game. Finding an optimal ordering via brute force is computationally infeasible, so we use heuristics to provide approximations. We apply these algorithms across Metamath's ZFC set theory library and present case studies demonstrating how automated reordering systematically improves the presentation of formal mathematics.

arXiv abstract · PDF

Formal Proof Assistants and Type Theory · primary corpus · published 2026-09-07T11:09:03Z
Christoph Benzmueller, Daniel Kirchner
arXiv categories: cs.LO, cs.AI, math.LO

In Isabelle/HOL, we apply the deep-and-shallow embedding methodology of our prior work to monadic second-order logic (MSO). Three embeddings are developed side by side: a deep embedding (an inductive datatype with an explicit satisfaction relation); a maximal-shallow embedding that translates the connectives and quantifiers directly into HOL, carrying the interpretation and both assignments explicitly; and a minimal-shallow embedding -- a locale that fixes those parameters, collapsing the formula type to bool. The enabling new ingredient is a two-sorted substitution apparatus -- capture-avoiding substitution, renaming, and a substitution lemma per namespace -- in which each binder is transparent for the other; faithfulness of all three embeddings is mechanised and largely automated. Our central contribution is a fully mechanised two-sorted downward Loewenheim-Skolem theorem: the minimal embedding recovers deep validity relative to the (countable) assignment ranges, and this range-relative reading is shown to coincide with the general (Henkin-style) reading of MSO, whereas the standard reading validates strictly more formulas, witnessed by comprehension. Both readings are nonetheless recovered from the minimal embedding, differing only in the admitted interpretations: all of them for the general reading, only the elementary substructures of the full model for the standard. We exercise the embeddings on classical MSO landmarks: the Boolean-closure and graph schemata hold under the full second-order domain yet fail in the minimal embedding, making the dichotomy concrete, while reachability and 2-colorability are refuted throughout.

arXiv abstract · PDF

Formal Proof Assistants and Type Theory · primary corpus · published 2026-09-08T11:16:19Z
Nils Anders Danielsson
arXiv categories: cs.PL, cs.LO

This text is concerned with the question of whether, in type theory with erasure annotations, one can postulate that some type is inhabited and still have a guarantee that a program will not get stuck. Previous work has provided such guarantees for consistent erased postulates, i.e. postulates that are restricted to be used in erased contexts. Here those guarantees are extended to type theory with identity types. Similar ideas provide a simple way to support quotient types: it is shown that one can let things like "the equivalence classes for two related values are equal" be erased postulates and have an eliminator that only computes for the equivalence class constructor, and still get a guarantee that programs will compute correctly. Another question is whether programs compute correctly if one is allowed to transport (cast) using erased identity proofs. It is shown that this is safe in the absence of quotients and postulates, and in the presence of quotients and erased postulates that can be implemented using equality reflection. However, unrestricted transports of this kind are not compatible with erased, postulated univalence. For that reason the text includes a study of the function []-cong, which encapsulates a limited form of transport for erased identity proofs. The text is accompanied by machine-checked Agda proofs.

arXiv abstract · PDF

Formal Proof Assistants and Type Theory · primary corpus · published 2026-09-08T17:59:46Z
Idan Davidovich, Debargha Ganguly, Vikash Singh, Vipin Chaudhary
arXiv categories: cs.CL, cs.LO

Leading benchmarks for formal theorem proving with large language models are small collections drawn from competition math, such as the IMO and Putnam, that poorly represent field-specific applications. We introduce StochBench, a Lean 4 benchmark of 450 graduate stochastic-processes problems at varying abstraction levels, each paired with its natural-language source. Addressing a field underrepresented in Mathlib, it covers finite and countable Markov chains, renewal processes, random walks, martingales, stopping times, queues, Brownian motion, stochastic calculus, weak convergence, and Poisson and continuous-time Markov processes. Our Opus 4.8-based agent achieves a 34.9% proof rate (157/450) under a 15-minute per-problem limit. StochBench better represents domain-specific applied mathematics while remaining challenging for advanced provers.

arXiv abstract · PDF

Formal Proof Assistants and Type Theory · primary corpus · published 2026-09-09T16:58:50Z
Mart\'in H\"otzel Escard\'o
arXiv categories: math.LO, cs.LO, math.GN

Perhaps surprisingly, there are infinite types that can be exhaustively searched mechanically in finite time. We use ideas from topology to build plenty of them, referring to searchable types as compact types, and we use ordinals to measure their logical complexity. We consider two systems of ordinal notations under which a single notation denotes both a discrete ordinal and a compact one, with an embedding of the former into the latter whose image has empty complement. A boolean valued function decides which points in the image of the embedding are isolated and which are topological limit points. The first system consists of the traditional Brouwer codes and the second is an inductive-recursive universe generalizing them. The discrete ordinals so obtained are trichotomous, and the compact ones have the least element property for complemented subsets, but these two desirable properties cannot be fulfilled simultaneously in a constructive setting. The ordinals obtained from Brouwer codes further enjoy a boolean Leibniz principle, which has the notion of total separatedness as its topological counterpart. This extends previous work from G\"odel's system T to intensional Martin-L\"of type theory with univalent universes, and is formalized in Agda in the TypeTopology repository.

arXiv abstract · PDF

Formal Proof Assistants and Type Theory · primary corpus · published 2026-09-10T04:32:43Z
Jason Hickey
arXiv categories: cs.SE, cs.LO

SaltBench is a benchmark protocol for one question: How does a machine referee change the way a coding agent works? A machine referee --- a proof kernel, a program verifier, or a withheld test suite --- decides what an agent's work is worth, and the agent cannot argue with it. Here we report a protocol that makes the referee's effect measurable and whose answers cannot be narrated afterwards: every outcome is decided outside the agent's own toolchain; the agent is walled off from the network, the reference solutions and the harness itself, and the wall is tested by probes that try to breach it before any scored run, so the isolation is observed rather than assumed; every run is authorized by a dated freeze with its predictions registered; and a budget stop is a halt, never a failure. In this study, the subject of the benchmark is a ``seat'', meaning an agent session in its standard harness. We tested five systems components, all authored in Rust under a pinned Verus toolchain, with a withheld test suite as the referee for each. Four arms are tested: a plain agent; an agent that is also instructed to create a specification and verify the code against it, in a reduced rendering of the method, as registered; and two arms where the specification is provided a priori, extended under a dated amendment to $k=4$, where the registered sign test reached no verdict (3 of 4, $p = 0.3125$, every premium below the resolvable floor). We found that the arm instructed to specify and verify cost more on all five components, and by a practical margin: across these five components no premium exceeded $2.8879\times$ under either reading of the declared set, and the three cheapest sat below $1.4\times$. That bound is a property of this population and not a promise about larger ones: the premium runs near $1$ on the smallest components and rises with size. We publish the complete record.

arXiv abstract · PDF

Formal Proof Assistants and Type Theory · primary corpus · published 2026-09-10T07:20:15Z
Yukiko Kato
arXiv categories: cs.LO

This note consolidates the core of the Quasi-Closed World Graph Model for Conflict Resolution (QCW-GMCR), which extends the standard Graph Model for Conflict Resolution with Belnap's four-valued logic to represent option-level epistemic ambiguity, and pairs the framework with a machine-checked Lean 4 formalization. QCW-GMCR combines: (1) FOUR-valued option assignments with compositional propagation to state-level feasibility; (2) graded reachability (definite, credible, possible) based on an FDE-inspired transition-warrant semantics, with definite reachability related to FDE consequence in the Boolean fragment; (3) axiomatized deterministic reductions from four-valued assessments to binary decisions, including four canonical operators reflecting distinct risk attitudes; and (4) catastrophe-avoiding equilibrium concepts with a quasi-closed-world safety invariant. A four-valued hypergame extension captures heterogeneous subjective assessments across decision makers. We state the core definitions and results and report the parts verified in Lean 4 with mathlib, including the classical GMCR stability hierarchy, algebraic and compositional properties of FOUR-valued conjunction, properties of the canonical reductions, and the graded reachability hierarchy. The formalization also helped identify and correct earlier claims, including a knowledge-monotonicity axiom replaced by truth monotonicity. This preprint provides a stable, citable record of the framework and its current formal verification status.

arXiv abstract · PDF

Formal Proof Assistants and Type Theory · primary corpus · published 2026-09-12T07:50:39Z
Shogo Saitou, Mashu Noguchi
arXiv categories: cs.LO, math.LO

We mechanized proof of G\"odel's first and second incompleteness theorems, Solovay's arithmetical completeness theorem of \mathbf{GL}, and related results in the Lean 4 theorem prover.

arXiv abstract · PDF

Formal Proof Assistants and Type Theory · primary corpus · published 2026-09-12T18:56:14Z
Lars Warren Ericson
arXiv categories: math.CO, cs.LO, math.GN

For a finite set $S$ with $\lvert S\rvert = N$, the number of families $\mathcal{B} \subseteq \mathcal{P}(S)$ that are topological bases is $\#(N) = \sum_{\mathcal{T} \in \operatorname{Top}(S)} 2^{\lvert\mathcal{T}\rvert - \lvert\mathcal{M}_{\mathcal{T}}\rvert}$, where $\mathcal{M}_{\mathcal{T}}$ is the canonical minimal basis of minimal open neighborhoods. The identity is proved in Lean 4 / Mathlib (`CARDB.lean`): bases generating $\mathcal{T}$ are exactly the sets with $\mathcal{M}_{\mathcal{T}} \subseteq \mathcal{B} \subseteq \mathcal{T}$. The small-$N$ table and the discrete-dominance sandwich are proved in `CARDB/SmallN.lean` and `CARDB/Asymptotics.lean`.

arXiv abstract · PDF

Formal Proof Assistants and Type Theory · primary corpus · published 2026-09-13T06:18:21Z
S P Suresh
arXiv categories: cs.LO

We present a new proof of weak normalization for intuitionistic natural deduction. The distinguishing features of this proof are that it works only with cuts rather than cut segments, provides explicit local rules for determining whether to contract a whole proof or reduce one of its subproofs, and in the latter case, which subproof to reduce. We also discuss a formalization of the entire proof in Lean, and present a deterministic algorithm for weak normalization.

arXiv abstract · PDF

Formal Proof Assistants and Type Theory · cs.SE candidate · published 2026-09-13T21:47:46Z
Andre Panossian
arXiv categories: physics.comp-ph, cs.SE

Scientific autoformalization turns verbal accounts into executable mathematics, but executable code does not settle which model has been constructed. We examine two sources of structural uncertainty: the formalizer that generates a response law, and the recurrence that turns that law into trajectories. In secondary analyses of an openly archived crossed experiment, we studied 320 response maps generated by two pinned language-model formalizers from five engineered cognitive accounts within one sparse quadratic grammar and 16 randomized blocks. With whole blocks held out, source-account identity was recovered at 78.8% accuracy (chance 20.0%) and formalizer identity at 96.3% (chance 50.0%; both p < 0.001). Program size was the stronger single feature family; a pre-specified exploratory comparison found no stable source-account predictive gain from local geometry beyond size. Holding every response map fixed, we then evaluated five recurrence families spanning 33 configurations and 1,013,760 finite-horizon trajectories. Added feedback, projection and leak produced sharply different outcome distributions. The consequential distinction was which comparisons survived: median cross-recurrence rank concordance was 0.73 for endpoint magnitude but 0.05 for settling, among the configuration pairs with defined rankings. Thus a common mathematical language did not erase translation provenance, and robust ordering under one observable did not transfer to another. Scientific autoformalization is usefully studied as model-space construction: the generated ensemble and its dynamical embedding are both part of the specification supporting a scientific claim.

arXiv abstract · PDF

Logical Reasoning and Proof Complexity · primary corpus · published 2026-09-07T10:46:53Z
Somayeh Chopoghloo, Mohammad Golshani
arXiv categories: math.LO

We develop a set-theoretic translation of a normal modal extension $T_m$ of a recursively axiomatizable first-order theory $T$. We first pass to the Henkin expansion of the underlying language by adding witness constants and work with the sentence algebra of this expansion. The translation is constructed using the corresponding Lindenbaum-Tarski algebra, the Stone space of its ultrafilters, and quotient forcing by a $\sigma$-ideal of Borel sets; in particular, the meager ideal yields Cohen forcing and the null ideal yields the random forcing. In a Boolean-valued universe, we interpret the modal operator $\Box$ by membership of the Boolean value of the translated formula in a suitable filter name. We prove that this translation is sound and complete: a modal formula is provable in $T_m$ if and only if its set-theoretic translation is forced in every associated interpretation. We then build Kripke frames and models from generic extensions and show that the forcing interpretation of $\Box$ agrees with quantification over the corresponding accessibility relation. As a consequence, we obtain completeness with respect to the resulting Kripke models.

arXiv abstract · PDF

Logical Reasoning and Proof Complexity · primary corpus · published 2026-09-07T22:24:01Z
Theodoros Papamakarios
arXiv categories: cs.LO

We show that a (stronger) version of random resolution has the feasible disjunction property. This is the first instance of a proof system not known to have feasible interpolation, which nevertheless has the feasible disjunction property.

arXiv abstract · PDF

Logical Reasoning and Proof Complexity · primary corpus · published 2026-09-08T16:15:00Z
Balder ten Cate
arXiv categories: cs.LO, cs.LG

For a finite set $O$ of Boolean functions, we consider the class of propositional formulas built using the functions in $O$ as connectives. We determine, for each possible choice of $O$, the complexity of various fitting and learning problems. These include: finding a formula that fits a given labeled sample, finding a small one (an Occam algorithm), minimizing the number of misclassified examples when the sample is not realizable (empirical risk minimization), and several forms of PAC learning. Our results apply both to formulas (represented as trees) and to circuits. We also briefly discuss the status of the same questions for other kinds of propositional fragments.

arXiv abstract · PDF

Logical Reasoning and Proof Complexity · primary corpus · published 2026-09-08T16:23:32Z
Arthur Nakamura, David Drummond, Welbert Pereira, Gustavo Lahr, Kaique Matias de Andrade Roberto
arXiv categories: cs.LO, math.ST, stat.TH

Paraconsistent Annotated Logic with two values (PAL2v) annotates a proposition with a pair $(\mu,\lambda)$ of degrees of favorable and unfavorable evidence, drawn from a bilattice whose four extreme points are the values of Belnap and Dunn. In applications, however, the second coordinate is almost always taken to be the complement of the first, and several such annotations are then fused. We show that this practice determines the sign of the degree of contradiction in advance, independently of the data: for aggregation functions $F$ and $G$ the fused degree of contradiction equals $F-G^{d}$, where $G^{d}$ is the De Morgan dual of $G$, so that it vanishes identically when the two are dual, and has a constant sign otherwise. In particular the componentwise minimum used throughout the literature yields only consistent annotations, and the conjunction of annotated logic only exact ones; five of the twelve logical states, contradiction among them, are essentially unreachable by construction. We also give a decision procedure for the twelve states that is provably total, in place of the inequality lists in current use, which assign two states to about half of the non-extreme region. We then propose a construction in which the two coordinates are computed from disjoint families of evidence, show that every logical state is attainable. Educational assessment provides a natural instance, since summative and formative instruments are institutionally distinct: mapping examinations to $\mu$ and disengagement to $\lambda$ makes the degree of contradiction equal to the gap between what a student demonstrates and what that student invests. Simulations over three cohort profiles illustrate the classification.

arXiv abstract · PDF

Logical Reasoning and Proof Complexity · primary corpus · published 2026-09-08T23:16:15Z
Juntao Wang, jieqiong Shi, Mei Wang
arXiv categories: math.LO

The main aim of this paper is to introduce a Frobenius--Galois expansion of the substructural logic $\mathbf{FL}_{ew}$ and develop its algebraic and categorical semantics. The resulting logic, denoted by $\mathbf{FL}^{\mathbf{FGC}}_{ew}$, is obtained by adjoining a pair of unary connectives forming a Galois connection and satisfying suitable Frobenius-type compatibility conditions. Firstly, we prove that $\mathbf{FL}^{\mathbf{FGC}}_{ew}$ is algebraizable in the sense of Blok and Pigozzi and identify its equivalent algebraic semantics with the variety of Frobenius-adjoint residuated lattices, establishing the conservativity over $\mathbf{FL}_{ew}$ and relating its finite model property to residual finiteness of finitely generated free algebras. Secondly, for the distributive setting, we lift the Kalman construction to the Frobenius-adjoint algebraic framework. More precisely, we establish a categorical equivalence between Frobenius-adjoint residuated distributive lattices and Frobenius-adjoint $c$-differential residuated distributive lattices with the condition $\mathbf{CK}$. This equivalence yields a positive-cone representation of the former structures and, in turn, a logical counterpart of the categorical correspondence. Finally, for the distributive extension $\mathbf{FL}^{\mathbf{FGC},d}_{ew}$, we prove that derivability, validity over Frobenius-adjoint residuated distributive lattices, and validity over the corresponding positive cones determine the same consequence relation, and further show that this correspondence preserves equational and quasi-equational consequence, conservativity, and finite countermodels. These results provide a unified algebraic, categorical, and logical framework for Frobenius--Galois expansions of substructural logics.

arXiv abstract · PDF

Logical Reasoning and Proof Complexity · primary corpus · published 2026-09-10T09:56:17Z
Jose Pascual Gumbau Mezquita
arXiv categories: cs.LO, cs.AI, cs.CL, math.LO

The undecidability of a program's static semantic properties is governed by Rice's theorem. Self-modifying systems, however, require analysing not whether a property holds now, but whether it is preserved when the system rewrites itself. We formalise this transition through a semantic elevation operator {\Lambda}{\Phi}, which turns the static question "does x satisfy P?" into the dynamic question "is P preserved after x is transformed by {\Phi}?". We prove that when {\Phi} is intensional (depending on the source code, not only on the computed function), the elevated property remains undecidable even though it breaks the extensionality that Rice's theorem requires; the proof rests on Kleene's recursion theorem, not on Rice. Consequently the class U of non-verifiable properties is closed under the elevation operator. Unbounded iteration of the operator climbs the arithmetical hierarchy -to {\Pi}02-completeness- consolidating non-verifiability as a structural fact. We further show that the supervisory regress does not terminate: no fnite tower of increasingly capable verifiers yields an unconditional certificate. A categorical reading of these results in the efective topos, in which elevation appears as an instance of Lawvere's fxed-point theorem, is left as a direction for future work.

arXiv abstract · PDF

Logical Reasoning and Proof Complexity · primary corpus · published 2026-09-10T13:17:14Z
Yasmine Briefs, Christoph Weidenbach
arXiv categories: cs.AI, cs.LO

Quantifier instantiation is currently the main approach to non-ground SMT solving: solvers generate ground instances and solve the resulting ground SMT problems with CDCL(T)-style reasoning. When a conflict is found, conflict analysis learns only a ground clause, even though the conflict comes from instances of non-ground clauses. Yet non-ground reasoning can give exponentially shorter proofs than purely ground reasoning. We propose a calculus that consists of ground instantiations, CDCL(T)-style rules, and non-ground conflict analysis. The solver reasons on ground instances, but the resolution steps of conflict analysis are performed on their original non-ground clauses. This produces learned clauses that are typically more general than the ground conflict. With a suitable strategy, the learned clauses are even non-redundant. We also show how chronological backtracking can be included in SMT solving. Our calculus gives a common setting for CDCL(T)-style SMT solving, a range of instantiation-based procedures, and non-ground clause learning, and we prove that it simulates CDCL, SCL(FOL), SCL(T), and even Resolution.

arXiv abstract · PDF

Logical Reasoning and Proof Complexity · primary corpus · published 2026-09-10T14:10:49Z
Pawel Pawlowski
arXiv categories: cs.LO, math.LO

This project began as an attempt to prove that Medvedev logic is decidable with the help of generative AI systems. The author (as well as the generative AI systems, or at least they claim to be since I have asked them) was surprised by its eventual conclusion. We prove that Medvedev logic ML, the intermediate logic of finite problems, is Pi-01-complete under computable many-one reductions. Consequently, ML is not recursively enumerable, a fortiori undecidable, and admits no recursively enumerable sound and complete proof calculus. The proof connects the periodic domino problem with intuitionistic formulas through a shared intermediate structure that we call a Wang-Medvedev pair. Such a pair consists of a finite partially ordered set of roles together with demands. Demands define the interaction between roles. A realization labels nonempty subsets of a finite set with these roles, respecting the order and satisfying the demands. We associate a pair with each finite Wang system and show that it has a realization iff the system tiles a finite torus. We then construct an intuitionistic formula that fails on some finite Medvedev frame iff the same pair is realizable. Realizability thus provides the link between periodic tilings and the countermodels.

arXiv abstract · PDF

Logical Reasoning and Proof Complexity · primary corpus · published 2026-09-10T15:06:30Z
Khashayar Irani
arXiv categories: cs.LO, cs.AI

In this paper, we develop warrant theory as a philosophical discipline concerned with the inferential legitimacy of propositions within logical analysis. Warrant theory reconceptualises logic as a normative framework governing the conditions under which propositions may be introduced, accepted, rejected, and inferentially employed. Warrant is understood as inferential entitlement and is distinguished from truth, belief, and other psychological attitudes, while its relation to inferential use and meaning is examined. Warrant-theoretic analysis is then developed as a systematic method for investigating how propositions acquire inferential standing, how that standing develops, and how inferential positions interact through relations of dependence, compatibility, incompatibility, and exclusion. Acceptance and rejection provide the bilateral vocabulary for representing positive and negative inferential positions and the consequences and commitments associated with them. Finally, these elements are brought together in a warrant-theoretic definition of logic as the formal and normative study of the conditions under which propositions may be legitimately accepted or rejected and of the inferential transitions that such legitimacy warrants. On this account, logical consequence and logical failure are understood through the presence, preservation, or absence of inferential entitlement, thus locating the philosophical subject matter of logic in the systematic governance of inferential legitimacy.

arXiv abstract · PDF

Logical Reasoning and Proof Complexity · primary corpus · published 2026-09-10T18:41:39Z
Magnus Boman
arXiv categories: cs.LO, math.LO

We study fifteen properties of binary relations that have established uses in modal logic, order and preference theory, and relation algebra. The organising question is pragmatic: once some properties of a relation are known, which further properties follow, which combinations force degeneracy, and which properties remain independent? We give a proved Horn basis of elementary and compound entailments, explicit countermodels for non-entailments, and a relation-algebraic translation of all fifteen properties. The modal discussion includes the usual Scott--Lemmon correspondences and the logic of transitive dense frames studied by Ghilardi and Mints. Exhaustive finite enumeration and targeted model search are used for discovery, while the catalogue is certified in Lean. A kernel-checked coverage calculation ranges over all 2^15 = 32,768 antecedent sets and all fifteen possible consequents. Its 51-rule Horn manifest is coupled definitionally to Lean proofs of semantic soundness, and its 49 witness rows are coupled definitionally to Lean-certified finite or infinite relations. Consequently, over non-empty domains, the Horn closure is complete for positive entailment among the fifteen selected properties, and the consistency classification is complete for their positive combinations.

arXiv abstract · PDF

Logical Reasoning and Proof Complexity · primary corpus · published 2026-09-11T17:49:49Z
Rodrigo Nicolau Almeida, S{\o}ren Brinck Knudstorp
arXiv categories: math.LO, cs.LO

We show that Medvedev's logic of finite problems, a well-known superintuitionistic logic, is undecidable. The key method is a reduction from the periodic tiling problem to non-theoremhood in Medvedev's logic. This settles a longstanding open problem. Using similar techniques, but reducing instead to the ordinary tiling problem, we likewise obtain undecidability of Skvortsov's logic of infinite problems, and the fact that the two logics are distinct -- in fact, they are separated by any aperiodic tiling of the plane. Due to the fact that Medvedev's logic figures in so many different areas, these results have implications for several fields -- for example, the study of schematic fragments of logics such as propositional dependence logic, or the study of internal logics of toposes. The core idea and technical work of the undecidability proof were obtained using ChatGPT Sol 5.6, and formally verified in Lean by Claude Opus 5. A detailed methodology section outlines how such results were obtained.

arXiv abstract · PDF

Logical Reasoning and Proof Complexity · primary corpus · published 2026-09-11T20:46:32Z
Mirco A. Mannucci, Giovanni Sambin
arXiv categories: cs.LO, cs.AI

We develop a conceptual and operational account of Positive Topology starting from a basic relation between points or models and observable properties. From this relation, two complementary structures emerge. The first captures universal refinement and cover: what must hold across all relevant cases and how information can be systematically refined. The second captures positivity and witnessed existence: what can be positively realized and sustained without relying on classical complements. A central result shows that the underlying relation between points and observables can be reconstructed from either of these induced structures. We also clarify the distinction between point-based and pointfree formulations: when points are available, positivity can be derived from the underlying forcing relation, while in the formal pointfree setting positivity is taken as primitive and its compatibility with cover is imposed axiomatically. We develop two complementary interpretations of the framework. The first is information-theoretic, viewing cover as refinement of partial information and positivity as witnessed feasibility. The second is game-theoretic, viewing positivity as the ability of a witness or hypothesis to survive successive legitimate refinements. The final part of the paper is deliberately programmatic. We outline how resource constraints, verification costs, and finite budgets can be incorporated into the framework. This leads to resource-sensitive notions of forcing, cover, positivity, and refinement, and raises new questions about how these structures behave as available resources change. Examples from medical diagnosis, legal reasoning, and AI systems illustrate the potential relevance of the approach to grounded, explainable, and resource-aware inference.

arXiv abstract · PDF

Logical Reasoning and Proof Complexity · primary corpus · published 2026-09-12T05:27:20Z
Kainan Zhou, Gangzhen Qian, Zhaoyi Li, Hang Xiao
arXiv categories: cs.AI, cs.LO

An external record may contain a procedure to apply or text to read, depending on the user's request. IBBench-Light tests both uses against the same record. Twelve semantic bases yield 144 matched pairs per model; four quantized instruction models produced 1,152 archived greedy responses. Paired exact-contract accuracy (PECA) requires both members to satisfy their output contracts. Qwen succeeds on 132 execute and 109 process prompts, but only 97 complete pairs, showing what marginal averages omit. We audit literal-target exposure and case normalization, then add 1,722 logged CPU generations to test directive-absent controls, twelve additional semantic bases, within-base wording changes, and generation stopping. In the pinned Phi rerun, changing the end-of-sequence (EOS) set changes exact paired success from 0/144 to 62/144. A bounded IHEval comparison uses the same SmolLM2 checkpoint and output budget while preserving its published instruction roles and scorer. The benchmark measures conditional task and output-contract success. Its task margins and paired count need to be read together with the stopping policy.

arXiv abstract · PDF

Logical Reasoning and Proof Complexity · primary corpus · published 2026-09-12T18:50:37Z
Tom\'a\v{s} Kol\'arik, Faezeh Labbaf, Fabrizio Leopardi, Grigory Fedyukovich, Michael Wand, Natasha Sharygina
arXiv categories: cs.LO, cs.LG

Formal explainability of classifying neural networks (NNs) is an active area of research, providing explanations with provable guarantees of the classification within continuous regions of the input feature space. However, the existing techniques are either limited to individual input features without guarantees on their relations or the provided solutions fail to scale to deep architectures. This paper addresses these issues by introducing a flexible symbolic framework for an efficient, guided computation of explanations of the NN behavior, parametrized by the activations of internal neurons, and using logical engines such as SMT solvers. Unlike prior methods that rely on specialized NN verifiers, our method yields explanations that are not restricted in shape. Our algorithm is implementable on top of a general-purpose logical solver, isolating the NN-specific encoding from the algorithmic framework. We experimented with a wide range of benchmarks from the domains of image recognition and medicine, illustrating the advantages of the new method, particularly in computational efficiency. Notably, our approach enables logical explanation of deep networks not amenable to prior logic-based methods.

arXiv abstract · PDF

Logical Reasoning and Proof Complexity · primary corpus · published 2026-09-13T23:03:36Z
Harrison Green, Claire Le Goues, Fraser Brown
arXiv categories: cs.SE, cs.LO

The software status quo is to use one system to process many different kinds of inputs. In contrast, we propose hyperspecialization: creating new software that is optimized for a single class of inputs. Hyperspecializing manually is anywhere from expensive to impossible. We conjecture that coding agents make automated hyperspecialization cheap, effective, and safe for problems with measurable performance and checkable output. This paper explores one such problem, SAT solving, by synthesizing hundreds of workload-specific SAT solvers at an average cost of \$37 each. Our specialists outperform their competition-winning, general-purpose cousins by 5$\times$ on average, and by over $10\times$ on a quarter of benchmark families. A general-purpose solver constructed from over a hundred of our prototype hyperspecialists won the SAT track at the 2026 SAT Competition.

arXiv abstract · PDF

Program Verification and Reactive Systems · cs.SE candidate · published 2026-09-07T11:35:49Z
Eitan Farchi
arXiv categories: cs.SE

Formal specification promises early error detection, explicit invariants, and correctness by design, yet its notational cost has kept it out of mainstream practice. We argue that AI removes much of that cost: natural language enriched with lightweight mathematics, written in \LaTeX, can serve as an intermediate specification language that is precise enough to reason over and prove, while a large language model (LLM) reviews it for ambiguity, drafts proofs, and generates the implementation. The specification becomes the artifact one authors, reviews, proves, and refines; the code becomes regenerable output. This paper is a follow-on to a prior study that established the discipline on an organizational-knowledge-growth simulation~\cite{predecessor2026}. Here we replicate the discipline in a different domain---an online-banking fund-transfer service---and extend it. The two domains share one spine: a conservation invariant (knowledge in the prior study, money here), which suggests the approach generalizes across domains. We contribute: (i) a second, independent case study of the method; (ii) a stress-test of the method on a richer problem---\emph{scheduled/recurring} transfers---whose generated code grows substantially while the invariant and its proof do not; (iii) an \emph{AI-proposed runtime coverage model} for invariants (``never violated $\neq$ covered''); and (iv) a Z formalization, including paired success/failure operation schemas and an invariant proved over the inductive set of all reachable configurations, together with an experiment in which the AI proposes the Z interfaces itself. We are explicit about the method's limits: the proofs and runtime checks live at the specification level and do not establish that the generated code refines the specification---that step is delegated to the AI. This is a case study, not a controlled experiment.

arXiv abstract · PDF

Program Verification and Reactive Systems · primary corpus · published 2026-09-07T17:58:09Z
Nicklas Nidh\"ogg
arXiv categories: cs.PL

Classical panic-mode recovery skips a failed scan forward by convention: it promises progress, and membership in a designated set where one is found, but no repair-universal boundary guarantee for the position it lands on. This paper chooses the resume position by theorem: a position is a sound recovery point when every prefix repair whose scan commits through the certificate's returned evidence places a token boundary there, complete repairs the special case, by a committed-prefix lemma over certificates posted for a different purpose (arXiv:2608.03473, arXiv:2608.09761). The quantifier is strictly the stronger one, and a dichotomy locates the difference exactly: the inclusion is strict precisely when no repair completes while some scan still commits through the evidence, a two-token witness realizing the case. The evidence-returning form pairs each answer with the interval it rests on, which is what makes the guarantee deployable: a caller who knows what the scanner cannot check decides whether the certified boundary transfers to the clean input it intended. The search is one forward walk in evidence order and provably terminates; the guarantee is per-automaton, relative to the active mode. The procedure ships in the munch lexing library, and a deterministic corruption study measures its recovery quality beside the classical skip-one and delimiter conventions. Every certified answer whose evidence survives the damage passes its executable landing check on every recovery move, 40,885 of 40,885; among first answers, the 5,595 resting on evidence the damage reached land 1,589 times, reported and never asserted. On 13,522 of the 16,808 trials the shipped repair routine labels beyond repair, the resumed suffix tokenizes whole and the two quantifiers provably coincide, so both are empty there if those negative labels are exact; 3,286 stay undetermined.

arXiv abstract · PDF

Program Verification and Reactive Systems · primary corpus · published 2026-09-08T02:44:49Z
Andreas Andreakis
arXiv categories: cs.DB, cs.DC, cs.LO

Change-data capture (CDC) feeds downstream systems like caches, search indexes, and data warehouses from a database's log of committed row changes. When bootstrapping, adding a table, or repairing downstream data, a pipeline must also copy existing rows. Merging this copy with the active log introduces the copy-to-log handoff problem. Changes must not fall through a gap, and older copied state must not overwrite a newer logged update or resurrect a deleted row. DBLog, developed at Netflix, addressed this problem by reading tables in chunks and interleaving those reads with the live log. Watermarks identify the changes that overlap each read, and the log wins when a copied row is stale. Debezium and Flink CDC have since adapted this design. Earlier work proved that applying the original algorithm's copied rows and logged changes in their emitted order reconstructs the source's rows, including the effect of every logged insert, update, and delete processed. Generalized DBLog asks when the same result holds for variants of that design. We state the conditions the source and capture implementation must satisfy. Once copying and reconciliation are complete, we prove that the result holds across all selected tables and key ranges even when their rows were read at different times. A single database snapshot is not required for the copy. Further logged changes advance the reconstructed state one event at a time. We establish these guarantees for classic watermarking, Debezium's signal-table and read-only modes, Flink CDC's parallel chunks, reads and dumps tied to exact log positions, and engine-consistent backups whose log position lies within known bounds. The complete theory is machine-checked in Isabelle/HOL, its core independently verified in Lean 4, and the protocols are also examined by bounded model checking in TLA+.

arXiv abstract · PDF

Program Verification and Reactive Systems · primary corpus · published 2026-09-08T20:44:28Z
Antoine Besset, Joris Tillet, Chuchu Fan, Julien Alexandre dit Sandretto
arXiv categories: cs.LO, cs.RO, cs.SY, eess.SY

Ensuring the satisfaction of Signal Temporal Logic (STL) specifications under uncertainty is challenging, as reachability-based monitoring provides guarantees but does not indicate how to restore satisfaction when it becomes indeterminate. A key difficulty is identifying which uncertain components actually affect global satisfaction, especially for nested formulas. This paper introduces a logical dependency tracking framework that propagates uncertainty through the STL structure and captures the causal contribution of reachable sets to satisfaction. By associating markers to uncertain predicates and propagating them via three-valued semantics, we extract in milliseconds a compact Disjunctive Normal Form (DNF) of sufficient constraints, avoiding combinatorial enumeration. As an application, we formulate control correction as a minimum-effort optimization problem. Using zonotopic reachability, the derived constraints are enforced via linear programming, yielding corrections that guarantee STL satisfaction under bounded uncertainty and provide certified probabilistic bounds in the stochastic case. We demonstrate the approach on a nonlinear system with nested STL specifications, showing that dependency tracking enables efficient and formally guaranteed correction. The tracking implementation is available at https://github.com/Antoine-Bst/STL-Three-Valued-Clause-Filtering/.

arXiv abstract · PDF

Program Verification and Reactive Systems · primary corpus · published 2026-09-09T02:57:26Z
Xizhe Yin, Yaokun Zhang, Yang Feng, Baowen Xu
arXiv categories: cs.PL

Rust guarantees memory safety without garbage collection through a strict ownership and borrowing system. However, for low-level systems programming, many widely used libraries rely on the unsafe keyword. These libraries encapsulate raw-pointer operations behind safe APIs to form safe abstractions. A single mistake in this internal unsafe code can break its safety contract, rendering the abstraction unsound and allowing safe clients to trigger undefined behavior. Detecting these potential soundness violations is challenging. Existing static analysis tools for C/C++ ignore Rust-specific safety contracts, while current Rust tools lack the deep semantic modeling required to track the contexts that raw pointers erase. To address this gap, we present UnsafeChecker, a compiler-integrated static analysis framework for detecting potential soundness violations in Rust safe abstractions. UnsafeChecker analyzes Rust MIR using a flow-sensitive abstract interpretation that maintains a shared state with three components: ownership, object validity, and layout. Each warning rule consumes the subset of facts needed for the corresponding Rust safety obligation. UnsafeChecker reports both instruction-level undefined behavior and boundary-level contract violations that may escape through safe APIs. We evaluate UnsafeChecker on a benchmark of 46 RustSec vulnerabilities, which contain 53 ground-truth bugs. UnsafeChecker outperforms several state-of-the-art tools, detecting 32 CVEs and covering 36 bugs (67.9% recall) with 51.6% alert-level precision. Furthermore, in a large-scale scan of real-world crates on crates.io, UnsafeChecker uncovered 114 previously unknown bugs across 83 crates, with 45 confirmed and 27 already fixed by maintainers.

arXiv abstract · PDF

Program Verification and Reactive Systems · primary corpus · published 2026-09-09T12:47:28Z
Fran\c{c}ois Hublet, Dhruv Nevatia, Joshua Schneider
arXiv categories: cs.LO

We study the policy change problem that arises in the runtime verification of long-running systems. The online monitors typically used in this context are generally treelike, in that they maintain substates that monitor subformulae of the target policy. We consider when and how the policy can be changed while the monitored system is running by only exploiting the information stored in the monitor's state. This is relevant, for example, to account for new system functionality or changes in regulatory requirements. We formally define the policy change problem in a general setting, independent of any specific (treelike) monitor implementation. We then show that policy change for past-time metric temporal logic (pMTL) is decidable but has tight non-primitive recursive lower and upper bounds, while with discrete-time semantics it is EXPSPACE-complete.

arXiv abstract · PDF

Program Verification and Reactive Systems · primary corpus · published 2026-09-09T15:44:46Z
Harshita Gupta, Mayank Kabra, Rakesh Nadig, Nika Mansouri Ghiasi, Sahand Divsalar, F. Nisa Bostanci, Ataberk Olgun, Konstantinos Kanellopoulos, Jisung Park, Haiyu Mao, Abdullah Giray Yaglikci, Mohammad Sadrosadati, Onur Mutlu
arXiv categories: cs.AR, cs.CR, cs.LO

Data-intensive applications move large amounts of data from storage to the compute unit, incurring significant data movement overhead. Storage-centric computing reduces this overhead by moving computation near or inside solid-state drives (SSDs). Enabling it requires modifying SSD policies, e.g., address translation and garbage collection, which are part of the Flash Translation Layer (FTL), the SSD's firmware. Modifying the FTL is error-prone. Because FTL logic has direct access to security-critical device components, even a functionally correct FTL can leak data between tenants, drop integrity tags, or assign a flash block to the wrong tenant. We show that a faulty FTL can corrupt the device state at five surfaces inside the SSD, and demonstrate them on a DaisyPlus OpenSSD. Prior work verifies individual FTL designs, but has two limitations. (1) It establishes only functional correctness, so a modified FTL can violate isolation, integrity, and ownership and still pass verification. (2) It is tied to a single FTL design, so every modification requires redoing every proof. We propose CertiFlash, a formal verification framework for FTLs, mechanized in the Rocq proof assistant, that gives designers a machine-checked proof of security and correctness. CertiFlash models an FTL as a deterministic state machine with a single global invariant over mapping, isolation, integrity, ownership, and allocation. We prove once, over a general FTL model, that (i) every FTL operation preserves the invariant and (ii) the model refines an idealized block device. For a new design, a designer discharges five hypotheses about its own operations instead of redoing either proof. Across four case studies, a designer adds 27 to 3,231 lines against a 16,489-line framework, significantly reducing the verification effort. CertiFlash is open source.

arXiv abstract · PDF

Program Verification and Reactive Systems · primary corpus · published 2026-09-09T17:07:59Z
Shay Allen Logan, Shawn Standefer, Thomas Ferguson
arXiv categories: cs.LO

We introduce the logic EDMon---an epistemic dynamic logic meant to model monitorability concepts in noisy runtime verification. Its syntax and semantics are defined and explained and the connection between EDMon and monitorability and noisy runtime verification concepts is explored. We then demonstrate that EDMon is sufficient to capture many of the results in the noisy runtime verification literature and catalog its relation to nearby logics and describe a large class of its theorems.

arXiv abstract · PDF

Program Verification and Reactive Systems · cs.SE candidate · published 2026-09-10T01:42:40Z
Zihao Zheng, Baichuan Li, Junyi Yao, Jiayu Long
arXiv categories: cs.SE

Agentic systems commit state-changing actions, but additional verifiers can inherit the same upstream fault. We present VP-CONTROL, a runtime-assurance design and deterministic benchmark for cost-aware commit gates. Its 48 task templates yield 2,880 scenarios across six fault regimes. A fixed-call 2 x 2 experiment separates verifier-model diversity from evidence-source diversity. On frozen proposals from two local actor families, a cross-model vote over shared evidence approves 62.9% of unsafe proposals, versus 22.9% with an independent source. The source effect is 40.9 percentage points, compared with 11.3 for model diversity. A portfolio controller selects verification plans using only deployment-observable metadata. Approximate cluster-adjusted calibration at a nominal 5% per-task target yields 1.9% unsafe execution and 38.2% automated safe coverage on the locked test. Matched-budget portfolios also improve on fixed verification policies. Transfer remains conditional: unseen fault families yield 16-26% risk, and a FinQA check fails to reproduce the source effect with the tested small verifiers. A preregistered live HTTP/SQLite study tests concurrent writes and lost responses. After-check races defeat verifier-only gates; transactional partial guards prevent only covered failures, while a full atomic guard records no unsafe effects across 216 episodes. Idempotent request identifiers prevent duplicate effects after lost responses. The results motivate explicit evidence lineage, cost-aware selection, and commit-time enforcement, while exposing the limits of approximate calibration and local-tool generalization.

arXiv abstract · PDF

Program Verification and Reactive Systems · cs.SE candidate · published 2026-09-10T11:17:19Z
Shengcheng Yu, Chunrong Fang, Zhenyu Chen
arXiv categories: cs.SE, cs.AI

Embedding an intelligent agent in an existing application creates a persistent coordination problem: users can revise goals and manipulate shared objects while delegated execution continues. We argue that dependable integration requires an explicit correspondence between task-level interaction and application behavior. We introduce Agent-Integrated Software (AIS) as a software pattern combining a conventional core, direct interaction, and a built-in agent, and Intent-Level Interaction Abstraction (IIA) as the task semantics through which users inspect and control delegated work. An open transition-system model relates AIS execution to IIA states and events. Interaction contracts constrain this relation through task bindings, role-specific authority, control transitions, and outcome evidence; continuous assurance maintains scoped claims as their dependencies change. A compact disclosure contract and conditional propositions illustrate why local component validity is insufficient and how selected admission invariants can be separated from planning. Contrasting software domains expose the framework's assumptions and limits. This perspective develops a research agenda spanning application abstraction, development support, controlled execution, quality assessment, and human supervision, with the aim of making agent integration a maintainable software engineering discipline.

arXiv abstract · PDF

Program Verification and Reactive Systems · cs.SE candidate · published 2026-09-10T17:58:48Z
Alexander Krentsel, Shubham Agarwal, Mert Cemri, Shu Liu, Sidharth Sankhe, Ziming Mao, Matei Zaharia, Ion Stoica
arXiv categories: cs.SE, cs.AI

Software development follows an implementation-verification loop in which developers or agents iteratively revise an implementation until an evaluator, such as a test suite, accepts it. The evaluator checks the implementation against a set of requirements under a model of the deployment environment. Yet even a formal proof that the implementation satisfies the requirements under the model cannot guarantee acceptable behavior after deployment. Requirements only approximate stakeholder intent, and the model only approximates the real deployment environment. We call these together - requirement gap and model gap - the two-gap framework, which unifies the main failure modes of agentic software engineer-ing: reward hacking exploits omissions in the requirements or model, while hallucination widens the gaps by fabricating requirements or environment assumptions. Because neither gap can generally be certified closed in an open, changing world, the goal shifts from closing them to continuously narrowing them. We therefore propose an assurance-revision loop that uses deployment evidence to revise the requirements, model, or evaluator when stakeholders reject the resulting behavior. We then cast assured agentic development as a resource-allocation problem over human judgment, agent capability, and compute. The two principal bottlenecks mirror the two gaps: human judgment for the requirement gap and faithful, costly evaluation for the model gap. Reality remains the final verifier: acceptable behavior under actual deployment conditions is the ultimate test, while predeployment evaluations remain proxies for it.

arXiv abstract · PDF

Program Verification and Reactive Systems · primary corpus · published 2026-09-10T21:42:14Z
Tiberiu-Andrei Georgescu, Dalal Alrajeh, Sebastian Uchitel
arXiv categories: cs.SE, cs.AI, cs.LO

Reactive synthesis is a powerful tool for generating correct-by-construction controllers from formal specifications. GR(1) is an assume-guarantee specification framework that enables efficient synthesis, allowing synthesised controllers to be used in a wide array of applications. The limitation of such controllers is that, should they encounter environment behaviour unspecified in the assumptions of the specification, the specified system guarantees are no longer ensured. Our work proposes an approach based on oracle-guided inductive synthesis to adapt the specification to be consistent with the observed assumption violation, while degrading system guarantees as little as possible to maintain realisability. Our methodology discovers multiple potential solutions, so we propose a preference criteria, based on the ability of the specification to enable robustness under adaptation. Although our approach is capable of degrading the entire specification, for our case studies we successfully discover degradations that preserve the entire set of original guarantees.

arXiv abstract · PDF

Program Verification and Reactive Systems · primary corpus · published 2026-09-11T18:09:38Z
Syyeda Zainab Fatmi, Stefan Kiefer, James C. A. Main, David Parker
arXiv categories: cs.LO, cs.FL

Behavioural equivalences, such as language equivalence and probabilistic bisimilarity, are fundamental techniques for reducing the size of probabilistic models. However, these equivalences are sensitive to the precise values of transition probabilities, making them unsuitable in applications where probabilities are subject to approximation. Motivated by settings in which the support graph of a labelled Markov chain is known but the transition probabilities are uncertain, we study robust variants of these equivalences. We introduce universal (perturbation) equivalence, which captures a variant of equivalence that is resilient to all perturbations of transition probabilities: two states or distributions are universally equivalent if they remain equivalent under every assignment of transition probabilities consistent with the support graph. We also consider the dual notion of existential (perturbation) equivalence, which holds whenever there exists an assignment of transition probabilities that yields equivalence. We establish that, for states, universal language equivalence coincides with universal probabilistic bisimilarity and develop a characterisation that yields a polynomial-time partition refinement algorithm. We implement the algorithm and demonstrate experimentally that it is effective as a technique for robust model reduction. We further show that universal language equivalence for distributions is closely related to the state case, and prove NL-completeness of deciding universal equivalence for both states and distributions. We prove that, for states, existential language equivalence coincides with existential probabilistic bisimilarity and deterministic witness transition functions always suffice, leading to an NP-completeness result. In contrast, we show that existential language equivalence for distributions is complete for the existential theory of the reals.

arXiv abstract · PDF

Program Verification and Reactive Systems · primary corpus · published 2026-09-12T13:24:44Z
Letterio Galletta
arXiv categories: cs.CR, cs.PL

Many attacks against workloads running on multi-tenant systems are multi-step and history-dependent: sequences of innocuous operations whose malicious nature emerges only over an execution trace. Defending against them requires security policies that are stateful, are enforced within the kernel, and have a precise semantics. Currently deployed proposals fail on at least one count: kernel's built-in syscall filtering and classical MAC frameworks are stateless, while current eBPF-based tools express their policies through ad hoc YAML rules that cannot capture temporal relations among events, and whose semantics is defined only by the implementation. We present BPFence, an in-kernel runtime-verification framework that satisfies the properties above. BPFence provides a policy language with a formal semantics that can express temporal relations among events. It also provides a type system that statically distinguishes events the kernel can control from those it can only observe. Every well-typed policy is compiled into a finite-state monitor proved correct with respect to its semantics, and then into eBPF programs that run inside the kernel. We evaluate BPFence on seven case studies drawn from real-world attack patterns, and on a set of micro- and macro-benchmarks to show that the enforcement overhead remains compatible with production deployment.

arXiv abstract · PDF

Programming Languages and Software Systems · primary corpus · published 2026-09-07T15:53:47Z
Stefano Raviola, Paola Giannini, Francesco Dagnino
arXiv categories: cs.PL

We present a concrete implementation in Haskell of a monadic framework that includes both a small-step interpreter and a type-and-effect checker for the corresponding language. Our approach separates the language syntax from the semantics of its effects. This design allows the interpreter to remain parametric over the underlying monad, while the static checker approximates effects independently of their concrete implementation. The theoretical foundation of this framework-applied to a call-by-value lambda calculus with generic effects represented by operations that produce monadic values and are managed through handlers-was introduced in previous work, where the focus was on proving the soundness of the approach. In contrast, the present work leverages Haskell's support for modular programming and monads to demonstrate that the framework is practically implementable and usable. We illustrate the approach with examples using the monad of exceptions and the one of nondeterminism and expressions both with and without handlers.

arXiv abstract · PDF

Programming Languages and Software Systems · primary corpus · published 2026-09-07T18:56:03Z
Antonios Kalampakas
arXiv categories: cs.LO, cs.FL

Finite automata can describe relations of unbounded arity that are exponentially larger than their descriptions. We prove that constraint satisfaction for such relations is solvable in polynomial time whenever their length slices are preserved by a common fixed edge operation on a finite domain. The algorithm computes compact representations of the complete solution relation and its projections. Its main ingredient is a polynomial-time compilation of nondeterministic finite automata into the fork witnesses and small projections required by the few-subpowers algorithm. In the Mal'tsev case, a direct proof is polynomial also when the domain and operation table are supplied as input, answering the Mal'tsev tractability question for automatic constraint satisfaction. We also characterize all invariant relations of a family of 3-edge algebras with neither Mal'tsev nor near-unanimity terms. Their normal forms combine Boolean activity constraints with affine value spaces and yield canonical quadratic-bit representations constructible from NFAs or arbitrary generators. For graphoid automata, these results give polynomial-time recognition without a graph-width restriction, effective boundary composition, and comparison of finite graph relations. The quadratic boundary bounds are optimal in the worst case. A fixed three-state example separates polynomial-time recognition from hard exact counting.

arXiv abstract · PDF

Programming Languages and Software Systems · primary corpus · published 2026-09-08T06:52:14Z
Antonios Kalampakas
arXiv categories: cs.LO

Completeness of an equational presentation guarantees an equality path but need not control the resources used along it. For finite graph expressions we measure derivational space by the largest input-output interface of an intermediate raw term. For every finite doubly ranked edge alphabet $\Sigma$, we prove that equal closed expressions of pattern width at most $k$ are joined by a derivation in which every step applies an equation in either direction and every intermediate width is at most a computable $B_\Sigma(k)$, independently of graph size. The derivation uses only the structural magmoid laws and the fifteen finite-graphoid schemes. The construction compiles each expression through protected cores and finite routing windows to an encoding-canonical representative $\operatorname{NF}_k$ of width at most $4k+4$. We call this property bounded equational coherence. We also prove $\operatorname{bw}(F)\le\operatorname{patw}(F)\le4(\operatorname{tw}(F)+1)$ whenever the underlying simple graph has at least two edges, separate layered linear from branching expressions on cliques, and provide machine-checkable witnesses and finite invariants for the first five nontrivial clique values.

arXiv abstract · PDF

Programming Languages and Software Systems · primary corpus · published 2026-09-08T15:03:57Z
Georg Zetzsche, Hongjian Jiang, Andy Yang, Pascal Bergstr\"a{\ss}er, Marco S\"alzer, David Chiang, Anthony W. Lin
arXiv categories: cs.LG, cs.FL, cs.LO

Recent advancements in transformer length generalization theory enable us to reliably predict when a transformer can learn to solve a task. In particular, the C-RASP hypothesis (a formalized version of the so-called RASP-l conjecture) posits that transformers length-generalize on a task if and only if a solution is expressible in the C-RASP language. While this hypothesis has strong empirical validation, theoretical problems arise from the fact that no computable length generalization bounds exist for C-RASP, alongside the discovery of seemingly contradictory experiments. To address these problems, we refine the C-RASP hypothesis utilizing the recently-proposed fragments C-RASP+ and C-RASP1. These fragments have computable length generalization bounds, though in the worst case requiring an extremely large (double exponential) sample size. It is an open question whether these sample size bounds are tight. In this paper, we resolve this open question by providing an exponentially tighter bound. In doing so, we show a polynomial length generalization bound for transformers if we adopt compressed strings, via a novel connection to power words. As an application, we show how this yields a fine-grained analysis of the C-RASP conjecture that resolves contradicting experimental evidence against it.

arXiv abstract · PDF

Programming Languages and Software Systems · primary corpus · published 2026-09-10T02:20:53Z
Joshua Horowitz, Jeffrey Heer
arXiv categories: cs.HC, cs.PL

Live programming provides visibility to programmers by running and tracing programs as they are edited. However, for programs with potentially harmful side effects, liveness can turn mistakes into disasters. We propose enabling live programming in environments with side effects via sandboxing: confining effects to a simulation of the true environment. We apply sandboxed live programming in the challenging context of shell scripting: a ubiquitous and powerful---yet notoriously opaque and error-prone---tool. ShellVis provides line-by-line feedback on a shell script's run-time behavior, with file operations sandboxed via a safe overlay of the file system. A qualitative user evaluation finds ShellVis to be helpful to participants, replacing tedious existing practices and instilling confidence. Participant responses also reveal areas for future research, particularly bridging the gulf of execution alongside the gulf of evaluation. ShellVis serves as a case study of how sandboxing can bring live-programming techniques into the many real-world programming contexts where side effects are important.

arXiv abstract · PDF

Programming Languages and Software Systems · primary corpus · published 2026-09-10T10:39:21Z
Ziteng Yang, Nicholas J. Riasanovsky, Warren Deng, Vivek Sarkar
arXiv categories: cs.DC, cs.PF, cs.PL

Determinism and numerical reproducibility are increasingly required of GPU kernels in machine learning systems, yet deterministic implementations of the same kernel can still differ bit for bit. Floating-point reduction order is the primary cause, alongside partial-sum precision, fused multiply-add operations, and rounding placement. These choices may be hand-coded, selected by a block-level language such as Triton, or hidden inside a closed-source library such as cuBLAS or rocBLAS. A tile shape chosen for performance therefore also determines the arithmetic, potentially breaking batch invariance. Preserving a fixed order can cost up to 20 percent, while an autotuner cannot identify which configurations are bitwise equivalent. We characterize the factors determining the bitwise behavior of reductions and general matrix multiplication (GEMM). First, we introduce a descriptor of GEMM reduction order, including the partitioning of K in split-K GEMM. Using it, we perform the first black-box reconstruction of a closed-source library's arithmetic for bit-level correctness. Our family of Triton GEMMs matches NVIDIA cuBLAS in all tested cases on Blackwell and Hopper. For realistic LLM shapes with fused epilogues, it matches or exceeds torch.compile performance. Second, we enforce balanced-tree reduction during Triton lowering and introduce a data-layout optimization that brings 19 of 27 kernels on GB300 and H100 within 10 percent of free-order performance. Third, we develop sound static checkers for bitwise equivalence between compiled GPU kernels, including the first checker spanning NVIDIA PTX and AMD GCN. Integrated into Triton's autotuner, the checker restricts search to a single bit-equivalence class.

arXiv abstract · PDF

Programming Languages and Software Systems · primary corpus · published 2026-09-10T15:45:23Z
Samuel Moussa, Steven Ibrahim, Ahmad Sudky, Ahmad Fawzy, Abanoub Nabil, Alhassan Sayed, Hossam Hassan, Hyung-Min Yoon
arXiv categories: cs.AR, cs.PL

Open-source RISC-V GPGPUs such as Vortex ship with directed-kernel regressions but no reference-model checking, functional-coverage model, or sign-off discipline. This paper presents a UVM 1.2 environment and methodology that closes that gap. The environment wraps a bus-master SIMT DUT with role-inverted agents, integrates Vortex's functional simulator (SimX) as a per-configuration golden model over DPI-C, and renders verdicts via two injection-qualified checkers: a bidirectional end-state scoreboard and a per-instruction, per-lane lockstep comparator under five SIMT alignment rules. A two-pass load-value feed makes racy fenceless multi-core programs instruction-granularity verifiable (residual zero over 5,432 retirements), with the interrupt-timing boundary stated. A three-layer coverage model adds, to our knowledge, the first published SIMT functional-coverage layer for RTL GPU verification (divergence depth, bank conflicts, coalescing classes), closing its own layers at 98.1% covergroup-bin / 94.7% total (ISA layer separately: 83.1% bins / 89.3% weighted) under machine-generated, RTL-cited exclusions and a blocking waiver-integrity gate; an unstimulated D-extension elaboration affects no functional bin, only lowering totals. The checking depth surfaced real defects on both sides of the comparison: a JALR LSB ISA deviation, a non-scaling watchdog constant (since fixed upstream), a reset-relay X window found by restoring a silenced assertion, a missing AXI error path proven by fault injection, and a reference-model fetch bug found by the lockstep itself. FuzzGPU (USENIX Security 2026), a concurrent RTL GPU fuzzer on the same DUT, is complementary: fuzzing finds bugs, this methodology quantifies sign-off; both independently found the JALR deviation. All findings ship in an evidence-cited register; every number carries provenance and the method's boundaries are stated rather than waived.

arXiv abstract · PDF

Programming Languages and Software Systems · primary corpus · published 2026-09-10T17:51:54Z
Riccardo Romanello, Andrea Esposito, Marco Bernardo, Carla Piazza, Sabina Rossi
arXiv categories: cs.LO

We study the relationships among the stochastic bisimulation-style equivalences over PEPA - Performance Evaluation Process Algebra definable according to the well known notions of lumpability for the continuous-time Markov chains (CTMCs) underlying process terms. Lumpability is a central tool in the analysis of a CTMC, because it results in aggregations of the state space enjoying properties that are useful for efficiently computing the state probability distribution of the original chain. At the level of process terms, various stochastic bisimilarities accounting for activity types and cumulative rates can be defined over PEPA, which induce different kinds of lumping. Since the formalisations of some of them are scattered across the literature, where they appear under different, and sometimes clashing, names, we collect them within a single, uniform framework, renaming each bisimilarity in a consistent way after the kind of lumping it induces. We present strong and weak variants of what we call ordinary, exact, and strict bisimilarities and show that they respectively induce ordinary, exact, and strict lumpings. We then organise the six bisimilarities into a taxonomy establishing all and only the inclusions holding among them. We also analyse how the taxonomy changes in three special cases: process terms whose underlying CTMCs are time reversible, process terms with no activities of unobservable types, and process terms with no recursion. The paper concludes by investigating the compositionality properties of the six bisimilarities. Some of them are not congruences with respect to the prefix and/or choice operators of PEPA. In that case we single out either a set of process terms over which congruence with respect to those operators is achieved, or the coarsest congruence with respect to them that is contained in the considered bisimilarity.

arXiv abstract · PDF

Programming Languages and Software Systems · primary corpus · published 2026-09-10T17:58:14Z
Boning Li, Longbo Huang
arXiv categories: cs.DC, cs.AI, cs.GT, cs.MS, cs.PL

Counterfactual regret minimization (CFR) is one of the few large numerical workloads that still runs faster on CPUs than on GPUs. Each iteration sweeps a game tree with up to billions of states in millions of small, interdependent gather and scatter steps issued through a generic tree interface. On a GPU every kernel finishes in microseconds, so kernel launches and framework dispatch dominate the run time, and prior GPU implementations have lost to optimized CPU code. We observe that for a fixed game, everything about a CFR iteration except the numerical values is known before the first iteration runs. We propose GPU-CFR, a compiler and runtime built on this observation. It compiles any game once into static dataflow: flat edge and information-set arrays, precomputed indices, and depth-level batched passes fix the entire operation sequence, and only solver state changes between iterations. Static chance folding, depth-level execution blocks, and a dual-lane reach buffer cut the number of framework operations by up to 18.1x. Because shapes, indices, and buffer addresses never change, CUDA Graph Replay records the iteration once and replays it with a single graph launch. On one A100, across an eight-game suite that spans card games, dice games, and board games, GPU-CFR runs 29.8--80.4x faster than the fastest prior GPU CFR on the same accelerator, and 14--258x faster than LiteEFG, one of the fastest open-source CPU implementations, on the four largest games. The compiled representation carries most of that margin: on eight CPU threads with no accelerator it is already 2.2--51.1x faster than the GPU baseline. On the CPU the optimized path reproduces the reference iterates bitwise, and tree construction and graph capture pay for themselves within the first solve. GPU-CFR beats every CPU and GPU baseline on the mid-to-large games of the suite without changing the update rule.

arXiv abstract · PDF

Programming Languages and Software Systems · primary corpus · published 2026-09-11T11:10:49Z
Kaushik Mallik, {\DH}or{\dj}e \v{Z}ikeli\'c
arXiv categories: cs.LO, cs.AI, cs.SY, eess.SY

We consider the problems of formal verification and synthesis in parametric Markov decision processes (MDPs) with general measurable state and action spaces. The heart of our approach is a parameter flattening transformation, which allows us to transform parametric MDPs into semantically equivalent non-parametric MDPs. Building on this transformation, we introduce the novel notion of parametric supermartingale certificates, which generalize the traditional supermartingale certificates---used for non-parametric MDPs---to the parametric setting. We use our parametric supermartingale certificates to design algorithms for verification and approximate synthesis in polynomial arithmetic parametric MDPs. This leads to the first verification and synthesis algorithms for parametric MDPs with general state and action spaces. We implement our algorithms and experimentally evaluate them on several continuous parametric random walk benchmarks.

arXiv abstract · PDF

Programming Languages and Software Systems · primary corpus · published 2026-09-11T22:31:02Z
Oleg Grynets, Olena Pochernina, Alona Seletska, Daryna Tukalo, Dmytro Kostetskyi, Ivan Fedorchuk, Vasyl Lyashkevych
arXiv categories: cs.SE, cs.LO, cs.MA

This study compares framework suitability across three classes of enterprise generative AI applications: a documentation-based development assistant, an email and inquiry automation system, and an Oracle-to-PostgreSQL migration tool. The analysis evaluates component boundaries, orchestration, policy retrieval or reasoning, model integration, deterministic validation, persistence, observability, and operational efficiency. Across the three applications, the evidence supports layered architectures in which probabilistic components generate proposals, while deterministic components retain authority over routing, authorization, validation, persistence, idempotency, and final outcomes. The results indicate that framework suitability depends on the application, deployment conditions, and component responsibility: search quality, workflow control, safety behavior, and migration validation cannot be reduced to a single cross-application assessment. Therefore, the study substantiates the need for framework selection at the component level, supported by explicit contracts, application-specific evidence, and independent validation boundaries.

arXiv abstract · PDF

Programming Languages and Software Systems · primary corpus · published 2026-09-12T13:24:41Z
Oleg Grynets, Olena Pochernina, Vasyl Lyashkevych
arXiv categories: cs.LO, cs.DB, cs.SE

Legacy database migrations often begin with incomplete or outdated documentation, leaving physical data definition language (DDL) as the principal evidence of data architecture. However, DDL does not fully encode conceptual intent, and model-generated completions can be plausible without being correct. This study proposes and evaluates a provenance-aware, deterministic-first pipeline for reconstructing logical and conceptual data specifications from Oracle-oriented DDL while explicitly separating observed facts, deterministic derivations, and large language model (LLM) suggestions. The pipeline performs DDL investigation, parsing, consolidation, primary-key backfilling, type normalization, and declared relationship-graph construction before optional LLM-assisted enrichment. It preserves source provenance in the deterministic catalog and declared relationship graph, and records inferred primary-key and foreign-key candidates in a separate reviewable overlay. We evaluated the implementation on 249 artifactized schema samples comprising 1,225 SQL files. The pipeline completed 244 samples (97.99%); 52 completed samples contained no extractable DDL. Across completed samples, the deterministic path reconstructed 208 tables and recovered 278 declared foreign-key records; 168 of the reconstructed tables lacked an explicitly parsed primary key before backfilling. LLM enrichment generated 100 foreign-key candidates in 36 samples, but the parent-table admissibility rate was only 17.9% for logical-specification candidates and 17.5% for conceptual-specification candidates. These findings show that the proposed deterministic-first architecture can preserve an auditable structural baseline, quantify observed primary-key and relationship gaps, and prevent model-generated hypotheses from being silently promoted to source-grounded architectural facts.

arXiv abstract · PDF

Programming Languages and Software Systems · primary corpus · published 2026-09-12T16:49:58Z
Georgios Alexopoulos, Konstantinos Karakatsanis, Nikolaos Alexopoulos, Dimitris Mitropoulos, Thodoris Sotiropoulos
arXiv categories: cs.DC, cs.PL, cs.SE

We present PyXtrim, a system that reduces the cold-start latency of serverless applications through debloating. We focus on Python, a dominant language for serverless applications whose dynamic features and extensive use of native extensions make traditional static debloating particularly challenging. PyXtrim frames debloating as a dynamic slicing problem, using the application's externally visible behavior as the slicing criterion. Everything outside the resulting slice is removed, both from the application and its dependencies. Our key technical contribution is that the slice is computed by a cross-language dynamic dependence engine that tracks data and control dependences across Python and native code and identifies operations that interact with the operating system, which form the slicing criterion. As a result, PyXtrim can effectively handle real-world applications that rely on dynamic features such as reflection, interoperate with native code and interact with system resources. Across 31 applications on AWS Lambda, PyXtrim reduces cold-start latency by 21.7% and peak memory usage by 17.1% at the median. This is more than double the reduction achieved by the state of the art, while debloating each application in minutes.

arXiv abstract · PDF

Programming Languages and Software Systems · primary corpus · published 2026-09-13T10:22:05Z
Oleg Grynets, Oleg Kaskun, Alona Seletska, Daryna Tukalo, Vasyl Lyashkevych
arXiv categories: cs.LO, cs.AI, cs.MA, cs.SE

Large language model (LLM)-based database migration is often treated as direct code transformation, although enterprise Oracle systems contain heterogeneous SQL and PL/SQL artifacts with different dependencies, execution order, complexity, and validation needs. This paper proposes a hybrid dependency-aware framework that identifies migration tasks, builds a cross-file dependency graph, condenses cyclic dependencies, and uses task specifications to generate specialized migration agents at runtime. The deterministic path combines ANTLR-based parsing with typed dependency extraction, while an LLM fallback is invoked only for units that cannot be parsed reliably. On a corpus of 116 Oracle files, the pipeline produced 1,037 units with zero coverage gaps and 1,271 AST-derived dependencies. The fallback processed 165 parse-error units, recovered 496 additional validated dependencies, eliminated unresolved-dependency units, and increased resolved internal edges from 446 to 527. The graph contained four dependency-respecting phases, while cycle handling was validated separately using Tarjan SCC condensation. A complementary experiment on 1,006 PL/SQL files regenerated 623 scripts (~62%), of which 380 (~61%) executed successfully in PostgreSQL 16. Tables achieved about 85% regeneration success, whereas no query regenerations succeeded under the evaluated specification-mediated baseline, and procedural objects remained strongly dependent on schema context. These results motivate dependency-aware context delivery, task-specific validation, and differentiated agent routing. The paper also formalizes task-to-agent mapping, introduces monitoring and diagnostics for execution feedback, and defines a controlled comparison of monolithic, static-decomposition, dependency-aware, and dynamically orchestrated migration strategies.

arXiv abstract · PDF

Programming Languages and Software Systems · primary corpus · published 2026-09-13T14:06:39Z
Anjali Pal, Brett Saiki, Ryan Tjoa, Cynthia Richey, Amy Zhu, Oliver Flatt, Max Willsey, Zachary Tatlock, Chandrakana Nandi
arXiv categories: cs.PL

Rewrite rules are critical in equality saturation, an increasingly popular technique in optimizing compilers, synthesizers, and verifiers. Unfortunately, developing high-quality rulesets is difficult and error-prone. Recent work to automatically infer rewrite rules does not scale to large terms or grammars. Users struggle to guide inference and incrementally construct rulesets because existing rule inference tools are monolithic and opaque. As a result, most equality saturation users still manually develop and maintain rulesets. This paper proposes Enumo, a new domain-specific language for programmable theory exploration. Enumo provides a small set of core operators that enable users to strategically guide rule inference and incrementally build rulesets. Short Enumo programs easily replicate results from state-of-the-art tools like Ruler, but Enumo programs can also scale to infer deeper rules from larger grammars than prior approaches. Enumo's composable operators even facilitate developing new strategies for ruleset inference. We introduce a new fast-forwarding strategy which does not require evaluating terms in the target language, and thus supports domains that were out of scope for prior work. Enumo is also easy to extend: two new operators suffice to incorporate large language models into rule inference, where they complement guided search. We evaluate Enumo and fast-forwarding across a variety of domains. Compared to state-of-the-art techniques, Enumo can synthesize better rulesets over a diverse set of domains, in some cases matching the effects of manually developed rulesets in systems driven by equality saturation.

arXiv abstract · PDF

Quantum Computing · primary corpus · published 2026-09-08T00:37:42Z
Marouane Benbetka, Merwan Bekkar, Bokyeong Yoon, Riyadh Baghdadi, Martin Kong
arXiv categories: cs.PL

Qubit mapping is a critical pass in quantum compilation. Despite various advances, dynamic circuits, those exhibiting data dependent control-flow, often resulting from qubit measurements, are not yet supported by the vast majority of available qubit mappers. The crucial limitation to overcome is the dependence on flat, one-dimensional representations of circuits. Further, qubit mappers currently lack compiler abstractions that capture the hierarchical nature of circuits, hindering the qubit mapping process. In this paper, 1 we introduce a new qubit mapping method and analyses to tackle hierarchical dynamic circuits. Our novelty resides in four key aspects: modeling (statically) sub-circuits in disjoint control-flow paths, introducing a novel Qubit Reconciliation pass to maintain consistency between sub-circuit and control-flow boundaries, a loop-entry remapping pass, and a refined cost function enhanced for SWAP count, circuit depth, circuit latency and error. We demonstrate the efficiency of our approach on a wide range of dynamic circuits on two monolithic Quantum Processing Units of 127 and 156 qubits, and on chiplet hexagon-based QPUs. On monolithic QPUs, our qubit mapper improves the SWAP count by up to 52%, depth by up to 18%, latency by up to 18.6%, and error by up to 40%. On chiplet architectures, we achieve improvements of up to 36% on SWAP count, 8.7% on depth, 15% on latency, and 15% of error.

arXiv abstract · PDF

Quantum Computing · primary corpus · published 2026-09-08T13:17:16Z
Mark Carney
arXiv categories: quant-ph, math.CT

This paper gives a categorical interpretation of Baumeler \& Wolf's logically consistent non-causal circuits, connecting them to postselected quantum teleportation. Looped feedback is represented by a trace in the category of non-negative matrices, and it is shown that the traced process is stochastic precisely when the induced loop transition matrix has trace $1$ for every external input, a condition shown to be equivalent to a unique fixed point for the loop for each input to a deterministic circuit. A classical non-causal circuit is represented by a measure-and-prepare quantum channel with an internal register utilising a maximally entangled Bell-state with postselection. The main result is that classical logical consistency is equivalent to the postselected Bell outcome having, for loop dimension $d$, probability exactly $1/d^2$ for each classical input distribution. The subsequent normalised conditional output then agrees exactly with the classical categorical trace. This work identifies a class of quantum Bell-postselection constructions whose conditional evolution maintains linear dependence on classical input distributions.

arXiv abstract · PDF

Quantum Computing · primary corpus · published 2026-09-08T18:00:00Z
Joseph K. L. Lee, Mehrdad Malekmohammadi, Hong-Sheng Zheng, Shuli Shu, Cheick Doumbia, Kalman Szenes, Mehran Zamani Abnili, Thomas Ainsworth, Matthew Seymour, Thomas Germain, Leonhard Neuhaus, Josh Izaac, Lee J. O'Riordan
arXiv categories: quant-ph, cs.DC, cs.PL

Moving from quantum research and development to production-grade, fault-tolerant quantum workload execution remains one of the most significant challenges facing quantum platform builders. While Python frameworks have enabled an easy entry point for quantum algorithm design, the low-latency requirements for real-time quantum error correction (QEC) demand performance that traditional interpreted environments cannot provide. FPGAs and ASICs play a central role at these layers, but their specialized programming models make development rigid and time-consuming. CPUs, GPUs, and other accelerators introduce a different challenge: as infrastructure becomes increasingly heterogeneous, programming across different devices and their associated abstractions becomes more complex. Allowing researchers to write workloads in high-level languages that map to low-latency execution across diverse distributed target platforms will enable the development of key infrastructure for utility-scale quantum systems. For this, we introduce $\textit{Backline}$, a heterogeneous compilation and runtime framework built within PennyLane and Catalyst. Backline allows us to design and build quantum-classical workloads for high-performance and low-latency devices, with compilation directly from a Python interface through MLIR. We demonstrate the compilation and execution of several quantum workloads with low-latency data movement across a mix of CPUs, GPUs, and FPGAs, for both local and distributed remote hardware targets, all from a vendor-agnostic Python frontend. With an AMD VPK120 FPGA board as the controller, issuing each round from its hardware-handshake engine, we measured median steady-state round-trip latencies over RoCE v2 of $2.305~\mu$s to an AMD Ryzen Threadripper PRO CPU and $4.5~\mu$s to an AMD Instinct MI210 GPU across $10^6-1$ rounds per path, demonstrating microsecond-scale synchronous co-processing.

arXiv abstract · PDF

Quantum Computing · primary corpus · published 2026-09-10T12:38:27Z
Zeyu Chen
arXiv categories: cs.LO, quant-ph

Hard symmetry constraints reduce model complexity, but can also erase label information. Statistical symmetry release determines when finite data and quantum measurements justify relaxing such a constraint, which directions to open, and how far to move. We connect global signal detection to local, loss-dependent improvement. A two-copy twirl--swap gate estimates task information in the symmetry-breaking complement with a dimension-independent copy count under paired-state and group-unitary access; reweighting the same records resolves representation sectors. An exact duality distinguishes this Hilbert--Schmidt signal from the larger signal accessible to bounded-outcome readouts. Local improvement is governed by the release gradient and a loss-corrected double-commutator matrix. Simultaneous confidence bounds convert empirical direction selection into certified descent, using either shared Pauli measurements or scalar probes with state-independent truncation bounds. Gaussian testing lower bounds quantify the cost of searching over unknown directions in the calibrated local experiment. Independent validation controls adaptively generated models, and a fast squared-loss bound preserves the approximation--estimation rate of a nested release path. On an eight-qubit Ising model, shared measurements certify release with 6300 times fewer shots than the specified scalar estimator on the tested budget grids. Quotient quantum natural gradient then controls parameter redundancy during training. Together, these results turn symmetry relaxation into a statistically justified model-selection decision.

arXiv abstract · PDF

Quantum Computing · primary corpus · published 2026-09-13T16:04:54Z
Lorenzo Ciardo
arXiv categories: quant-ph, cs.CC, cs.LO, math.CO, math.OA

We prove that the quantum monad in dimension $2n$ admits no natural transformation to the polymorphism clone of linear equations modulo $n$. Consequently, for every $n\geq 2$, there exists an unsatisfiable system of linear equations over $\mathbb{Z}_n$ whose constraint system game admits a perfect finite-dimensional quantum strategy. As a corollary, we completely characterise pseudo-telepathic constraint languages in finite dimension. The proof combines a result of Harding, Jager, and Smith on group-valued measures on subspaces of Hilbert spaces with the polymorphism-minion characterisation of quantum pseudo-telepathy.

arXiv abstract · PDF

Category Theory and Homological Algebra · primary corpus · published 2026-09-07T02:10:24Z
Keima Akasaka
arXiv categories: math.CT, math-ph, math.AT, math.MP

Building on the dagger Bergner and dagger Joyal models constructed in Part I, we develop simplicial-space models for dagger $(\infty,1)$-categories. We first construct a homotopically constant resolution model and a model structure for unitarily complete dagger Segal spaces. A change-of-index adjunction compares the two presentations of dagger simplicial spaces. We then prove a dagger analogue of the Joyal--Tierney Quillen equivalence. Together with Part I, these results give a chain of Quillen equivalences between the dagger Bergner, dagger Joyal, and dagger Rezk models.

arXiv abstract · PDF

Category Theory and Homological Algebra · primary corpus · published 2026-09-07T14:06:30Z
V\'ictor Becerril, Marco A. P\'erez
arXiv categories: math.CT

We explore some methods to obtain cotorsion pairs and model category structures from a Frobenius pair. Specifically, we consider a type of Frobenius pair $(\mathcal{X},\omega)$ in an abelian category $\mathfrak{C}$ for which there exists a nonnegative integer $m$ such that every object in the right orthogonal complement $\mathcal{X}^{\perp_1}$ of $\mathcal{X}$ under $\text{Ext}^1_{\mathfrak{C}}(-,\sim)$ has a special $\omega^\wedge_m$-precover and a special $[\omega^\wedge_m]^{\perp_1}$-preenvelope, where $\omega^\wedge_m$ denotes the class of objects in $\mathfrak{C}$ with resolution dimension relative to $\omega$ at most $m$. The cotorsion pairs and model structures obtained from these Frobenius pairs will involve the classes $\mathcal{X}$, $\omega$, $\mathcal{X}^\wedge_m$, $\omega^\wedge_m$, and their orthogonal complements, in the description of its cofibrant, fibrant and trivial objects. As applications of our results, we obtain several cotorsion pairs and model structures related to relative and absolute Gorenstein homological dimensions.

arXiv abstract · PDF

Category Theory and Homological Algebra · primary corpus · published 2026-09-07T15:27:12Z
Azat M. Gainutdinov, Ingo Runkel, Bangxin Wang
arXiv categories: math.CT, math.GT, math.QA

For a crossed module $\chi: G \to H$, we introduce the notion of $\chi$-crossed braided (resp. ribbon) categories, where the categories are graded by group $G$ and carry an $H$-action. Our definition unifies and generalises several familiar notions: taking $\chi = id: G \to G$ with the conjugation action recovers $G$-crossed braided categories; taking $\chi: G \to \{*\}$ for abelian $G$ yields $G$-graded braided categories; taking $\chi: \{*\} \to G$ leads to braided categories equipped with a $G$-action. The equivalence relation between $\chi$-crossed braided categories is typically finer than that between $G$-crossed braided ones. We classify $\chi$-crossed braided structures on the category of $G$-graded vector spaces in terms of cohomological data, and give explicit examples for cyclic groups. Given a doubly central algebra with $G$- and $H$-actions in a braided monoidal category, we define a notion of twisted-local modules and show how they give rise to $\chi$-crossed braided categories. We furthermore give sufficient conditions so that these categories are additionally $\chi$-crossed ribbon or admit an orthogonal $G$-decomposition.

arXiv abstract · PDF

Category Theory and Homological Algebra · primary corpus · published 2026-09-08T09:33:30Z
Leonid Positselski
arXiv categories: math.AG, math.CT

Let $X$ be a quasi-compact, quasi-separated scheme that is not semi-separated. We present a locally cotorsion contraherent cosheaf on $X$ that does not have an admissible monomorphism into any locally injective locally contraherent cosheaf. The construction and proof follow the arguments of Slavik and Stovicek in arXiv:1902.05740. A complementary positive result, claiming that every $\mathbf W$-locally contraherent cosheaf on a Noetherian scheme $X$ of finite Krull dimension has an admissible monomorphism into a locally cotorsion $\mathbf W$-locally contraherent cosheaf, can be found in the preprint arXiv:2603.27732v5, Section 4.7.

arXiv abstract · PDF

Category Theory and Homological Algebra · primary corpus · published 2026-09-08T12:51:49Z
Ping He, Bo Le
arXiv categories: math.RT, math.CT

We give a new equivalent formulation of Verdier's octahedral axiom. An initial square in a pre-triangulated category determines an obstruction in a quotient of ordinary Hom groups. Its vanishing is equivalent to the existence of a good completion, and $\mathrm{TR4}$ is equivalent to this vanishing for the squares associated with composable morphisms. As a consequence, if two pre-triangulations have the same underlying additive category and one is triangulated, then the other satisfies $\mathrm{TR4}$ precisely when their relative inverse Heller comparison admits an exact lift along every short exact sequence in the Freyd category. As applications, we prove that the exotic pre-triangulated category of D\'iaz Cabrera--Muro is in fact a triangulated category over every algebraically closed field. We construct scalar families for type-$A_{3a-1}$ preprojective algebras over arbitrary fields and for a range of Dynkin preprojective algebras in characteristic two; in each family the zero parameter is the unique triangulated member. The local equations also yield separable descent, including canonical triangulations for non-modular equivariantizations and for the Markman--Mehrotra K3 deformation categories.

arXiv abstract · PDF

Category Theory and Homological Algebra · primary corpus · published 2026-09-08T14:01:19Z
Lucas Anderson, Ariel E. Rosenfield, Eric Yu
arXiv categories: math.CT

Toward modeling computational concurrency using the language of central idempotents in monoidal categories, we give an explicit construction of the pushout of strict symmetric monoidal categories with strong monoidal functors between them. We show that any braided strong monoidal functor strongly preserves central idempotents, and as a corollary, that the lattice of central idempotents of a symmetric monoidal category is isomorphic as a meet-semilattice to that of its strictification.

arXiv abstract · PDF

Category Theory and Homological Algebra · primary corpus · published 2026-09-08T17:12:24Z
Wilmer Leal, Benjamin Merlin Bumpus, Jana K. Nickel, Johan Garc\'ia, James Fairbanks, Warren Dixon
arXiv categories: cs.AI, cs.MA, cs.SY, eess.SY, math.CT

Modern science and engineering increasingly rely on time-varying data, yet the mathematical tools used to model temporal phenomena are often developed within separate disciplines, obscuring common principles and limiting the transfer of ideas across fields. This chapter presents the theory of narratives, an abstract framework for time-varying objects of any mathematical kind that supports both theoretical investigations and applications. To illustrate this perspective, the chapter develops three vignettes, each illustrating a different research direction. The first addresses a general concern: What information loss can occur when switching between different representations of temporal data? The second concerns structural and algorithmic approaches: How can we systematically decompose time-varying data into simple pieces and obtain invariants describing its structural complexity? The third is an application to control theory: How can we model multi-agent systems with switching communication topologies? More important than any individual vignette, the central message of this invitation is that a suitable abstract perspective can organize and guide research across remarkably diverse mathematical and scientific domains.

arXiv abstract · PDF

Category Theory and Homological Algebra · primary corpus · published 2026-09-09T12:44:51Z
Chiara Ascenzi
arXiv categories: math.RT, math.CO, math.CT

We study universal derived equivalences between diagram categories indexed by finite posets. Starting from a construction of Ladkani, we give an intrinsic criterion for determining when a finite poset admits a decomposition to which this construction can be applied. This leads to the notion of an admissible cut, formulated entirely in terms of the order structure of the poset. Our main result therefore provides a method for producing, from a given finite poset admitting such a cut, a new poset that is universally derived equivalent to it. The construction is reversible once the partition is retained, so that the original mixed order relations can be recovered from the transformed poset. As applications, we show that every finite poset of height at most one is universally derived equivalent to its opposite, give a criterion characterizing source-to-sink transformations at minimal elements, and recover the universal derived equivalence of all orientations of a finite tree through sequences of such local transformations. These results are also applied to persistence modules indexed by finite posets and to extensions obtained by adjoining further finite parameters.

arXiv abstract · PDF

Category Theory and Homological Algebra · primary corpus · published 2026-09-09T13:19:16Z
Fei Ren
arXiv categories: math.AG, math.CT

We prove a duality theorem for lax equalizers of stable $\infty$-categories, and we apply it to Frobenius and Cartier modules on a Noetherian $F$-finite scheme $X$ of characteristic $p$ with a unit dualizing complex. When $X$ has affine diagonal, comparison with the derived categories of coherent modules and passage to homotopy categories recovers Baudin's derived Hom duality. The duality of coherent modules exchanges the standard $t$-structure on one side with the perverse $t$-structure determined by the dualizing complex on the other. In particular, it identifies the abelian category of coherent Cartier modules with a perverse heart of coherent Frobenius modules, and conversely.

arXiv abstract · PDF

Category Theory and Homological Algebra · primary corpus · published 2026-09-09T16:32:52Z
Noa Bihlmaier, Nick Ruoff
arXiv categories: math.DS, math.CO, math.CT

Originating in ergodic structure theory, nilspace theory is concerned with the study of cubical spaces. A first key result in this theory, the weak structure theorem, is the representation of a concrete fibrant compact cubespace as a tower of its canonical truncations, exhibiting each step over the previous one as a principal bundle by a compact abelian group. We present a categorical proof of the weak structure theorem by systematically interpreting the relevant concepts in an appropriate context.

arXiv abstract · PDF

Category Theory and Homological Algebra · primary corpus · published 2026-09-10T16:15:02Z
Cesar Bardomiano Martinez, Jana K. Nickel, Maru Sarazola, Daniel Teixeira, Santiago Toro Oquendo, Paula Verdugo
arXiv categories: math.CT, math.AT

Cartesian 2-fibrations provide a way to understand indexed categories, but their classical ``straightening'' construction requires several layers of weak coherence data. This paper develops a homotopical framework that replaces much of this bookkeeping with a fully strict model. By using marked 2-categories to record the cartesian morphisms and 2-cells, we construct a model structure whose fibrant objects are precisely the cartesian 2-fibrations over a fixed 2-category $\mathcal{C}$. We then show that the marked Grothendieck construction identifies these 2-fibrations, up to weak equivalence, with strict 2-functors from $\mathcal{C}$ into $2\mathrm{Cat}$. As an additional contribution, we construct localizations of 2-categories that simultaneously invert selected morphisms and 2-cells.

arXiv abstract · PDF

Category Theory and Homological Algebra · primary corpus · published 2026-09-11T16:26:50Z
Lucrezia Bottegoni, Davide Ferri, Paolo Saracco
arXiv categories: math.QA, math.CT

Evidence suggests a tight connection between the existence of antipode-like maps on bialgebra-like structures, and the Frobenius property for the associated free Hopf module functor. In this paper, we prove that in any braided monoidal category satisfying few mild assumptions, a bimonoid is a one-sided Hopf monoid and the antipode is a bimonoid anti-homomorphism, if and only if the free Hopf module functor is Frobenius. Our interest in these structures stems from having found genuine examples of one-sided Hopf monoids in contexts where the braiding is non-trivial. In fact, we provide a construction of the free one-sided Hopf monoid over a comonoid in any symmetric monoidal category with some non-restrictive additional assumptions. We present several examples of this construction, and describe the resulting one-sided (sometimes two-sided) Hopf monoids.

arXiv abstract · PDF

Category Theory and Homological Algebra · primary corpus · published 2026-09-12T04:18:43Z
Jiaojiao Lu, Zhongkui Liu, Renyu Zhao
arXiv categories: math.CT

Let $K$ be a field, and $\mathcal{T}$ a $K$-linear essentially small triangulated category equipped with an extendable $t$-structure $(\mathcal{T}^{\leq0}, \mathcal{T}^{\geq0})$ with respect to a good metric $\mathfrak{B}$. Given a torsion class $\mathcal{X}$ in the heart of $(\mathcal{T}^{\leq0}, \mathcal{T}^{\geq0})$, we prove that lifting the HRS-tilt of $(\mathcal{T}^{\leq0}, \mathcal{T}^{\geq0})$ at $\mathcal{X}$ along the completion of $\mathcal{T}$ coincides with the HRS-tilt of the lifted $t$-structure at the completion of $\mathcal{X}$. As an application, we provide the compatibility result between left silting mutation in $\mathcal{T}$ and HRS tilting in the ambient completion.

arXiv abstract · PDF

Category Theory and Homological Algebra · primary corpus · published 2026-09-12T08:03:24Z
Tessa Kammermeier
arXiv categories: math.CT

In recent years, higher categorical variants of idempotents have become an object of interest. Notably, they appear when categorifying algebraic structures motivated by mathematical physics. Working in the setting of bicategories, we give a rigorous definition of the bicategorical idempotent completion as outlined by Gaiotto and Johnson-Freyd in arXiv:1905.09566. We show that this agrees with the Cauchy completion of a locally idempotent complete bicategory in the sense of Lawvere.

arXiv abstract · PDF

Category Theory and Homological Algebra · primary corpus · published 2026-09-12T08:45:43Z
Hongliang Lai, Bo Pang
arXiv categories: math.CT

Let $Q$ be a commutative unital quantale and $\QRel$ the ordered category of sets and $Q$-relations. We develop a categorical foundation for formal and property-oriented concept lattices of $Q$-relations via the diagonal category $\DQRel$ and back-diagonal category $\BQRel$. Our main results are: (1) the formal concept lattice construction is induced by a representable functor on $\BQRel$; (2) the property-oriented concept lattice construction corresponds to a representable functor on $\DQRel$; and (3) for regular $Q$-relations, the property-oriented concept lattice of their pointwise tensor product is naturally isomorphic to the tensor product of the respective property-oriented concept lattices.

arXiv abstract · PDF

Algebraic Structures and Higher Categories · primary corpus · published 2026-09-08T12:49:46Z
Xiaojin Zhang, Panyue Zhou
arXiv categories: math.RT, math.CT

Let $A$ be a split finite-dimensional algebra over a field whose radical $J$ satisfies $J^3=0$, and let $s$ be the number of isomorphism classes of simple $A$-modules. We prove that a non-projective module $M$ with ${\rm Ext}_A^i(M,A)=0$ for all $i>0$ has a non-zero self-extension in some degree between $1$ and $3s+1$. In particular, $A$ satisfies the Auslander--Reiten conjecture, which asserts that every self-orthogonal generator is projective. As a consequence, every finite-dimensional algebra over an algebraically closed field with radical cube zero satisfies the Auslander-Reiten conjecture.

arXiv abstract · PDF

Algebraic Structures and Higher Categories · primary corpus · published 2026-09-09T16:50:41Z
Tinhinane Amina Azzouz, Mainak Ghosh, Sebastien Palcoux
arXiv categories: math.QA, math.CT, math.OA, math.RT

We establish local Ocneanu rigidity for separable algebra objects in Hom-finite monoidal categories C over an algebraically closed field k. A separability morphism contracts the first two Hochschild cohomology groups without requiring an abelian ambient category. Separable algebra structures and homomorphisms from separable sources have open algebraic-group orbits, and affine Bezout estimates give effective finiteness results. For Frobenius subalgebras, exchange relations replace the source and embedding data by a single self-dual idempotent. We prove that their separable inner-conjugacy classes are open in the exchange locus, yielding a bound of 2^(dim_k End_C(X)) for nonzero ambient algebras; connectedness gives the same bound on the actual number of subalgebras. As an application, we obtain an effective form of the Etingof-Walton finiteness theorem: every finite-dimensional semisimple Hopf algebra H over the complex numbers has at most 2^(dim_C H) left coideal subalgebras. In the unitary setting, we bound E-compatible intermediates of C*-algebra and von Neumann algebra inclusions up to unitary conjugacy, under finite-index and finite-center hypotheses. For irreducible subfactors, these improve the 9^[M:N] bound of Bakshi-Das-Liu-Ren to 2^[M:N].

arXiv abstract · PDF

Algebraic Structures and Higher Categories · primary corpus · published 2026-09-09T17:36:02Z
Zurab Janelidze
arXiv categories: math.CT, math.CO

In this paper, we study certain categories of labeled finite rooted ordered trees over a fixed set of labels where each label is equipped with an arity: a fixed number of children that the vertex with the given label must have. Equivalently, these are expression trees for operations in a free non-symmetric operad. A morphism between these trees matches a pruning of one tree (a prefix) with an entire subtree of another (a suffix). We characterize such categories, up to isomorphism, in terms of suitable exactness properties. It turns out that these categories exhibit strong algebraic behavior, in the sense that every such category, when appended with a strict initial object, has a particularly nice noetherian form.

arXiv abstract · PDF

Algebraic Structures and Higher Categories · primary corpus · published 2026-09-09T23:45:44Z
Suddhasattwa Das, Tomoharu Suda
arXiv categories: math.CT

Dynamical systems theory primarily concerns the study of different forms of invariance, such as invariant sets, densities, measures, and observables. Ergodic systems are a special class of dynamical systems which are measure theoretically irreducible. In spite of this specialized property they dominate most discussions on ergodic theory because of the ergodic decomposition theorem. The viewpoint that any dynamical system is a composite of multiple ergodic components enables us to partition the face space into the basins of the different measures. The coexistence and mutual connections between these various coexisting subsystems are illuminated very effectively using the language of Category theory (CT). Some recent advancements have shown how the essence of measure theoretic dynamical systems can be captured through the formalism of Markov categories. This formalism captures the essential features of invariance and ergodicity through the language of limits and colimits. This article continues that formalism by studying the concept of joins using the language of spans and push-outs. A classical result is re-proven which establishes the connection between joins, ergodicity and mixing. In the process, the categorical language is refined to capture the notion of sub sigma-algebras and their invariance.

arXiv abstract · PDF

Algebraic Structures and Higher Categories · primary corpus · published 2026-09-10T17:06:25Z
Jacek Kenig, Dmitri Pavlov
arXiv categories: math.AT, math-ph, math.CT, math.MP

We develop tools to compute moduli spaces of geometric functorial field theories as mapping spaces of equivariant simplicial presheaves. Given a d-dimensional geometric structure F, presented as a presheaf on the site of smooth families of d-manifolds, we define its Cartesian realization, which is an O(d)-equivariant simplicial presheaf on the site of Cartesian spaces. We use Cartesian realizations to present the moduli space of functorial field theories with geometric structure F as a mapping space between O(d)-equivariant simplicial presheaves. In a companion paper, we use this result to compute the moduli space of smooth one-dimensional oriented Riemannian functorial field theories valued in an arbitrary smooth symmetric monoidal infinity-category.

arXiv abstract · PDF

Algebraic Structures and Higher Categories · primary corpus · published 2026-09-12T21:43:37Z
Frank Murphy-Hernandez
arXiv categories: math.CT, math.QA

We construct a categorification of the functor of grouplike elements of a Hopf algebra in the setting of braided monoidal categories. Given a braided bistrong monoidal functor admitting a right adjoint, we define a functor assigning to each Hopf monoid a group object obtained as a subobject of its underlying object by means of finite limits. We prove that this construction is functorial and provides a right adjoint to the induced free Hopf monoid functor, thereby extending the classical correspondence between groups and grouplike elements of Hopf algebras to a categorical setting.

arXiv abstract · PDF

Algebraic Structures and Higher Categories · primary corpus · published 2026-09-13T04:09:24Z
Yuki Imamura, Tomoki Yoshida
arXiv categories: math.GT, math.CT, math.GR

We introduce a notion of nilpotency for surjective quandle homomorphisms, which relativizes the nilpotency of quandles recently defined by Darn\'e. A surjective homomorphism is called nilpotent if its relative inner automorphism group is nilpotent relative to the inner automorphism group of the source. We show that this condition can equally be described through the relative transvection group and the relative adjoint group, and that it is equivalent to being a finite composite of covering homomorphisms. Extending the relative lower central series to transfinite ordinals, we then introduce hypocentral homomorphisms and characterize them as the surjections that are right orthogonal to the strongly connected homomorphisms. As a consequence, the strongly connected and the hypocentral homomorphisms form an orthogonal factorization system for the surjections in the category of quandles. Finally, we also introduce reduced and operator-reduced homomorphisms, which relativize reduced quandles, and give sufficient conditions for such a homomorphism to be nilpotent.

arXiv abstract · PDF

Algebraic Structures and Higher Categories · primary corpus · published 2026-09-13T05:00:20Z
Jean-Simon Pacaud Lemay
arXiv categories: math.CT

For any category, there exists both a free dagger category and a cofree dagger category over it. A natural question to ask is: given a dagger category, how can we tell if it is free or cofree without specifying an external base category? In this paper, we provide characterizations of both free dagger categories and cofree dagger categories via internal dagger category structure. To characterize cofree dagger categories, we use rectangular bands and show that a dagger category is cofree if and only if it is enriched over rectangular bands. For free dagger categories, we define the notion of a zigzag dagger category, and then show that a dagger category is free if and only if it is a zigzag dagger category. We also show that free dagger categories can be characterized as the coalgebras of the induced comonad from the free dagger category adjunction, and similarly that cofree free dagger categories can be characterized as the algebras of the induced monad from the cofree dagger category adjunction.

arXiv abstract · PDF

Algebraic Structures and Higher Categories · primary corpus · published 2026-09-13T08:38:38Z
Qikai Wang, Yuxiao Wang, Haiyan Zhu
arXiv categories: math.CT

We give a counterexample to completeness descent from ideal cotorsion pairs to their objects. A radical-square-zero algebra on the two-cycle gives a finite-dimensional example. The construction is intrinsically non-weakly-idempotent-complete.

arXiv abstract · PDF

Algebraic Structures and Higher Categories · primary corpus · published 2026-09-13T17:13:59Z
Roy Ferguson, Zurab Janelidze
arXiv categories: math.CT

A Grothendieck topology on a category determines both a subform of covering sieves and a quotient form obtained by identifying locally equivalent sieves. We place these two constructions in a single short exact sequence. For this purpose we introduce distributivity forms: indexed meet-semilattices equipped with distinguished indexed joins over which finite indexed meets distribute, and a strong version in which these joins also satisfy Beck--Chevalley. Over a fixed base, the resulting categories have all small limits and have kernels and cokernels relative to the closed ideal of fibrewise constant-top morphisms. Their monomorphisms are the fibrewise injective morphisms, and their relative cokernels, together with the top-reflecting morphisms, form an orthogonal factorization system. Cokernels compose but need not be stable under pullback, whereas kernels need not compose. We call a short exact sequence with prescribed middle term an extensional presentation, and prove that Grothendieck topologies on a category are precisely the extensional presentations of its maximally distributive form of sieves. Further applications recover universal productive closure operators and Lawvere--Tierney topologies, functorial non-Archimedean group topologies, and functorial linear topologies on commutative rings.

arXiv abstract · PDF

Algebra Analysis and Geometry · primary corpus · published 2026-09-08T01:18:41Z
Kenji Tokuo
arXiv categories: quant-ph, math-ph, math.LO, math.MP

We study the spectral sign implication for quantum logic, defined by the nonnegative spectral projection of the operator obtained by subtracting the antecedent projection from the consequent projection. The construction agrees with classical material implication on commuting projections and compares arbitrary pairs of projections through the spectral structure of their difference. It satisfies Hardegree's four minimal implicative conditions, his law of contraposition, and a falsity condition. It differs from the standard polynomial implications in that its value need not belong to the ortholattice generated by its arguments. Within a uniform class of Borel constructions for pairs of projections, the operations satisfying entailment, contraposition, and the falsity condition correspond exactly to measurable choices of spectral branch. In the continuous subclass, these three conditions determine the spectral sign implication uniquely. In finite dimensions, the operation is also the largest among the acceptance projections of optimal projective tests for Helstrom discrimination between subspace states with priors proportional to rank. These results connect quantum implication with the operator theory of two projections and binary quantum discrimination.

arXiv abstract · PDF

Algebra Analysis and Geometry · primary corpus · published 2026-09-08T23:38:41Z
Matthew Petersen
arXiv categories: math.HO, math.CT

A categorial approach to the non-metric geometry in Books V and VI of Euclid's \textit{Elements} is presented. Specifically, we introduce a diagrammatic syntax that can be overlaid immediately on his diagrams, thus bridging intuitive presentation with fidelity to Euclid's arguments. This syntax makes complicated definitions like V.5, and indeed the arguments throughout books V and VI, including arguments about similar figures, intuitively clear. We show in an appendix that this syntax can be used to solve a puzzle regarding ancient mathematics. Finally, we offer evidence that this approach to Euclidean diagrams is rooted in the Aristotelian tradition itself, and that a similar syntax was utilized, in antiquity, for related questions of numeric and proportions. Thus the syntax is plausibly faithful to Euclid's own thought-world, and not an outside-imposition.

arXiv abstract · PDF

Algebra Analysis and Geometry · primary corpus · published 2026-09-09T07:11:26Z
Hui Kou, Mingchun Xie
arXiv categories: math.CT

This paper introduces a natural fuzzy order on fuzzy numbers that extends the natural orders on real numbers and interval numbers. We investigate its completeness properties and show that the space of uniformly bounded fuzzy numbers is conically complete and conically cocomplete, and that it is complete if and only if the underlying continuous t-norm is the G\"odel t-norm. Moreover, it is proved that this space constitutes a \([0,1]\)-enriched domain if and only if the underlying continuous t-norm satisfies the (S) condition. These results provide a foundation for ordering fuzzy numbers.

arXiv abstract · PDF

Algebra Analysis and Geometry · primary corpus · published 2026-09-09T12:09:16Z
Gregory Patchell, Austin Shiner
arXiv categories: math.OA, math.FA, math.LO

In a tracial von Neumann algebra M, two subsets X and Y are said to be N-independent if alternating products of length at most N of trace zero words from X and Y have trace zero. We show that two approximately 2N-independent finite tuples can be perturbed, in operator norm, to be exactly N-independent. Consequently, we are able to generalize Theorem 5.1 and Theorem H of Houdayer-Ioana and resolve Problem 31 of Kunnawalkam Elayavalli in the positive.

arXiv abstract · PDF

Algebra Analysis and Geometry · primary corpus · published 2026-09-09T14:18:18Z
Jananan Arulseelan, James E. Hanson
arXiv categories: math.OA, math.LO

Using set-theoretic methods, we prove that every $\mathrm{AW}^*$-algebra is normal, resolving a question of Wright that has stood open for 46 years. This was previously known in the case of $\mathrm{AW}^*$-factors, by work of Sait\^o and Wright. We also show that if there is a model $V$ of $\mathrm{ZFC}$ with an $\mathrm{AW}^*$-algebra that fails to be monotone complete, then in some forcing extension of $V$ there is an $\mathrm{AW}^*$-factor that fails to be monotone complete, implying that any $\mathrm{ZFC}$ proof that all $\mathrm{AW}^*$-factors are monotone complete yields a $\mathrm{ZFC}$ proof that all $\mathrm{AW}^*$-algebras are monotone complete. Both results build on transfer principles for Boolean-valued factor representations originally developed by Ozawa. This work was assisted by the Danus LLM orchestration system.

arXiv abstract · PDF

Algebra Analysis and Geometry · primary corpus · published 2026-09-09T19:18:22Z
Dominika Bure\v{s}ov\'a, Pavel Pt\'ak, Jan \v{S}evic
arXiv categories: math.LO

Suppose that L is a quantum logic (= an orthomodular poset) and A, B are Boolean subalgebras of L. Suppose further that s1(resp. s2) is a state on A (resp. on B). We ask when both s1 and s2 allow for a simultaneous extension over L. Under a natural necessity condition on A, B, s1, s2 we find a sufficient condition for the existence of the extension. This condition is the requirement of an abundance of two-valued states on L. We then show by the Greechie pasting technique that this condition is far from necessary even for state-space-rich logics.

arXiv abstract · PDF

Algebra Analysis and Geometry · primary corpus · published 2026-09-10T06:57:01Z
Shuangquan Li, Yao Ouyang
arXiv categories: math.FA, math.LO

The weak dominance of aggregation operators, particularly between triangular norms (t-norms) and triangular conorms (t-conorms), has attracted considerable attention in aggregation operator theory. While several characterizations have been obtained for Archimedean and continuous cases, a general criterion for continuous t-conorms over continuous t-norms remains to be fully clarified. In this paper, we provide a complete characterization of a continuous t-conorm weakly dominating a continuous t-norm. We first reduce the problem for ordinal sum operators to that for their single Archimedean components, and then express the weak dominance condition entirely in terms of the additive generators of these components. Our approach covers both strict and nilpotent cases uniformly, and recovers the known results for Archimedean operators as a special case.

arXiv abstract · PDF

Algebra Analysis and Geometry · primary corpus · published 2026-09-10T08:14:40Z
Andrzej Odrzywo{\l}ek
arXiv categories: cs.SC, cs.LG, math.LO

The discovery of the EML operator, sufficient to evaluate the standard explicit purely transcendental elementary functions, has led to considerable interest and discussion across multiple scientific disciplines. However, most authors have focused on the binary EML itself, while numerous similar variants with slightly different properties are now known. This article attempts to close this gap by enumerating and classifying them. We also take this opportunity to clarify common misconceptions related to the EML operator. The principal goal, symbolic regression within an architecture as close as possible to proven neural networks which combine matrix multiplication with a single univariate non-linear activation function, remains beyond reach. Instead, we propose a M\"obius layer, with rational functions replacing matrix operations, and showcase the recently discovered activation function eml(x,1/x), which allows exp(x) and ln(x) to be recovered separately, and hence all elementary functions to be evaluated within a rational generalization of the neural network.

arXiv abstract · PDF

Algebra Analysis and Geometry · primary corpus · published 2026-09-13T13:34:02Z
Zhenyu Xiu
arXiv categories: math.LO

We establish necessary and sufficient conditions under which a binary operation on a bounded trellis is a proper nullnorm. The representation combines a t-conorm on the lower interval, a t-norm on the upper interval, two order-preserving maps, and a commutative, increasing function on $I_a^3\times I_a^3$, where $I_a^3$ consists of the elements incomparable with the absorbing element $a$ that neither reach $a$ nor are reachable from $a$. Unlike earlier range-restricted constructions, this function may take values anywhere in the trellis. To preserve associativity for such unrestricted values, we introduce a mixed interaction function that evaluates every pair with at least one component in $I_a^3$. We also derive the specializations in which this region is empty or consists of a single element, including an exact description of the admissible value in the singleton case. A five-element lattice example shows that the mixed associativity condition is independent of the remaining hypotheses, while a fourteen-element nontransitive trellis example demonstrates the necessity of allowing the unrestricted range. Finally, the principal range-restricted subclasses and the bounded-lattice case are recovered as specializations of the general representation.

arXiv abstract · PDF

Logic Computability and Foundations · primary corpus · published 2026-09-07T11:02:51Z
Andrew Moorhead, Reinhard P\"oschel
arXiv categories: math.RA, math.LO

It is well known that the polymorphism clone of a quasiorder is determined by its unary part, in the sense that any operation is a polymorphism if it satisfies the condition that all unary functions obtained by fixing some of its variables at constant values are polymorphisms. We show that a clone satisfies an analogous property for a particular fixed arity $d$ if and only if it is determined by a collection of what we call higher-dimensional generalized quasiorders whose dimension is equal to $d$. We define higher-dimensional generalized quasiorders with the appropriate generalizations of reflexivity and transitivity to the higher-dimensional setting, which rely on an explicit analysis of 'rectangular' arity.

arXiv abstract · PDF

Logic Computability and Foundations · primary corpus · published 2026-09-07T12:57:26Z
Matteo Casarosa, Philipp Schlicht
arXiv categories: math.LO

Kechris, Solecki and Todor\v{c}evi\'c's $G_0$-dichotomy characterizes Borel graphs that admit a Borel measurable coloring with countably many colors. We show that the analogue to the $G_0$-dichotomy for generalized Cantor spaces fails at the lowest possible complexity, namely for closed graphs.

arXiv abstract · PDF

Logic Computability and Foundations · primary corpus · published 2026-09-07T13:31:43Z
Mervyn Tong
arXiv categories: math.LO, math.CO

We give direct combinatorial proofs that 1-semi-equational theories satisfy two combinatorial properties that imply the non-interpretability of certain fields. Our main result is that Boolean combinations of 1-semi-equations have almost linear Zarankiewicz bounds, and hence no infinite field is interpretable in a 1-semi-equational theory; this answers a question of Chernikov--Mennen and Chernikov--Starchenko, who had respectively established almost linear Zarankiewicz bounds for Boolean combinations of $(2,1)$-semi-equations and Boolean combinations of weakly normal relations. (This was recently and independently established by Gou, Mirabi, Mittal, Tran, and Yang, using different techniques and producing different bounds.) We also show that $(k,1)$-semi-equations satisfy the $\delta$-strong Erd\H{o}s--Hajnal property with $\delta=1/6^{k-1}$; this had previously been established by Chernikov--Starchenko for an ineffective constant $\delta>0$.

arXiv abstract · PDF

Logic Computability and Foundations · primary corpus · published 2026-09-07T22:50:50Z
Boaz Tsaban
arXiv categories: math.GN, math.LO

We prove that there is, consistently, a regular Lindel\"of space of cardinality $\aleph_1$ that is not a D-space. This settles a central problem in set-theoretic topology, and many related problems. The existence of such a space is independent of ZFC\@. The question whether, consistently, every regular hereditarily Lindel\"of space is a D-space remains open.

arXiv abstract · PDF

Logic Computability and Foundations · primary corpus · published 2026-09-07T23:58:34Z
M\'{a}rk Po\'{o}r, Jing Zhang
arXiv categories: math.LO

We show that, relative to the existence of an inaccessible cardinal, it is consistent that for an inaccessible cardinal $\kappa$, there is a non-trivial automorphism of $\mathcal{P}(\kappa)/\mathrm{fin}$ whose restriction to $\mathcal{P}(\beta)/\mathrm{fin}$ is induced by a bijection on $\beta$ for every $\beta<\kappa$. This answers questions posed by Larson--McKenney, Shelah--Stepr\=ans, and Veli\v{c}kovi\'{c}.

arXiv abstract · PDF

Logic Computability and Foundations · primary corpus · published 2026-09-08T01:07:28Z
Patrizio Cintioli
arXiv categories: math.LO

We construct a set $U\leq_T\emptyset''$ whose bounded finite-one degree, ordered internally by one-one reducibility, consists exactly of a countable dense linear order without endpoints. More precisely, \[ \left( \{[B]_1:B\equiv_{\mathrm{bfo}}U\},\leq_1 \right) \cong (\mathbb Q,\leq). \] This exact realization contrasts with two previous results. In earlier work, a bounded finite-one degree was constructed that contains a copy of $(\mathbb Q,\leq)$, but the same degree also contains an infinite antichain of one-one degrees and, more generally, embedded copies of all countable partial orders; thus the dense chain does not exhaust the degree. In a different direction, $m$-rigidity yields an almost-sure and comeager obstruction: for a measure-$1$ and comeager class of sets, the corresponding bounded finite-one degree contains an infinite antichain of one-one degrees and hence is not linearly ordered. The present construction shows that, despite this typical negative behaviour, exact dense linear order can occur. In particular, it gives an affirmative answer to Open Question~3 of Richter, Stephan, and Zhang. The proof has two main parts. A block homogenization construction produces a noncylindrical set $U$, a weak dyadic tower $(U_e)_{e\in\mathbb N}$, computable reservoirs of both colours, and a base absorption property. An abstract absorption-to-exhaustivity theorem then shows that every member of the bounded finite-one degree of $U$ is one-one equivalent to some finite autojoin $mU_e$, thereby yielding the exhaustive classification above.

arXiv abstract · PDF

Logic Computability and Foundations · primary corpus · published 2026-09-08T08:26:29Z
Xavier Pig\'e
arXiv categories: math.LO, math.AG

We generalise Yin's motivic integration with section to the Hensel-minimal framework, with and without volume forms, building on Stout and Vermeulen's work on a Hrushovski-Kazhdan style motivic integral for $1$-h-minimal valued fields. In particular, we get a bijective motivic integral \emph{\`a la} Hrushovski-Kazhdan between certain Grothendieck groups of definable sets on the valued field and the coarse Grothendieck groups on $\mathrm{RV}$ in the Denef-Pas language, with angular component. In the second half of the article, we build a Cluckers-Loeser-like framework and show that our constructions indeed give back Cluckers-Loeser motivic integral. Thus Cluckers-Loeser motivic integration derives from an isomorphism of Hrushovski-Kazhdan motivic integration, but in the Denef-Pas language with a section of $\mathrm{RV}$.

arXiv abstract · PDF

Logic Computability and Foundations · primary corpus · published 2026-09-08T14:49:58Z
Ismael Calomino, Daniela Montangie
arXiv categories: math.LO

The aim of this paper is to present a topological duality for the algebraic category of Stonean Hilbert algebras and certain morphisms between them, called $\neg$-morphisms. Also, we apply this duality to characterize the Heyting algebra of $\alpha$-ideals of a Stonean Hilbert algebra.

arXiv abstract · PDF

Logic Computability and Foundations · primary corpus · published 2026-09-08T17:46:45Z
Ming Ng
arXiv categories: math.NT, math.AG, math.CT, math.LO

Classically, the places of $\mathbb{Q}$ are often regarded as a one-point compactification of $\mathrm{Spec}(\mathbb{Z})$, with the real place corresponding to a formal ``prime'' added at infinity. Re-examining this picture from a topos-theoretic perspective reveals a subtler geometry: while the non-Archimedean places are identified with singletons indexed by the non-zero prime ideals of $\mathbb{Z}$, the Archimedean place is represented by the space of upper reals $\overleftarrow{[0,1]}$, which may be informally thought of as the unit interval equipped with a non-Hausdorff topology. On a technical level, our analysis brings together geometric logic and descent techniques from topos theory, distinguishing standard descent from lax descent toposes both at the level of sheaves and of the geometric theories they classify. More broadly, this paper brings into conversation two parallel distinctions: on the number-theoretic side, between Archimedean and non-Archimedean phenomena, and on the topos-theoretic side, between standard and lax descent. Looked at from a high level, these perspectives begin to converge on a common theme: how should the connected and the disconnected interact?

arXiv abstract · PDF

Logic Computability and Foundations · primary corpus · published 2026-09-09T15:00:07Z
Achyuth Jayadevan
arXiv categories: math.GR, math.LO

For an ordinary finite presentation $P=\langle x_1,\ldots,x_n\mid R\rangle$, put $G(P)=F_n/\langle\langle R\rangle\rangle$. We construct a primitive-recursive predicate $V$ with $G(P)''=1 \Longleftrightarrow \exists c\in\mathbb{N}: V(P,c)=1$. Thus finite presentations of metabelian groups are recursively enumerable, answering Kourovka Problem 17.124. An effective form of the Bieri-Strebel covering construction, using signed Laurent relations and rational separation, gives a family of finitely presented metabelian groups cofinal under epimorphisms. Products of conjugates of defining relators witness these epimorphisms. The construction and enumeration theorem are formalized in Lean 4.

arXiv abstract · PDF

Logic Computability and Foundations · primary corpus · published 2026-09-09T22:06:00Z
Rasoul Ramezanian
arXiv categories: math.LO

We develop a foundational distinction between \emph{well-definedness} and \emph{predetermination}. A persistent mathematical or computational object may return a unique answer whenever a query is made and preserve every previously returned answer, while its answers to as-yet unqueried inputs are not represented by one completed, history-independent extension. We call such an object \emph{well-defined but non-predetermined}. We next formulate an observer-based semantics. All observers inhabit one shared computational world, their interactions modify one common global state, and they have access to one realized history. Under axioms of shared history, historical irreversibility, persistence, and historical indistinguishability, embedded observers cannot establish from the realized history alone whether its compatible extension was predetermined or progressively formed. A persistently evolutionary polynomial time computable oracle supplies a concrete example and yields a deterministic--nondeterministic separation under an explicitly history-sensitive semantics. We then derive a conditional result concerning the provability of \(P=NP\). The conclusion is an observer-relative unprovability theorem, not an unconditional proof of classical \(P\neq NP\).

arXiv abstract · PDF

Logic Computability and Foundations · primary corpus · published 2026-09-09T22:19:01Z
Tenyo Takahashi
arXiv categories: math.LO

A modal logic is elementary if it is sound and complete with respect to an elementary class of Kripke frames. We prove that if a finitely axiomatizable modal logic L is elementary, then the validity problem for L, which asks whether a given finite Kripke frame validates L, is in P. This allows us to transfer complexity results in graph theory to the study of elementarity of modal logics. As an application, we construct infinitely many finitely axiomatizable K4-stable logics that are not elementary, assuming P $\neq$ NP. This result provides a conditional negative answer to an open question in [Bezhanishvili et al., 2018] for K4-stable logics.

arXiv abstract · PDF

Logic Computability and Foundations · primary corpus · published 2026-09-10T03:58:00Z
Lu Liu
arXiv categories: math.LO

The Kolmogorov complexity of a string characterize how complex it is to describe the string. If every prefix of a real $x$ is more complex to describe than every prefix (of the same length) of real $y$, then it is seen as $x$ is more complex to describe than $y$. It is wondered if there is a real $x$ so that no other reals are strictly more complex (to describe) than $x$. The behavior of Kolmogorov complexity functions generated by reals (namely $n\mapsto$ the minimal description length of the real) is quite chaos. Therefore, it is widely believed that there are many reals that are maximally complex to describe. For instance, it is conjectured that all random enough reals have maximal $K$-degree. In this paper, it is shown that there is no real with maximal $K$-degree. Actually, for almost all real $x$, we can uniformly computably find another real whose $K$-degree is strictly above $x$.

arXiv abstract · PDF

Logic Computability and Foundations · primary corpus · published 2026-09-10T08:38:02Z
Shimon Garti
arXiv categories: math.LO, math.CO

We prove, in $\mathsf{ZFC}$, that the $\lambda$-terraced cube relation fails whenever $\lambda$ is an uncountable cardinal. The corresponding terraced relation for quadruples fails for every $\lambda$. If $\lambda$ is $\aleph_0$ then the pretinent terraced relation has consistency strength of at least one Woodin cardinal. We prove positive polarized relations at a successor and a double successor from wondrous ideals. We show, however, that there are no such ideals over two consecutive cardinals simultaneously.

arXiv abstract · PDF

Logic Computability and Foundations · primary corpus · published 2026-09-10T12:57:20Z
Esha Jain, Sankha S. Basu
arXiv categories: math.LO

In this article, we have introduced a new possibilistic logic on a logic of formal inconsistency with the aim of developing a possibility theoretic framework to deal with uncertainty and inconsistency meaningfully without leading to a system collapse. We have discussed the syntax and semantics for this logic and have proved the soundness and completeness theorems. A set of new measures of consistency, contradictoriness, and triviality of a set of formulas have been defined. These have then been put to use in an example to show that this framework can provide better means of machine reasoning.

arXiv abstract · PDF

Set Theory Topology and Dynamics · primary corpus · published 2026-09-09T23:13:01Z
David J. Webb
arXiv categories: math.LO

We show that the only degree which cannot co-enumerate a non-trivial $\Pi^0_1$-immune real is $\emptyset$, resolving a conjecture of the author. The main ingredient is that if a real $A$ has that all $A$-maximal sets are c.e., then $A$ has c.e. degree, which can be proved via a coding mechanism and two classical results of Lachlan.

arXiv abstract · PDF

Set Theory Topology and Dynamics · primary corpus · published 2026-09-10T05:25:07Z
Yatir Halevi, Itay Kaplan
arXiv categories: math.GR, math.LO

For any infinite cardinal $\kappa$, we give an example of a centerless group $G$ of cardinality $\kappa$ whose automorphism tower terminates after $\kappa^+$ steps, answering a question of Simon Thomas. The work on this paper was assisted by AI.

arXiv abstract · PDF

Set Theory Topology and Dynamics · primary corpus · published 2026-09-10T15:29:12Z
Xinan Dai, Wenhao Deng, Yingdong Shi, Tailin Wu, Yuchen Yang
arXiv categories: math.DS, math.LO

We prove that conjugacy of minimal homeomorphisms of the Cantor space is Borel bireducible with isomorphism of countable graphs, answering the Cantor minimal case of a question of Foreman. We obtain the lower bound by encoding countably based profinite groups. Finite quotient homomorphisms are represented by factor maps between a common family of minimal subshifts. Amalgamation makes the resulting inverse limit independent, up to conjugacy, of the quotient presentation. Conversely, finite-stage factorization recovers the group from any conjugacy of these inverse limits.

arXiv abstract · PDF

Set Theory Topology and Dynamics · primary corpus · published 2026-09-10T17:42:06Z
Clement Yung
arXiv categories: math.LO, math.CO

We provide a proof, free of ultrafilters and almost reduction, that every subset of a topological Ramsey space is Ramsey in the Solovay model.

arXiv abstract · PDF

Set Theory Topology and Dynamics · primary corpus · published 2026-09-10T17:57:55Z
Jos\'e de Jes\'us Pelayo-G\'omez
arXiv categories: math.LO, math.CO

We answer in the negative the question of Thomas, recorded by Conley, Conley--Marks--Unger, and Conley--Tamuz, of whether every locally finite Borel graph admits a Borel unfriendly partition. Our counterexample has unbounded degree and is closed on a zero-dimensional Polish space; its connectedness relation is hyperfinite, and its components are bipartite and one-ended. Every unfriendly colouring is proper. Together with a parity obstruction, this rigidity rules out Baire measurable colourings that are unfriendly on a comeager set, and measurable colourings that are unfriendly almost everywhere for a quasi-invariant probability of finite average degree. In the positive direction, a Borel graph of maximum degree at most four admits a Borel unfriendly colouring whenever each component contains a cycle or a vertex of degree at most two. This reduces the Borel problem in maximum degree three to cubic forests and, with a theorem of Conley--Marks--Unger, gives Baire measurable unfriendly colourings for all Borel graphs of maximum degree at most four.

arXiv abstract · PDF

Set Theory Topology and Dynamics · primary corpus · published 2026-09-11T03:50:07Z
Joey Veltri
arXiv categories: math.LO, math.DS

We prove several necessary and sufficient conditions under which a point satisfies the Poincar\'e Recurrence Theorem for all computable (ergodic) measure-preserving transformations and all sets of a particular complexity. The necessary conditions are obtained by constructing specific measure-preserving transformations which violate recurrence. While some of these conditions pertain to standard notions of algorithmic randomness, others involve new notions of genericity developed in the context of a computable probability space, which we call $\Pi^0_n$-genericity and quasi-$\Pi^0_n$-genericity. We also provide conditions under which points recur at a positive frequency in sets containing them, regarding both simple and multiple recurrence.

arXiv abstract · PDF

Set Theory Topology and Dynamics · primary corpus · published 2026-09-11T08:34:57Z
Anton Freund, Katarzyna W. Kowalik, Davide Manca
arXiv categories: math.LO

We exhibit a well-ordering principle that is equivalent to a theory of partial impredicativity. The latter goes back to Towsner and relates to recent work of Suzuki and Yokoyama. Together with part I of the present paper, this yields a combinatorial upper bound on the axiomatic strength of Fra\"iss\'e's conjecture.

arXiv abstract · PDF

Set Theory Topology and Dynamics · primary corpus · published 2026-09-11T11:40:11Z
Andreas Weiermann
arXiv categories: math.LO

We bound the eventual order types of Skolem functions below finite exponential towers. Writing $E_0(u)=u$, $E_{n+1}(u)=2^{E_n(u)}$, and $\omega_0=1$, $\omega_{k+1}=\omega^{\omega_k}$, the argument gives \[ |\Sk_{<E_n(x^m)}|<\omega_{r_n},\qquad r_n=2+\frac{n(n+3)}2\quad(n\ge1,\ m\ge2\text{ fixed}). \] For triple towers we obtain the sharper bound $|\Sk_{<E_3(x^m)}|<\omega_{10}$ for every fixed $m\ge1$. The proof combines comparisons of asymptotic expansions with finite recursive decompositions and ordinal estimates for ordered sums and products. The analytic part is developed in the classical field of logarithmic-exponential series. We prove the required discreteness, support and truncation statements in this setting. The external inputs are the series construction of van den Dries--Macintyre--Marker and the order and ordinal estimates recalled from Berarducci--Mamino. These bounds imply $|\Sk|=\varepsilon_0$.

arXiv abstract · PDF

Set Theory Topology and Dynamics · primary corpus · published 2026-09-11T14:42:39Z
Piotr Koszmider
arXiv categories: math.LO, math.FA, math.GN, math.OA

We show that maximal abelian C*-subalgebras (masas) of the Calkin algebra (the algebra of all bounded operators on the separable Hilbert space modulo compact operators) may consistently have their densities strictly less than continuum and we describe many isomorphism types of such masas. Specifically, we prove that after adding any number of Cohen reals to a model of CH the algebra $C(K_{\mathcal A})$ of all complex-valued continuous functions on the Stone space $K_{\mathcal A}$ of a Boolean algebra $\mathcal A$ of cardinality $\omega_1$ is $*$-isomorphic to a masa of the Calkin algebra if and only if $\mathcal A$ does not admit a countably generated ultrafilter. Moreover, for every such Boolean algebra we obtain $\omega_2$ pairwise unitarily non-equivalent such masas, none of which has a commutative lift. We also show in ZFC that if a C*-algebra of the form $C(K)$ for any compact Hausdorff $K$ is $*$-isomorphic to a masa of the Calkin algebra, then no point of $K$ may have character smaller than $\mathfrak p$. Therefore, consistently, there may not be any masa of the Calkin algebra of density less than continuum.

arXiv abstract · PDF

Set Theory Topology and Dynamics · primary corpus · published 2026-09-11T20:26:42Z
Vladimir Vovk
arXiv categories: math.LO

A finite object is called probabilistically random if it is an algorithmically random element of a finite set whose Kolmogorov complexity is relatively small. This note studies the amount of probabilistically nonrandom objects (those that are not probabilistically random) as gauged by the universal measure and without assuming any structure on the objects. The main results imply that the universal measure of probabilistically nonrandom objects is vanishingly small and establish the dependence of their universal measure on the required degree of probabilistic randomness.

arXiv abstract · PDF

Set Theory Topology and Dynamics · primary corpus · published 2026-09-12T11:23:15Z
Joanna Jureczko
arXiv categories: math.LO

In 1929, Banach and Kuratowski proved under CH a combinatorial theorem, which implies that there is not a non-vanishing $\sigma$-additive finite measure on $\mathbb{R}$ which is defined for every set of reals. In 2003 Bartoszy\'nski and Halbeisen proved that Banach and Kuratowski theorem is equivalent to the existence of a K-Lusin set of the cardinality continuum an the existence of such sets is independent of $ZFC + \neg CH$. On the other hand in 1965 Efimov introduced the strong sequences method which used to prove some well-known theorems in dyadic spaces. The aim of this paper is to show that all this notions can be generalized, i.e. considered in the generalized Baire space and to show some equivalences among them. Moreover, some applications in the direction of calibres, boundedness and partitions relations are also shown.

arXiv abstract · PDF

Set Theory Topology and Dynamics · primary corpus · published 2026-09-12T13:30:31Z
Farmer Schlutzenberg
arXiv categories: math.LO

Let $M$ be a $(0,\omega_1+1)$-iterable mouse with no largest cardinal. Let $\gamma\leq\kappa$ be uncountable cardinals of $M$, with $\kappa$ regular in $M$. Then $M$ satisfies $\diamondsuit_{\kappa\gamma}^+$, and if $\kappa$ is non-ineffable in $M$ then $M$ satisfies $\diamondsuit_{\kappa\kappa}^+$. Suppose that either $\omega_1^M=\omega_1$ or $M$ satisfies "I am $(0,\omega_1+1)$-iterable". Let $\kappa\geq\omega_1^M$ be a cardinal of $M$. Then $M$ satisfies $\diamondsuit^*_{\kappa\omega_1^M}$.

arXiv abstract · PDF

Set Theory Topology and Dynamics · primary corpus · published 2026-09-12T16:48:00Z
Evan Leach
arXiv categories: math.LO

We present a new approach to lower bounds on Borel rank via a connection between Borel sets and infinite circuits. We prove an infinite analog to H{\aa}stad's switching lemma called the \emph{restriction lemma}, which shows that by fixing the values of some inputs, we can simultaneously reduce the complexity of one Borel function while largely maintaining the complexity of another. This result provides a purely combinatorial proof of the Borel hierarchy theorem, as well as simple proofs of various Ramsey-like properties of Borel sets and functions. We prove that the restriction lemma is sharp and also discuss counterexamples demonstrating the limitations of the restriction technique, in the context of both Borel functions and $\mathsf{AC}^0$ circuit families.

arXiv abstract · PDF

Set Theory Topology and Dynamics · primary corpus · published 2026-09-12T23:04:24Z
Henning Fernau, Sanjay Jain, Linus Richter, Frank Stephan, Dan Turetsky
arXiv categories: cs.FL, math.LO

We study the complexity of simple semi-conditional grammars (SSCGs) in terms of the number of their terminals and non-terminals. We show that SSCGs with three non-terminals can generate all RE languages; two non-terminals suffice for linear languages; and one suffices for unary regular languages. We also determine both upper bounds and fundamental limitations of SSCGs: while certain one-non-terminal SSCGs can generate non-context-free languages, every language generated by a one-non-terminal SSCG is in non-deterministic linear space. We also prove that there exists a regular language of alphabet size at least 3 which cannot be generated by any one-non-terminal SSCG. Finally, we prove that membership testing for SSCGs of two non-terminals is already NP-hard.

arXiv abstract · PDF

Set Theory Topology and Dynamics · primary corpus · published 2026-09-13T17:53:46Z
Michael Lange
arXiv categories: math.LO

We prove that the SU-rank of a supersimple theory is no greater than that of any of its supersimple expansions. A proof for finite rank theories already exists in the literature, but non-continuity presents a problem at limit ranks. We prove the non-decreasing of SU-rank in expansions type-by-type by reducing to finding, in the base theory, certain trees of forking extensions in which the formulas and dividing numbers which witness dividing have a sufficiently uniform pattern. In the case of countable ranks, we can give an especially nice description of this uniformity: for a countable ordinal $\alpha$, any type of SU-rank at least $\alpha$ in a supersimple theory has a chain of forking extensions in the reverse order type of $\alpha$.

arXiv abstract · PDF

Agent Security and Assurance · cs.SE candidate · published 2026-09-08T07:37:00Z
Dimitrios Stamatios Bouras, Yihan Dai, Sergey Mechtaev
arXiv categories: cs.SE

Coding agents use system-level tools to read files, execute commands, and modify source code. Within the agent's sandbox, these tools often carry ambient authority: naming a resource is sufficient to act on it. Indirect prompt injection exploits this authority by placing instructions in repository files or tool output that cause the agent to perform actions the user did not request. We propose CapScope, a harness-level authorization mechanism that restricts tool use without requiring the model to identify malicious text. Before repository contents or tool output are read, CapScope derives a task-wide authority ceiling from trusted input. It then assigns each agent a separate set of typed capabilities, stored outside the model's context. Every tool call is checked against the capabilities of the agent that issued it. Permissions assigned to one sub-agent are therefore not automatically available to another. An injection may cause an agent to request an action, but the request is blocked unless that agent already has the required capability. We implement CapScope on the Pi coding agent and evaluate it in a repair workflow where an orchestrator delegates subtasks to separate sub-agents. The evaluation covers five Python tasks, five injection surfaces, four authorization conditions, and three trials per cell (300 runs). The injected effect executes in 33-47/75 runs under the ambient-authority and global-policy baselines, compared with 3/75 under CapScope. CapScope completes 68/75 repairs, while the baselines complete 68-72/75.

arXiv abstract · PDF

Agent Security and Assurance · cs.SE candidate · published 2026-09-08T09:11:53Z
Yang Li, Sergey Volkov, Hai Liu, Zongsi Xu, Xiyu Chen, Tuo Zhou, Dian Shao, Hao Sun, Ye Lu
arXiv categories: cs.MA, cs.SE

Agentic systems persist model-visible memory while mutating workspaces, while a runtime, registry, or approval service may hold authority state outside both. Identical final files can then require opposite safe actions. We call this the cross-substrate authority gap: decision- relevant authorization information resides outside the planner-visible workspace or memory state. Across two controlled mini-benchmark families, three experiments compare planner-observation augmentation with an execution-time authority check using real Git lineage, durably recorded agent execution attempts, deterministic oracles, and two model routes. Experiment 1 is a 128-cell controlled evidence ablation: authority-blind candidate evidence obtains 0/32 final semantic success, while raw receipts and a typed relation both obtain 32/32. The missing authority fact accounts for the gain; typed packaging provides no observed planning-accuracy gain over equal raw information. Experiment 2 uses 96 planning calls: workspace-visible evidence yields 12/16 unsafe publication decisions, and planning with the typed relation remains unreliable (15/32 first actions correct; 11/32 invalid or absent). Experiment 3 replays the same 32 fixed model-generated first-action intents with zero additional model calls; a deterministic execution guard prevents all six unsafe intents from becoming effects and permits all 12 valid authorized publish intents. These results position authority enforcement at the mutation boundary as the operational endpoint of memory governance.

arXiv abstract · PDF

Agent Security and Assurance · cs.SE candidate · published 2026-09-09T22:18:36Z
Alireza Lotfi, Mirza Masfiqur Rahman, Imtiaz Karim, Elisa Bertino
arXiv categories: cs.CR, cs.SE

The Agent2Agent (A2A) protocol, now governed by the Linux Foundation, is an open standard that enables autonomous AI agents to discover, authenticate with, and delegate tasks to one another across organizational boundaries. Designed to complement the Model Context Protocol (MCP) for tool integration, A2A is rapidly emerging as the horizontal communication layer of the multi-agent ecosystem. Yet the protocol's security has received no systematic analysis. This paper presents A2ABreak, the first rigorous systematic security analysis of the A2A protocol. We introduce a novel framework that utilizes an LLM-assisted extraction of a verified finite-state machine directly from the natural-language specification, producing a unified model of 37 states and 76 transitions from 929 formalized statements, and then systematically reasons over this model to discover protocol-level vulnerabilities through adversarial verification, under a full-compliance assumption. Our analysis uncovers 11 new vulnerabilities, each exploitable by a specification-compliant adversary without requiring any implementation flaw. Among the findings are cross-client context injection through unprotected context identifiers, credential harvesting via multi-hop identity loss in delegation chains, and data exfiltration through rogue agents advertising unattested capability claims. A2ABreak achieves 73.3% precision and 84.6% F1 against independent expert review, while a zero-shot LLM baseline operating over the same specification produces zero confirmed findings, demonstrating that explicit formal grounding is essential for sound protocol security analysis.

arXiv abstract · PDF

Agent Security and Assurance · cs.SE candidate · published 2026-09-10T03:10:58Z
Shenghan Zheng, Zonglin Di, Yimin Liu, Kyoung Whan Choe, Jiankai Sun, Heguang Lin, Penghao Jiang, Yifeng He, Xiao Cheng, Jicheng Wang, Wenbo Chen, Alex Yates, Yinzhe Zhao, Bingran You, Yuan Gao, Ayush Munot, Shubham Gaur, Zhe Ye, Hao Wang, Xiangyi Li, Dawn Song, Christophe Hauser
arXiv categories: cs.CR, cs.AI, cs.SE, cs.SY, eess.SY

LM-agent benchmarks increasingly function as interactive evaluation infrastructure. Agents observe state, call tools, modify workspaces, submit artifacts, and receive rewards from outcome procedures. This interactivity makes evaluations vulnerable to reward hacking: an agent improves its measured score by exploiting the reward-relevant trajectory instead of solving the intended task. Existing defenses rely largely on task-specific patches, prompt instructions, or post-hoc detectors. They do not provide reusable evidence that a concrete run remained within its intended evaluation boundary. This paper presents BenchShield, a model-backed instrumentation layer for reward integrity in LLM-agent evaluation. BenchShield grounds detection in a finite lifecycle model of an evaluation's reward-relevant events. Within the benchmark infrastructure, two complementary analyses operate over this model. A static, phase-aware taint analysis exposes reward-hacking paths before a run. Its runtime counterpart uses infrastructure-side evidence to attribute concrete agent use and emit evidence-backed claims. We construct BenchShield Trajectories, a human-labeled corpus of 456 adjudicated trajectories from more than 31,000 public agent runs across three benchmarks. Compared with an agentic hackability scanner baseline on the same tasks and model, BenchShield improves full-chain recall from 23-94% to 77-100%, same-vector coverage from 16-56% to 43-78%, and reduces per-task cost by up to 65%. Its runtime analysis achieves 96% accuracy in detecting reward hacking from infrastructure-side evidence.

arXiv abstract · PDF

Agent Security and Assurance · cs.SE candidate · published 2026-09-13T20:40:11Z
Mirza Samad Ahmed Baig, Syeda Anshrah Gillani, Asher Ali, Muhammad Hamzah Siddiqui
arXiv categories: cs.CR, cs.AI, cs.DB, cs.SE

Multi-tenant tools commonly accept a tenant identifier and validate it against the caller's entitlement. For a large language model (LLM) agent, that pattern delegates resource selection to a process whose context may contain attacker controlled instructions. We formalize this stochastic deputy problem and present a structural defense: remove tenant identity from the Model Context Protocol (MCP) tool schema, bind scope to a verified credential, and enforce it below the agent. In a 373-trial ablation across eight model configurations and two transports, a correctly validated tenant parameter served every out-of-scope attempt: 26 of 26, or 26 of 41 plausible-pretext trials overall. With the parameter removed, no tool signature could express the read. Twelve of 56 trials instead escaped the interface by forging writable scope, showing that interface invariance requires cryptographically protected context. On a production dataset containing multiple GBs of data, set-valued scope caused a measured $57\times$ latency ratio under function-wrapped membership predicates; a JSON_TABLE lateral join recovered index access where the tenant key was indexed. The evaluation also exposes deployment limits, including an entitlement-size query-planner cliff and incomplete index coverage. The result is a tenant-isolation argument that depends on enforceable interfaces and credentials rather than model compliance.

arXiv abstract · PDF