Search arXivSearch

arXiv · 2609.15879

Finite Dependence and Invariance Hierarchies for Finitely Supported Structures

Abstract

Finite support indicates that the dependence is limited, but not how each finite context controls what can be observed. For a data symmetry G \leq Sym(A) and a finitely supported G-set X, we study the finite-dependence profile X^S = {x : Fix_G(S) fixes x}, indexed by finite contexts S \subseteq A. For relations on A^n this yields Boolean algebras B^{(n)}_{G,S} = Inv_n(Fix_G(S)), forming the invariance hierarchy. The hierarchy separates several nominal principles. Its meet law is the relation-algebra form of the Bojanczyk-Klin-Lasota least-support criterion, while level injectivity is fungibility. The independent join law governs composition across unions of contexts; it holds for locally oligomorphic automorphism groups of ultrahomogeneous structures in purely relational languages of arity at most two, but can fail for unary observations over ternary data. Freshness remains valid sort by sort, and its unrestricted some/any form characterizes full equality symmetry among closed groups. With least supports, orbit-finiteness implies finite context levels and a uniform support bound; under local oligomorphicity the converse also holds. Pointwise closure does not change the profile, and standard atomic-site presentations show that suitable ultrahomogeneous structures with the same age have equivalent action topoi, even though their material FSS universes may retain different external cardinal data. Contextual orientability gives a complementary pointed invariant whose threshold is the least support size of choice from unordered pairs. For countable omega-categorical structures with degenerate algebraic closure, the meet law is equivalent to weak elimination of imaginaries.

Explore related subjects

Keep this discovery

Explore connections, maps & timelines

BibTeXRIS

Gabriel Ciobanu. 2026-09-14. Finite Dependence and Invariance Hierarchies for Finitely Supported Structures. https://arxiv.org/abs/2609.15879

Cite the original work for its findings. Save a collection to share your selection of sources.

KEEP EXPLORING

Related papers

Deciding Predicate Logical Theories of Real-Valued Functions

The notion of a real-valued function is central to mathematics, computer science, and many other scientific fields. Despite this importance, there are hardly any positive results on decision procedures for predicate logical theories that reason about real-valued functions. This paper defines a first-order predicate language for reasoning about multi-dimensional smooth real-valued functions and their derivatives, and demonstrates that - despite the obvious undecidability barriers - certain positive decidability results for such a language are indeed possible.

cs.LO

Structural Liveness of Conservative Petri Nets

We show that the EXPSPACE-hardness result for structural liveness of Petri nets [Jancar and Purser, 2019] holds even for a simple subclass of conservative nets. As our main result, we prove that for structurally live conservative nets, the values of the minimal live markings are at most doubly exponential in the size of the net. This implies the EXPSPACE-completeness of structural liveness for conservative Petri nets. The result also applies to structurally bounded Petri nets, whereas the complexity of the general case remains open. As a proof ingredient of independent interest, we present an extension of known results on the bounds of minimal integer solutions to Boolean combinations of linear equalities, inequalities, and divisibility constraints.

cs.LO

Verifying Numerical Methods with Isabelle/HOL

Modern machine learning pipelines and ODE solvers are built on numerical algorithms. Reliable numerical methods are thus a prerequisite for trustworthy machine learning and cyber-physical systems. We evaluate a framework designed for verifying imperative programs and the Isabelle proof assistant as tools for proving the total correctness of four numerical algorithms: the bisection method, the fixed-point method, the perceptron, and the gradient descent algorithm. Our verifications required subtle extensions and generalisations to Isabelle's version of Taylor's theorem and higher-order derivatives. Finally, we reflect on the framework's automation, friendly syntax, and on further requirements to turn it into a verification tool for numerical methods.

cs.LO