Flip-packability: uniform characterisations of tame graph classes

Ioannis Eleftheriadis

Home/Archive/arXiv

arXiv · 2609.33705

Flip-packability: uniform characterisations of tame graph classes

Ioannis Eleftheriadis

View original source ↗Read source document ↗Export metadata ↓

Abstract

A class of graphs is monadically dependent if one cannot encode all graphs in coloured graphs from the class using a fixed first-order formula, and monadically stable if one cannot even encode arbitrarily long linear orders. Bonnet et al. (ICALP 2025) characterised monadic dependence by flip-separability: for every vertex weighting, boundedly many flips - complementations of the adjacency relation within a vertex subset - make every ball of radius $r$ carry at most an $\varepsilon$-fraction of the weight, so that every set carrying an $\varepsilon$-fraction has two elements pulled apart. We introduce flip-packability: boundedly many graphs, each obtained from the input by boundedly many flips and all determined by the weighting before any set is presented, such that every set carrying an $\varepsilon$-fraction of the weight has $m$ elements pairwise far apart in one of them. The number of flips producing each graph depends on the radius alone; only the number of graphs depends on $\varepsilon$ and $m$. We prove that a class of graphs is flip-packable if and only if it is monadically stable, and $2$-flip-packable, that is, flip-packable with $m=2$, if and only if it is monadically dependent. The passage from two scattered elements to $m$ is thus exactly what separates the two notions. For monadically stable classes we show that the flipped graphs can be computed from the weighting in cubic time. Varying the three parameters of the definition - the sparsifying operation, the radius, and the number $m$ of elements scattered - produces eight known characterisations of sparse and dense graph classes from the same template. In each case $m$ separates a depth-like notion from its width-like relaxation: treedepth from treewidth, shrubdepth from cliquewidth, and monadic stability from monadic dependence.

Explore related subjects

cs.LO cs.DM math.CO math.LO

Keep this discovery

Explore connections, maps & timelines

BibTeX RIS

Ioannis Eleftheriadis. 2026-09-29. Flip-packability: uniform characterisations of tame graph classes. https://arxiv.org/abs/2609.33705

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

KEEP EXPLORING

Related papers

arXiv2026

Improved Tristate Multiplication With Formalization in Rocq

We give a new multiplication algorithm for tristate numbers improving upon the state-of-the-art implementation from the Linux kernel in terms of precision and formal proofs. Our algorithm is significantly more precise as shown by experimental evaluation (at the peak, giving better results in 95.59% cases compared to the previous work for 31-bit samples). Importantly, we achieve this additional precision with performance comparable to the previous algorithm, as demonstrated by benchmarks. Finally, we formalize and prove the soundness of the algorithm in the Rocq proof assistant, adding to the trust in the resulting implementation. Our algorithm is now part of the upstream Linux kernel. Our soundness proof in Rocq for the new multiplication algorithm works for all bit widths, while the SAT/SMT-based machine-checked proof accompanying the previous algorithm was restricted to 8 bits. We also provide Rocq proofs for the soundness and optimality of the newly added tnum union operation and the existing tnum addition algorithm from the Linux kernel. Our optimality proof for tnum addition presents a simpler and straightforward lemma compared to prior work.

cs.LO↗

arXiv2026

Observer Determinacy of Termination Certificates: Sufficient Statistics, Blackwell Comparison, and Simple Projections for Step-Duplicating Recursion

The recursor $F(x,y,0)\to x$, $F(x,y,S(n))\to G(y,F(x,y,n))$ terminates and is confluent under all contexts, yet every orienting expression of the stated direct-measure grammar ignores the copied argument $y$; a payload-sensitive orienter exists outside it. An observer $q:X\to Q$ licenses a target $P:X\to V$ when $P$ is constant on its fibers. For a sound and complete language whose observer sees the input dimension, operational inexpressibility is equivalent to two context-sharing worlds with equal observations and different target values; each hypothesis is necessary. The counter observer licenses an orienting target outside the grammar's definable class. On finite sets with a rational prior, the least weight refused by a repair with $k\ge1$ side symbols is $1-V_k(μ)$, where $V_k$ is the best probability of guessing the target within $k$ tries per observation; this curve is weakly decreasing and convex. For set-valued certificate tasks with a certificate at every state, the least side alphabet is the maximum fiber chromatic number of the hypergraph of subsets whose common certificate set is empty. Observer refinement equals deterministic Blackwell comparison, and licensing equals statistical sufficiency under deterministic observation and a full-support prior. In every faithful recursor realization, natural-valued root and extracted-call rankings each have infinitely many full-order classes, and counter-determined extracted-call rankings have one. The occurrence-role channel separates the active and frame copies of one payload and resolves one bit under the uniform binary law. Every signature homomorphism constant in the counter slot identifies two terms that the counter projection separates. The declared cost model gives quadratic omitted mass against linear residual work. The general results and recursor instances are formalized in Lean 4.

cs.LO↗

arXiv2026

New Proofs of Weak Normalization for Propositional Logic

We present new proofs of weak normalization for intuitionistic and classical propositional logics (with the full set of operators -- falsum, implication, conjunction and disjunction). These proofs work with cuts rather than cut segments, and they provide 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. Interestingly, much of the complication in the case of intuitionistic logic is due to the disjunction elimination rule, while our version of the same rule for classical logic has falsum as conclusion always, and so is much easier to handle. All the complication in the case of classical logic shifts to cuts involving the reductio ad absurdum rule. We also discuss a formalization of the entire proof in Lean, and present a deterministic algorithm for weak normalization.

cs.LO↗