A Survey of Symmetries Compression Must Respect
RoPE, SignPhase, BoundedArithmetic, DenseSparse, dormancy — a living catalogue of algebraic invariants that any compression scheme must preserve, with Lean 4 formal coverage.
-
A Catalogue of Symmetries Compression Must Respect
Compression schemes regularly violate algebraic invariants of weight structure—producing models that pass perplexity checks but fail downstream. Here are the five core symmetry types a formally verified survey is collecting.
-
A Survey as a Living Document
What it means to maintain a formal proof corpus that stays in sync with its own coverage badge, and what happened when RWKV was added as a new architectural family without invalidating existing theorems.