AASC Yang-Mills Lean Audit Endpoint This release contains the dedicated Lean 4 archive for the AASC Yang-Mills local-net and Clay-extension audit. The purpose of this archive is to make the formal support for the Yang-Mills manuscript easier to inspect, build, and cite. It separates the Yang-Mills Lean work from the larger mixed AASC working repository and places the relevant theorem-routing, endpoint, seam-checking, and audit files in one focused release. What Was Verified The release was checked with: powershell -ExecutionPolicy Bypass -File scripts/check-yang-mills-a-plus-audit.ps1 That check confirms that: the Yang-Mills Lean package builds; the A+ audit files run successfully; the audited Yang-Mills files contain no live project-level axiom, sorry, admit, or unsafe; the release records exactly which Lean/mathlib environment was used. What This Archive Covers This archive formalizes the manuscript-facing proof route: the theorem-routing layer, the load-bearing seams, the endpoint handoff, and the audit-control structure used to connect the local-net construction to the Clay-extension endpoint. It is meant to support audit and reproducibility: a reader can see which Lean modules correspond to the claimed proof route and can rerun the verification script. Important Boundary This release does not claim to reprove every standard background theorem from first principles. Standard Lean/classical foundations and imported mathematical background remain part of the explicit boundary. In particular, dependency reports may mention standard foundations such as propext, Classical.choice, and Quot.sound. These are not project-specific Yang-Mills axioms. Environment Lean: leanprover/lean4:v4.28.0 mathlib revision: 8f9d9cff6bd728b17a24e163c9402775d9e6a365 Release tag: v1.0.1