Verified graphon-game aggregates, Nash equilibria and fixed-profile perturbation bounds

Five complete Lean formalizations in the exact Prove2Me real-action graphon-game model: best-response L2 sensitivity (Lemma 3.7), aggregate-profile L2 sensitivity (Lemma 3.16, display 15), aggregate existence and almost-everywhere uniqueness (Proposition 3.1), Nash equilibrium existence and almost-everywhere uniqueness under condition (17) (Proposition 3.17), and aggregate sensitivity under a change of graphon at a fixed action profile (Lemma 3.19). The player measure is Lebesgue probability on the unit interval. Kernels are symmetric, measurable, real-valued and square-integrable. The exact extended-real operator norm is proved finite before its real part is used. Assumption 1 imposes the squared Lipschitz bound and the stated mean-zero finite-second-moment noise law. Assumption 4 imposes C1 strong convexity in the real action and Lipschitz dependence of the action derivative on the aggregate. Aggregate existence requires sqrt(c_z)||W||<1; Nash uniqueness additionally requires (ell_J/ell_c)sqrt(c_alpha)||W||/(1-sqrt(c_z)||W||)<1. The fixed-profile perturbation target retains both contraction conditions and Assumption 5, the uniform positive bound c0 on |b|. The proof infrastructure checks selected-minimizer existence and uniqueness, nonlinear L2 closure, kernel-product integrability, exact operator bounds and contractions on complete L2 equivalence classes. The five complete original signatures and actual accepted bodies are included. Internal proof reuse is documented and is not counted as extra targets. Original mathematics: René Carmona, Daniel B. Cooney, Christy V. Graves and Mathieu Laurière, Stochastic Graphon Games: I. The Static Case, arXiv:1911.10664v1 (2019). Their Lemma 3.7 credits an estimate of Francesca Parise and Asuman Ozdaglar, Graphon games, arXiv:1802.00080 (2018), reference [26]; that predecessor attribution is retained. The pinned Carmona et al. PDF was inspected and hashed; papers are cited, not redistributed. mikedeng1 supplied platform formulations; Shuze Chen confirmed platform statements, not these proofs. Lean and Mathlib contributors retain foundational credit. The standalone packet contains five unchanged accepted proof sources, two platform definitions, independent full-type and every-local-declaration axiom audits, immutable Lean 4.33.1 and Mathlib pins, the established archive verifier, fresh reproduction logs and seven rejected controls. The controls cover all five target interfaces, an unused forbidden local axiom and modified proof bytes. Verification uses autoImplicit=false and only propext, Classical.choice and Quot.sound. Verified third-party compiled caches are trusted inputs. The claim covers real actions and the platform's pointwise Nash predicate, not general constrained actions or the rich Fubini-extension construction and its equivalence to this predicate. Theorem 3.20, full equilibrium sensitivity under graphon perturbations, remains outside this edition; the fixed-profile bound does not prove it. Finite-player approximation and pointwise estimate (16) are also excluded. Assumption 4 applies to the exact defined integral cost; no separate integrability premise for f is silently added. Alexander Richard Towell directed research and publication; OpenAI Codex substantially constructed, formalized, checked, submitted and documented the proofs and packet. Mathematical novelty, source-author endorsement and independent human proof review are not claimed. The original proof submissions and acceptances occurred on October 21, 2026; this archive is a separate publication event and adds no accepted target.