Nash Bargaining Characterization in Lean

Abstract — v1

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.