Skip to content

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

Latest

Choose a tag to compare

@krystophny krystophny released this 11 Sep 13:52
· 33 commits to main since this release
v0.3.2
c379bbd

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.