What question did this study set out to answer?

This work aims to present a formalized software archive for the NEMS program, emphasizing new modules and zero custom axioms.

June 3, 2026Open Access

UGP/GTE Lean formalization

Key Points

This work aims to present a formalized software archive for the NEMS program, emphasizing new modules and zero custom axioms.
Bundled a pinned Git snapshot with 283 modules
Merged with ugp-lean-exp to add 52 new modules
Included named axioms related to computational simulation and physics
New modules cover various aspects like TemporalVoxelCC and EtherProperTimeRate
All core modules reported to have zero apologies for errors
Introduced complete QG/cosmology arc from P44 to P47

Abstract

Lean 4 software archive for the **NEMS** program: **Lean Ugp**. This Zenodo record bundles a pinned Git snapshot of the formalization (283 modules, zero sorry, zero custom axioms on core path). Merged with ugp-lean-exp on 2026-05-30 (52 new modules since v2026-05-27). New modules include TemporalVoxelCC, CKMCPPhase, PhiMDLProperTimeBridge, EtherProperTimeRate, and the full QG/cosmology arc (P44-P47). All core modules zero sorry; named axioms: rccₚhysicsₐx, rule110ₛimulatescomputable, simultaneousdualₜapeₐx. 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ᵢdentifiers`.

UGP/GTE Lean formalization

Key Points

Abstract

Cite This Study