Files
proofs/CLAUDE.md
zeekay c59b82e136 lean/Crypto: Magnetar.lean (was Comet.lean) + HQC + lakefile — rip AI slop in docstrings
Magnetar.lean: top docstring 36→14 lines, inline /-- ... -/ docstrings tightened.
All 9 axioms + 2 theorems preserved verbatim. CHRONOLOGY moved to legacy-md/.
2026-05-18 21:21:12 -07:00

Symbolic link
6 B