Python library containing tools for calculating asymptotic directions and vertical cut-off rigidities.

Fast algorithms on 2 dimensional rigidity and (k,l)-sparsity matroids. M-component hypergraph, transversal on the MCT sets and redundant augmentation in O(|V|^2) time and O(|V|) memory.

Lean4 flagship repository for the Unified Rigidity Framework. Canonical module layout, invariant-first design, and CI-stable proof skeletons used across URF projects.

Deterministic WL³-style sampling and collapsed obstruction witness for URF (CI-safe, format-robust).

Terminal obstruction (Cyclone) for locality-bounded computation: overlap-rank BOM, AKR CPD₁ kernel, entropy-depth lower bounds, and Lean formalization toward P≠NP.

Deterministic support-drift principle with bounded-capacity witness and reproducible artifacts

Certified minimal obstructions for graph and inference baselines under the Unified Rigidity Framework (URF).

Lean 4 development repository for overlap rigidity: local cycle-overlap invariants, FOᵏ locality interfaces, and executable proofs. Dev scaffold; authoritative artifacts released from the frozen repo.

Canonical counterexamples and boundary constructions for OWC-style rigidity and capacity–locality claims. Includes explicit witnesses, verification scripts, and documented failure modes to delineate admissible vs. non-admissible regimes.