SYMMETRY SURVEY · v0.1 DRAFT · APR 2026
Preprint Lean 4 · Mathlib — symmetry classes — theorems

Verified neural compilation of RoPE and gauge equivalences in transformers.

Transformer weights admit non-trivial symmetries — RoPE-commuting rotations, sign / phase gauges, parabolic stabilizers, observable quotients, and probe-induced fake equivalences — under which the function the network computes is preserved exactly or up to a measured budget. This survey catalogs the ones we have isolated so far, with each formalised as a Lean theorem and each fake symmetry surfaced as a refinement test against finer probes.

—
Theorems proven
—
Symmetry classes
—
Deferred
FIG 1 · Taxonomy of 12 symmetry classes · EDGES = subsumption / composition ■ gauge-free   ■ training-invariant   ■ probe-fake
§ 02  ·  CATALOG

Symmetry catalog

One card per discovered symmetry. Each links to its detail page with the full invariant, derivation, and Lean theorem list.

§ 03  ·  WIDGETS

Interactive invariants

Three working demos — slider-driven, no frameworks. Each illustrates one symmetry class from the catalog. Move a control, the invariant holds live.

RoPE rotational equivalence

Rotation $R_\theta$ applied to both $Q$ and $K$ leaves attention logits unchanged. The affected frequency bands depend on $\theta$.

—

Channel dormancy

Zeroing rows of $W$ collapses the downstream image. The invariant block — the submatrix untouched by training — is highlighted.

—

Sign-phase gauge

Conjugating a hidden layer by $D = \mathrm{diag}(\pm 1)$ yields a gauge-equivalent network. Output is identical up to floating-point noise.

—
§ 04  ·  LEAN

Proof status

Per-symmetry counts, auto-populated from _data/lean_status.json.

Symmetry Proven Deferred Axiomatic Stub Total Distribution
§ 05  ·  ARTIFACTS

Paper & code

Manuscript, source, and formal proofs. Cite as below.

pending PDF Manuscript build pending latexmk on manuscript/main.tex
pending arXiv Preprint submission pending after manuscript finalisation
Repository github.com / d3banjan / symmetry-survey-paper Lean 4 · Mathlib · MIT Citation BibTeX entry below · one-click copy 
@article{basu2026symmetry,
  title   = {Symmetry Survey for Verified Neural Compilation},
  author  = {Basu, Debanjan},
  year    = {2026},
  note    = {Lean 4 companion at github.com/d3banjan/symmetry-survey-paper}
}