Local capital geometry for maxmin concavification (C73-17)

Abstract

A local-capital-geometry characterization of equality between the informed-player maxmin and concavification at every prior. The additional Lean project formalizes the criterion using the nonrevealing lower value; its README explains the relationship to the complete-information game value and the manuscript's determinacy reference. Contents. Original proof PDF and LaTeX source, a complete research archive with pinned GitHub source snapshots and existing release assets, and a provenance manifest. The archive retains available verification records, source audits, reproducibility instructions and Lean source files. Original files are preserved byte-for-byte. Status. Author-submitted preprint and accompanying research materials. GitHub submission and Zenodo deposit do not constitute independent peer review or catalogue acceptance. This deposit records the existing results and their stated scope; archival checks do not certify mathematical correctness or replace a Lean build. AI use. The hand-proof manuscript and its supporting research materials were developed with GPT Codex assistance, including proof development and AI-assisted checks, as documented in the original repository. These checks are not represented as independent human peer review. The additional Maxmin Lean development is attributed to Claude Fable 5.1; its BorelValue library is attributed to Claude Opus 5.5 and Claude Fable 5.1. Source versions. maxmin-concavification-characterization — 448392472b35ef2303148f78fbbd819147bab774 maxmin-concavification-lean-20261011 — 66e4210bc876a338361f97dfdd041b9a81747794 Rights. CC BY 4.0 applies to the author-controlled materials that did not already carry a license. Existing file-level licenses, copyright notices and third-party attributions remain in force. Original manuscript and repository files have not been edited for this deposit.