Axiom-Audited Trustworthy Formalization of Game-Theoretic Commitment in Lean

As large language models increasingly generate proofs in Lean, Rocq, and Isabelle, a machine-checked proof's trustworthiness turns on two questions its script does not foreground: which foundational axioms it rests on, and where an external, unproved trust assumption enters. We answer both mechanically in a Lean 4 formalization of a game-theoretic commitment result, and from it extract two methods for trustworthy formalization that we argue transfer to verifying AI-generated and autoformalized mathematics. The first treats axiom hygiene as an executable regression test: #guard_msgs-guarded #print axioms assertions pin the foundational-axiom footprint of all 56 declarations (kernel+Classical only; no sorry, no custom axioms), so any drift fails the build with a mismatch. The second isolates the development's single trust assumption (that an external attestation faithfully reflects intent) in a TrustedOracle typeclass with an explicit truthfulness predicate, a worked instance, and a non-instance counterexample proving the obligation is non-vacuous. The case-study object is a dominance-and-equilibrium theorem: for every Stag-Hunt-ordered game, routing players through a verified wrap combinator makes attesting Cooperate weakly dominant, with mutual cooperation the unique Pareto-undominated Nash equilibrium. We prove this for the 2-player and n-player, symmetric and asymmetric cases, the 2-player results obtained by machine-checked specialization of the n-player ones.