UGP/GTE Lean formalization

Lean 4 software archive for the **NEMS** program: **Lean Ugp**. This Zenodo record bundles a pinned Git snapshot of the formalization (229 modules, zero sorry, zero custom axioms on core path). Includes new Universality layer (P28 Computational Universality results: TwoLayerConfluence, GTECompilation, GTEUniqueness, GoEHierarchy, PSCUniversality, HypothesisB, HypothesisBCChain, CUP3DPSCUnification, CUP3DPhysicalIncompleteness), BraidAtlas layer (P29 Dark Sector results: MirrorWindingNumber, EWBosonRHNConnection, RHNGapTheorem, DarkBraidAtlas, DarkQuarkCharge), QG/Phi_MDL arc (P38-P43: StressEnergyTensor, GravitonFockSpace, GeodesicTheorem, ZGMMesInvariant, Z7ZeroSectorDiscriminant, GaugeInvariance, ChiralPairVA, PSCOrbitWindows, AsyncLiftingTheorem, and more), and 99 additional modules since the 2026-05-18 release. rule110-lean dependency added at commit 9ac43e3. All core modules zero sorry; named axioms: rcc_physics_ax, rule110_simulates_computable, simultaneous_dual_tape_ax. Exact file scope and revision policy appear in the repository manifest shipped with the archive. Cite using the Zenodo DOI after publication. When available, add companion articles or public repository URLs to Zenodo `related_identifiers`.