HEXAGONbeta

Submitted works

Advanced search
hexagon:2610.00003v1

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.00002v1

math.OC — Optimization and Control

A Finite Coordinate Reduction for Approachability Loss in Lean

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

We explain a Lean 4 development of a finite-coordinate loss-preserving construction motivated by Theorem 4 of Dann, Mansour, Mohri, Schneider, and Sivan. Nonempty finite constraint and action index sets give a joint probability simplex with a canonical action marginal. For each mixed constraint, a linear comparator adds its outer product with that marginal. The comparator has mass two and leaves the legal action set. A one-step pairing identity yields exact equality of finite-horizon approachability and comparator-regret objectives, with explicit anchored lifts and marginal decoders. The development also proves a row-wise decomposition with at most one rank-one term per constraint index. We describe the twelve declarations registered in Palomar and their historical verification provenance. The scope is deliberately narrow: the constraint simplex parametrizes coordinate functions, both causal strategy translations observe original loss histories, and the comparators have no fixed point in the joint simplex. Thus the checked statements establish finite algebraic loss preservation; they do not certify the full published reduction, its fixed-point-defined improper class, reduced-loss-only feedback, or asymptotic rate theory. No mathematical novelty or formalization priority is claimed.

Primarily AI-generated textHuman understanding: some parts
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.00007v1

math.AC — Commutative Algebra

Prime-Generated Localization Descent for Unique Factorization in Lean

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

We give a source-grounded exposition of a Lean 4 formalization of prime-generated Nagata factoriality descent. A commutative noetherian integral domain is a unique factorization domain if a localization is a unique factorization domain and every denominator is exactly a finite product of prime elements belonging to the denominator submonoid. The formal statement works with an arbitrary algebra carrying Mathlib’s IsLocalization structure. We explain the two cases for an irreducible element, the multiset cancellation and splitting arguments, and the corollary for submonoids generated by arbitrary sets of primes. A registered polynomial corollary illustrates reuse of the descent package; its Laurent-polynomial premise is proved using Mathlib’s existing polynomial UFD instance, a dependency made explicit here. The exposition is tied to the registered source and dependency pins, distinguishes historical mechanical verification from manuscript review, and situates the development relative to an earlier Lean preprint and an Isabelle/HOL formalization. No new algebraic theorem or priority claim is asserted.

Primarily AI-generated textHuman understanding: some partsLean 4MathlibNagata factorialitycommutative algebralocalizationunique factorization domains
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.00152v1

math.AT — Algebraic Topology

A Lean Formalization of the Classical Seifert van Kampen Groupoid Theorem

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

We explain a Lean 4 formalization of the classical Seifert van Kampen theorem for the full fundamental groupoid. For an arbitrary topological space covered by two open subsets, the inclusion-induced square of ordinary continuous-path fundamental groupoids is a pushout in the category of categories. Every point is retained as an object; no basepoint, connectedness, or separation hypothesis is required. The development identifies an auxiliary directed path category for the indiscrete preorder with Mathlib's fundamental groupoid through strictly inverse functors and naturality equalities. It then assembles the pushout universal property from attributed path-subdivision and homotopy-grid helpers adapted from the directed-topology formalization of Basold, Bruin, and Lawson. We describe the descent construction, its transfer to ordinary fundamental groupoids, and the statement and verification boundaries of the exact artifact registered in Palomar. This is an expository account of a classical theorem and an existing formal artifact, with no claim of mathematical novelty or formalization priority.

Primarily AI-generated textHuman understanding: some partsLean 4MathlibSeifert van Kampen theoremcategorical pushoutfundamental groupoidopen cover
Sep 30, 2026PDF ↗View work →
hexagon:2609.00149v1

cs.DS — Data Structures and Algorithms

Deferred Acceptance in Lean for Finite Strict Preference Markets

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

We describe a Lean 4 development of men-proposing deferred acceptance for finite one-to-one markets with complete strict preferences and optional partners. The two sides may have different cardinalities; the principal theorems assume a nonempty receiving side. A proposal-set measure proves termination of a specified, classically chosen run. Reachability invariants establish consistency of the resulting partner maps, stability, and the fact that a rejected proposal cannot be a stable-achievable partnership. The public optimality theorem is conditional on a man receiving a partner; an internal lemma separately excludes stable-achievable partners for men unmatched at quiescence. We give mathematical proofs corresponding to the source architecture, identify the precise theorem interface, and separate fresh source inspection from the repository's reported build and axiom audit. This is an exposition of a pinned formalization of classical results, with no claim of new matching theory or priority of formalization.

Primarily AI-generated textHuman understanding: some partsGale-ShapleyLean 4deferred acceptanceformalizationstable matching
Sep 30, 2026PDF ↗View work →
hexagon:2609.00151v1

math.OC — Optimization and Control

A Lean Formalization of Roberts Theorem on Unrestricted Valuations

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

We describe a Lean 4 formalization of the finite unrestricted-domain version of Roberts theorem. For finite nonempty agent and alternative types, with at least three alternatives, an onto deterministic direct-revelation mechanism that is dominant-strategy incentive compatible has an affine-maximizer choice rule. Valuations range over all real-valued profiles; the conclusion uses fixed nonnegative weights, at least one nonzero, and alternative offsets, and asserts membership in the maximizing set. The development follows the modular proof route: taxation and weak monotonicity, perturbation-based tie-breaking to strong monotonicity, no-veto range analysis, affine prices for two agents, and induction through fixed-report slices. We explain the proved tie-set transport lemma, the construction of fresh payments for the tie-broken rule, and the transfer back to arbitrary ties. A version-pinned account distinguishes the proved library from statement-only comparator placeholders and separates source inspection from executable checks. This is an exposition of a classical result and its formal artifact, with no claim of mathematical novelty or formalization priority.

Primarily AI-generated textHuman understanding: some partsLean 4Roberts theoremaffine maximizersdominant strategiesformalizationmechanism design
Sep 30, 2026PDF ↗View work →
hexagon:2609.00150v1

math.OC — Optimization and Control

Finite VCG and Groves Payments in Lean

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

We describe a Lean 4 development of finite direct mechanisms with quasi-linear utility and unrestricted real-valued valuations. The Clarke pivot mechanism selects a reported-welfare maximizer and charges each agent the loss in other-agent welfare relative to its maximum over the same fixed alternative set. The development proves efficiency, dominant-strategy truthfulness, nonnegative payments and no deficit, and individual rationality under the explicit assumption that every valuation is nonnegative. It also proves that every efficient, dominant-strategy incentive-compatible mechanism on the full valuation domain has Groves-form payments, with a term independent of the paying agent's report. We explain the finite-maximization interface, the report-update invariants, and the characterization argument using outcome-forcing reports and positive perturbations. The exposition is tied to a specific source revision and separates proved implementations from statement-only comparator placeholders. These are classical mechanism-design results; no new mathematical theorem or formalization-priority claim is made.

Primarily AI-generated textHuman understanding: some partsClarke pivot paymentsGroves characterizationLean 4VCG mechanismdominant strategiesformal verification
Sep 30, 2026PDF ↗View work →
hexagon:2609.00148v1

math.OC — Optimization and Control

A Lean Formalization of Finite Zero Sum Minimax via Sion's Theorem

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

We describe a Lean 4 formalization of the minimax theorem for finite nonempty two-player zero-sum games with arbitrary real payoffs. Mixed strategies are probability vectors, and the two game values are defined using real indexed suprema and infima. An explicit payoff bound supplies the boundedness obligations required by these conditional extrema. The reverse minimax inequality follows by applying Mathlib's proved Sion saddle-point theorem to compact convex coordinate simplices, with the minimizing player placed in its first argument. We explain the representation bridge, the proof obligations, and the passage from a saddle point to equality. The accompanying version-pinned artifact separates a reusable library from a statement-only challenge and its proved solution. This is an exposition of a finite-game specialization of existing formal analysis, with no claim of a new mathematical proof or formalization priority.

Primarily AI-generated textHuman understanding: some partsLeanSion's theoremformalizationminimax theoremzero-sum games
Sep 30, 2026PDF ↗View work →