Matching works

10 works

math.LO — Logic

Arrow and Gibbard Satterthwaite Theorems in Lean

Contributed by Arthur, David Barros Hulak, Ruy J. G. B. de Queiroz

We give a source-aligned account of two Lean 4 formalizations of classical finite social-choice impossibility theorems. For a finite nonempty electorate and a finite alternative set containing three distinct alternatives, Arrow’s theorem derives dictatorship from unanimity and independence of irrelevant alternatives. Its proof expands a weakly decisive coalition from one ordered pair to all pairs, then contracts decisive coalitions to a singleton. The Gibbard–Satterthwaite development proves that every onto strategy-proof choice function on the unrestricted strict-ranking domain is dictatorial by constructing a social welfare function and applying that Arrow implementation. We explain the essential construction in full: top-two profiles define pairwise comparisons; strategy-proof monotonicity and three-top profiles establish a strict total order; predecessor counts provide injective natural-number ranks. Exact hypotheses, vendored dependencies, pinned source identities, prior formalizations, and the distinction between historical registry verification and the present source audit are recorded. The contribution is an exposition and audit of reusable formalization artifacts, not a new social-choice theorem or a claim of first formalization.

Primarily AI-generated textHuman understanding: some parts

Oct 01, 2026PDF ↗View work →

hexagon:2610.00004v1

math.LO — Logic

A Lean Formalization of the Shapley Value Characterization for Finite Cooperative Games

Contributed by Arthur, David Barros Hulak, Ruy J. G. B. de Queiroz

We describe a Lean 4 formalization of the standard four-axiom characterization of the Shapley value for finite transferable-utility cooperative games. Games are arbitrary real-valued characteristic functions normalized at the empty coalition; the player type may itself be empty. The factorial coalition formula is proved efficient, symmetric for interchangeable players, null-player respecting, and additive. Uniqueness follows from the values of arbitrarily scaled unanimity games and an explicit Boolean-lattice Möbius decomposition. The proof requires neither a real-homogeneity axiom nor a continuity assumption on competing allocation rules. We explain the finite-sum arguments, the precise Lean statements, the separation between the registry’s challenge and implemented solution, and the historical verification evidence for the pinned source revision. The contribution is an auditable exposition of an existing formalization of classical mathematics, with no claim of new mathematics or formalization priority.

Primarily AI-generated textHuman understanding: some parts

Oct 01, 2026PDF ↗View work →

hexagon:2610.00005v1

math.LO — Logic

Nash Bargaining Characterization in Lean

Contributed by Arthur, David Barros Hulak, Ruy J. G. B. de Queiroz

We describe a Lean 4 formalization of the classical two-person Nash bargaining characterization. A bargaining problem consists of a compact convex subset of the real plane, a feasible disagreement point, and a feasible outcome strictly improving both utilities. The Nash product is maximized over the individually rational part of that set. The development proves existence and uniqueness of the maximizer, verifies Pareto optimality, symmetry, positive affine invariance, and independence of irrelevant alternatives, and proves that these four axioms characterize the maximizer among feasible selection rules. We explain the algebraic midpoint proof of uniqueness and the normalization argument, including an explicit small-step tangent bound and a compact symmetric enlargement. The exposition is tied to an immutable repository snapshot and four declarations registered in Palomar. Historical registry verification is distinguished from the source inspection used to prepare this manuscript. The contribution is a documented formalization of established mathematics; no new bargaining theorem or formalization-priority claim is made.

Primarily AI-generated textHuman understanding: some parts

Oct 01, 2026PDF ↗View work →

hexagon:2610.00008v1

math.LO — Logic

Finite Nash Equilibria and Dependent Mixed Strategies in Lean

Contributed by Arthur, David Barros Hulak, Ruy J. G. B. de Queiroz

We present two complementary Lean 4 developments of finite Nash equilibrium. The pure-game layer uses player-specific legal action sets, distinguishes one-way generalized ordinal potentials from bidirectional ordinal potentials, and proves potential-maximizer certificates, a local-maximum characterization, absence of strict-improvement cycles, and weak acyclicity. The mixed-game layers use either a common finite action type or a dependent finite action type for each player. They prove payoff equalization on equilibrium supports, Dirac payoff identities, continuity of the normalized payoff-excess map, and mixed equilibrium existence. We explain the finite-sum and sum-of-squares arguments and the reindexing bridge to an attributed, proved product-of-simplices Brouwer theorem. An additional legal-subtype interface is separated from the declarations selected by the registry comparator. The account is tied to two immutable source snapshots and dated verification records. It documents established mathematics and its formal interfaces, without claiming a new equilibrium theorem or formalization priority.

Primarily AI-generated textHuman understanding: some partsBrouwer fixed pointLean 4MathlibNash equilibriumdependent action typesmixed strategiespotential games

Oct 01, 2026PDF ↗View work →

hexagon:2610.00006v1

math.GR — Group Theory

An Executable Stallings Recognizer for Finite Generating Lists in Lean

Contributed by Arthur, David Barros Hulak, Ruy J. G. B. de Queiroz

We explain a Lean 4 construction of a finite inverse automaton recognizing the subgroup of the rank-two free group generated by any finite list of signed words. The implementation builds a flower multigraph and computes the least equivalence relation compatible with deterministic labelled transitions by exhaustive finite search over Boolean relations. Canonical representatives realize the folded graph on the original finite state type. A coset-potential invariant proves that folding introduces no additional subgroup elements; preservation of the input loops proves the opposite inclusion. A separate reduction argument shows that traversal of the canonical reduced representative decides membership. We distinguish the registered theorem, its executable witness, and classical reasoning used only in the proof. The construction retains unused states and has no formalized complexity, core-trimming, subgroup-basis, intersection, or index algorithm. This is an expository account of a classical recognition theorem and a pinned formal artifact, with no claim of mathematical novelty or formalization priority.

Primarily AI-generated textHuman understanding: some partsLean 4MathlibStallings foldingfinite inverse automatafree groupssubgroup membership

Oct 01, 2026PDF ↗View work →

hexagon:2610.00001v1

cs.LO — Logic in Computer Science

A Lean Formalization of Myerson-Satterthwaite Impossibility for Continuous Bilateral Trade

Contributed by Arthur, David Barros Hulak, Ruy J. G. B. de Queiroz

We present a source-grounded account of a Lean 4 formalization of the Myerson-Satterthwaite impossibility theorem for continuous bilateral trade. Buyer values and seller costs are independent, with atomless probability measures supported on compact real intervals whose interiors overlap. The model explicitly requires restricted Lebesgue measure to be absolutely continuous with respect to each type measure, together with full support; it does not require the type measures themselves to have densities. Under allocation and transfer measurability and integrability conditions, the registered theorem excludes the simultaneous satisfaction of almost-sure ex post efficiency, Bayesian incentive compatibility at every admissible type and report, interim individual rationality, and weak ex ante budget balance. The proof derives envelope identities from incentive inequalities, identifies the efficient allocation almost everywhere, and uses a layer-cake representation to show that the required information rents strictly exceed efficient surplus. We explain the analytic steps, their Lean declarations, and the verification evidence for the exact Palomar-registered source revision. This is an exposition of a classical result and an existing formal artifact, without a claim of mathematical novelty or formalization priority.

Primarily AI-generated textHuman understanding: some parts

Oct 01, 2026PDF ↗View work →

hexagon:2610.00009v1

cs.DS — Data Structures and Algorithms

A Lean Certificate for the Single Source Unsplittable Flow Cost Counterexample

Contributed by Arthur, David Barros Hulak, Ruy J. G. B. de Queiroz

We explain a standalone Lean 4 and Mathlib verification of the finite counterexample announced by Dmitry Rybin to the cost-preserving single-source unsplittable-flow conjecture. The instance has seven vertices, nine directed arcs, and three terminal demands. An exact rational path flow saturates every arc, has cost 58, and has largest demand 15. Exhaustive graph-path classification reduces every unsplittable routing to two choices per terminal. Three backbone-arc inequalities force any routing with load at most the fractional load plus 15 to use at least two paid routes, each costing 30. Thus every such routing costs at least 60, ruling out cost preservation even with a non-strict congestion bound. We present the numerical certificate, its graph realization, and the boundary between the pinned proved implementation and its statement-only verification interface. The contribution is an exposition of a source-based formal certificate; no new counterexample, first formalization, or general rounding algorithm is claimed.

Primarily AI-generated textHuman understanding: some partsGoemans cost conjectureLean 4MathlibRybin counterexamplefinite counterexampleformal verificationsingle-source unsplittable flow

Oct 01, 2026PDF ↗View work →

hexagon:2609.00141v1

math.LO — Logic

Ordinal-definable families in Cohen, random, and collapse extensions

Contributed by Elliot Glazer

We study ordinal-definable families of sets of arbitrary rank in Cohen, random, and collapse extensions. Over $L$ , countable OD families have OD enumerations after adding one Cohen or one random real. A single generalized Cohen subset gives the corresponding sharp theorem at every regular uncountable cardinal. When $\kappa$ is singular strong limit and has uncountable cofinality, adding $\kappa$ Cohen reals makes every member of a short-parameter definable family of size at most $\kappa$ definable from a short parameter. Adding $\kappa$ random reals gives a single short-parameter definable enumeration for every such family of size strictly below $\kappa$ . The random bound is sharp. The proofs use coordinate amalgamation and small-index arguments. We also obtain arbitrary-rank descent for countable families after collapsing any infinite cardinal, with applications to choice in the relative Feferman--Levy model. In the full Solovay collapse extension of an arbitrary ZFC ground, every family definable from a real and ordinals that represents fewer than $2^{\mathfrak c}$ classes modulo null sets consists of measurable sets; the corresponding category assertion also holds. In the extensions of $L$ by $\omega_1$ Cohen or random reals, no model of $I\Delta_0$ of size at most $\aleph_1$ , definable from ordinals and a real, has full binary-coded standard system. $\Pi^1_1\text{-}\mathsf{CA}_0$ proves a finite-fragment Borel obstruction to a full binary standard system for $I\Delta_0$ . For regular uncountable $\kappa$ , the generalized Cohen extension by $\Add(\kappa,\Lambda)^L$, $\Lambda>\kappa$ , has no ambiently $\kappa^+$ -saturated $I\Delta_0$ model in $\operatorname{HOD}_{H_{\kappa^+}}$ , regardless of its size. Consequently every infinite regular $\kappa$ of $L$ admits a cofinality-preserving GCH extension with no $\mathrm{OD}_{\mathcal P(\kappa)}$ saturated arithmetic presentation of size $\kappa^+$ . ZFC also proves that every singular strong limit $\kappa$ admits an OD $\kappa^+$ -saturated elementary extension of $\mathbb N$ of size $2^\kappa$ , hence of size $\kappa^+$ under GCH.

Primarily AI-generated textHuman understanding: some partsBoolean algebrasSet theorydefinability

Sep 30, 2026PDF ↗View work →

hexagon:2609.00134v1

math.LO — Logic

Five equations for first-order logic, modulo the structure of existential graphs

Contributed by Anthony Hart

Peirce’s existential graphs draw a first-order formula so that the order and grouping of conjuncts, the names and order of bound variables, the position of a quantifier relative to conjuncts that do not mention its variable, and how a network of equalities is written cannot be seen. We take these structural laws for granted. On top of them, five two-way laws are complete for ordinary first-order logic with equality over nonempty domains. That is, any two equivalent formulas are connected by applying the laws inside them, in either direction. The laws are double negation, deiteration X ∧ ¬(X ∧Y ) ⇔ X ∧ ¬Y , annihilation ⊥ ∧ X ⇔ ⊥, substitution of equals, and existential introduction X(a) ∧ ∃u.X(u) ⇔ X(a), and none of them follows from the other four. The first three were already known to be complete for the propositional part. We prove first-order completeness by reduction to Tarski’s representation theorem for locally finite cylindric algebras. A size-ordered search over first-order laws, run up to size 5, kept four of the five; deiteration has size 7 and was added by hand. We also show that a published basis for Spencer-Brown’s boundary algebra is incomplete.

Primarily AI-generated textHuman understanding: all partscylindric algebraexistential graphsfirst-order logic

Sep 29, 2026PDF ↗View work →

hexagon:2609.00114v4

math.LO — Logic

Under Measurables, HOD_{Ord^{\omega}} is locally arbitrary

Contributed by Elliot Glazer

For the inner model HOD_{Ord^{\omega}}, we derive an analogue for Roguski's classical result that without nontrivial assumptions on V, HOD is an arbitrary model ZFC model. For any sentence \sigma, letting CM denote "class of measurables," the following theories are equiconsistent: (1) ZFC + CM + [HOD_{Ord^\omega} \models (\exists \kappa V_{\kappa} \models \sigma)]; (2) ZFC + GCH + CM + [HOD_{Ord^\omega} \models (SVC \wedge CM \wedge \exists \kappa V_{\kappa} \models \sigma)]; (3) ZF + DC + CM + \exists \kappa V_{\kappa} \models \sigma. Thus, under measurables we have that HOD_{Ord^{\omega}} is "locally arbitrary."

Primarily AI-generated textHuman understanding: some partsSet theoryaxiom of choice

Sep 28, 2026PDF ↗View work →

math.AC — Commutative Algebra
math.AG — Algebraic Geometry
math.AP — Analysis of PDEs
math.AT — Algebraic Topology
math.CA — Classical Analysis and ODEs
math.CO — Combinatorics
math.CT — Category Theory
math.CV — Complex Variables
math.DG — Differential Geometry
math.DS — Dynamical Systems
math.FA — Functional Analysis
math.GM — General Mathematics
math.GN — General Topology
math.GR — Group Theory
math.GT — Geometric Topology
math.HO — History and Overview
math.IT — Information Theory
math.KT — K-Theory and Homology
math.LO — Logic
math.MG — Metric Geometry
math.NA — Numerical Analysis
math.NT — Number Theory
math.OA — Operator Algebras
math.OC — Optimization and Control
math.PR — Probability
math.QA — Quantum Algebra
math.RA — Rings and Algebras
math.RT — Representation Theory
math.SG — Symplectic Geometry
math.SP — Spectral Theory
math.ST — Statistics Theory
cs.CC — Computational Complexity
cs.CG — Computational Geometry
cs.DM — Discrete Mathematics
cs.DS — Data Structures and Algorithms
cs.FL — Formal Languages and Automata Theory
cs.IT — Information Theory
cs.LO — Logic in Computer Science
cs.MS — Mathematical Software
cs.NA — Numerical Analysis
cs.SC — Symbolic Computation
math-ph — Mathematical Physics
quant-ph — Quantum Physics
stat.TH — Statistics Theory