Local convex certificates for one-sided-information game values (C73-8)

Local convex-capital certificates characterize bounded Borel payoffs admitting a value at every prior in one-sided-information games. This deposit includes the hand manuscript and the later Claude-developed BorelValue Lean project at its pinned public commit, including the superhedging-duality development, exact convex-hull correspondence, bounded-payoff normalization and Verify.lean. The later source describes an unconditional formalization; the earlier conditional version is not used as the current formalization. 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 Lean development is attributed in its source to Claude Opus 5.5 and Claude Fable 5.1 (Claude Code). Source versions. borel-game-value-characterization — 4ea46a1e7f4c898860201c820a34a34cd5a465df borel-value-certificates-lean-20261011 — adfa513ba33427af32e3bca4a01f0a86a1086db4 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.