Skip to content

AlgebraicAnalysis v0.3.0

Choose a tag to compare

View all tags
@krystophny krystophny released this 08 Sep 20:37
· 41 commits to main since this release
v0.3.0
This tag was signed with the committer’s verified signature.
krystophny Christopher Albert
SSH Key Fingerprint: ARNu2jnP8I1sJSIRgpYCbp5/cwEB8FqKnMf0gYdIy5U
Verified
Learn about vigilant mode.
4aae479
This commit was signed with the committer’s verified signature.
krystophny Christopher Albert
SSH Key Fingerprint: ARNu2jnP8I1sJSIRgpYCbp5/cwEB8FqKnMf0gYdIy5U
Verified
Learn about vigilant mode.

AlgebraicAnalysis v0.3.0 provides the shared Lean foundations for the corrected Stafford38 and Global Stafford formalizations. It includes finite-order coordinate generation for differential operators and generic regular-action faithfulness, together with the existing Ore, localization, filtered-module, and rank interfaces.

The mathematical source is the successor of v0.2.0 at 44921f5914c5dbd40d2d532c2867adce0f519cb9; the release commit adds publication metadata and verification evidence. Lean remains v4.33.0, with the official Mathlib v4.33.0 commit db584cd6d46c92f209a44c0f1c829460d327499d. Mathlib artifacts were successfully downloaded from the public cache.

The release history records the older exact library pins used by Stafford38 and Global Stafford. Those historical snapshots and the v0.2.0 tag are retained. The coordinated downstream candidates pin the full v0.3.0 release commit. Their releases follow their own verification gates. License: Apache-2.0. See the attached verification record and checksums for the checks performed.

Zenodo: https://doi.org/10.5281/zenodo.22666517. All 111 files in the deposited source ZIP match the exact v0.3.0 Git tree. Historical v0.1.0 and v0.2.0 are archived at https://doi.org/10.5281/zenodo.22666361 and https://doi.org/10.5281/zenodo.22666206 respectively.

Assets 5
Loading