Verified Neural Compilation

Classifying the RoPE commutant, multi-head foldability, and formalizing the architectural boundaries of key-only routing.

1. Classifying the RoPE Commutant: Symmetry in Verified Neural Compilation

   Apr 25, 2026

   The algebra of which orthogonal transformations survive RoPE at zero cost, derived from the Symmetry.lean formalization.

   #research #rope #geometry #lean

2. Multi-Head Foldability: Scaling Verified Compilation

   May 3, 2026

   Lifting single-head RoPE proofs to multi-head bundles and residual wrappers in the Verified Neural Compilation project.

   #research #lean #rope #attention

3. The Impossibility of Key-Only Routing: An Architectural Boundary

   May 10, 2026

   Formalizing why MoE routers must depend on residual-stream state rather than key-only summaries.

   #research #moe #architecture #lean