algebraic-analysis v0.3.2 — filtered-ring layer and shared Hessian package

v0.3.2: filtered-ring layer and shared Hessian package

Mathematics release at 8c1c96e09d15a39e80f31d28522e96a3a252425c. Lean
v4.33.0 and Mathlib db584cd6d46c92f209a44c0f1c829460d327499d are unchanged
from v0.3.1.

Filtered-ring, Hilbert-function and Gelfand–Kirillov layer

New AlgebraicAnalysis.Filtration.* modules:

• RingFiltration: ascending, exhaustive, unital, submultiplicative ring
  filtrations over a commutative base ring, their associated graded pieces
  with well-defined multiplication, and the order function with its
  subadditivity under products and sums.
• GoodFiltration: compatible and good filtrations on a module over a
  filtered ring, existence for finitely generated modules, and the comparison
  lemma that any two good filtrations lie inside a bounded shift of each
  other.
• HilbertFunction: Hilbert functions of filtrations by finite-dimensional
  subspaces and their growth degree, valued in the extended reals so that
  superpolynomial growth is not collapsed onto the bounded case; the growth
  degree is invariant under bounded shifts.
• GKDimension: Gelfand–Kirillov dimension from that growth degree, the exact
  Hilbert-function count finrank (m + n).choose n of the total-degree
  filtration on a polynomial ring in n variables, and dimension exactly n.
  The Bernstein inequality is stated as a named proposition and deliberately
  left unproved; it is the open target of the layer.

Shared HessianAlgebra package

The neutral AlgebraicAnalysis.HessianAlgebra.* modules (polynomial self-map
calculus, derivative kernel, affine and triangular inverses, coordinate and
Hessian transport, constant-Hessian and homogeneous-support results) now live
under stable package module paths with a dedicated AlgebraicAnalysisHessian
library root. They are extracted from hc6-formal; source revisions,
declaration mappings and downstream consumers are recorded in
docs/provenance.yaml.

Verification and release boundary

The library and test targets build cleanly on the pinned toolchain. Every new
public statement depends only on propext, Classical.choice and
Quot.sound; no project axiom or sorry is introduced. This release does not
claim a Palomar registration or an independent human proof audit; the
downstream -formal repositories remain the authority for their own
mathematical status. The Zenodo DOI for v0.3.2 is recorded in
docs/release-history.md only after the archival identifier is issued.

algebraic-analysis v0.3.1 — literature and proof sources

v0.3.1: literature and source index

The README now displays the principal literature and links to a source-to-Lean
index. Module docstrings identify the mathematical context and exact source
roles. The index also distinguishes proved APIs from conditional literature interfaces.

Mathematical declarations, imports, frozen Challenges, Comparator configurations,
and dependency pins are unchanged. Lean edits affect comments only, checked
against the preceding commit with a nested-comment-aware comparison. Historical
verification reports retain their original source commits; this documentation
release does not claim a new independent mathematical replay or Palomar version.

Validation: local Markdown targets, reference keys, graph dependencies (where
present), release metadata and whitespace checks; both formal-repository PDFs
were rebuilt with resolved citations and no overfull boxes or missing glyphs.

AlgebraicAnalysis v0.3.0

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.

AlgebraicAnalysis v0.1.0 — historical dependency archive

Historical AlgebraicAnalysis v0.1.0 source snapshot at 2fdc928835347a2638b6c85a4bfa770e3f70ed9e, used by Stafford38 formal v1.0.0 and v1.0.1.

This archival tag and release were created on 2026-09-08 to preserve the earlier dependency version on Zenodo. They do not imply that this GitHub tag existed at the time of the original verification. The source package already identified itself as version 0.1.0; no source file or historical dependency pin was changed.

Historical dependencies: Lean v4.33.1, Mathlib 0df444a360eaa60ab8c11dca51a86af692955474. This is an archival deposit, not a new verification under current dependencies. The current downstream releases use the newer cacheable Lean/Mathlib v4.33.0 stack and the new library release. License: Apache-2.0.

AlgebraicAnalysis v0.2.0

Reusable Lean 4 foundations for algebraic analysis: derivation-Ore extensions,
differential operators, filtered modules and their two-term pages, localization,
rank and length arguments, and hyperplane restriction.

This release builds against Lean v4.33.0 and Mathlib
db584cd6d46c92f209a44c0f1c829460d327499d, a commit on Mathlib's master
branch. The previous pin was Mathlib's v4.33.1 tag, which exists only on the
stable branch; the two Mathlib commits differ by one line in Mathlib's own
lean-toolchain file, so no Mathlib mathematics changed. The move keeps this
library usable by downstream projects that require a Mathlib revision reachable
from master.

Apache-2.0.

Exact source commit: dfdd2da091a9d67e7a29cc7914f192d746a2400d. This is the library release pinned by Stafford38 formal v1.0.2. The signed tag and source archive retain their original contents.