Skip to content

Releases: israelflores8789/eig3x3-lean

Release list

v1.0.0

Choose a tag to compare

@github-actions github-actions released this 02 Sep 02:03
f65cd35

Added

  • Closed-form eigendecomposition of 3x3 real symmetric matrices in pure Lean 4
    over Float, with no Mathlib dependency
  • Eigenvalues via the Habera-Zilian (2025) closed-form method
  • Eigenvector construction following Eberly's (2014) r0 × r1 cross-product
    convention
  • Core types: SymmMat3, Vec3, Mat3, and Decomposition (with
    eigvals and eigvecs fields)
  • Numerical certificate checks at maximum justified machine precision:
    residual, orthonormality, reconstruction, determinant, and eigenvalue
    ordering
  • Python parity test suite validating results against NumPy/LAPACK
  • Supported on Lean toolchains v4.27.0, v4.30.0, and v4.34.0-rc2