grassmannian

A Matlab toolbox with implementations of different Grassmannian constellation designs for noncoherent communications

A Lean 4-verified research programme on positive geometry and emergent spacetime, testing whether dimensionless Standard-Model quantities follow with zero fitted parameters. 1378 theorems, 0 non-standard axioms; papers on Zenodo.

Program that constructs all oriented matroids of the given rank and on the given number of elements.

COSMOS: learning as gauge dynamics on the Grassmannian. Reference implementation in Rust.

Deterministic local layer for permission, entitlement, route, and data-boundary sitting over Playwright, with Grassmann attention, and LLM-generated scenario-proposal workflows gated by a finite-state verifier.

Exact computation with cluster algebras in Julia: quiver and seed mutation, principal coefficients, finite-type classification, exchange graphs, green sequences, and Grassmannian cluster structures

Lean 4 (v4.34.1 / Mathlib) formalization of noncommutative information geometry, Peirce-Weyl units, Drazin-Moore-Penrose spectral splittings, Jordan-Lie operator algebras, and categorical inductive colimits.

Code, experiments and Lean 4 formalization for the paper "A Fast Algorithm for Subspace Convolution"

Matlab code for "Tree-structured quantization on Grassmann and Stiefel manifold", S. Schwarz et al., DCC 2021

Lean 4 proofs that the quantum geometric tensor Tr(ΠVW) is a Frobenius inner product, so its Gram matrix is positive semidefinite and the Berry curvature is bounded by the quantum metric, in every finite dimension.