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.

1. A Catalogue of Symmetries Compression Must Respect

   Apr 26, 2026

   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.

   #ml-research #compression #symmetry #quantization #RoPE

2. A Survey as a Living Document

   May 3, 2026

   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.

   #ml-research #lean4 #formal-verification #RWKV #methodology