| license: agpl-3.0 | |
| language: | |
| - en | |
| tags: | |
| - formal-mathematics | |
| - theorem-proving | |
| - lean4 | |
| - quantum-computing | |
| - attention-mechanism | |
| - nand-decomposition | |
| - snapkitty | |
| - research | |
| - latex | |
| pretty_name: SnapKitty Formal Papers | |
| # papers | |
| Formal mathematics papers from the SnapKitty / SNAPKITTYWEST research stack. | |
| ## Contents | |
| - π `quantum/cpsc_qft_conservation_preserving_compilation.pdf` β Conservation-Preserving Compilation for a 1+1D Lattice Shadow of Οβ΄ (Ahmad Ali Parr, October 2026). Paper text licensed GPL-3.0-or-later (code: CPSC-ESCL-1.0 or AGPL-3.0-only). Release page: [Snapkitty/cpsc-qft-paper](https://huggingface.co/datasets/Snapkitty/cpsc-qft-paper) Β· DOI [10.5281/zenodo.23287576](https://doi.org/10.5281/zenodo.23287576) | |
| - `formal-math/attention_nand_decomposition_full.pdf` β Full NAND decomposition of the attention mechanism | |
| - `formal-math/gkn_boole_e7_quartic.pdf` β GKN Boole E7 quartic (PDF + LaTeX source) | |
| - `formal-math/theorem_t1.pdf` through `theorem_t4.pdf` β Core theorem sequence | |
| ## Links | |
| - [SNAPKITTYWEST GitHub](https://github.com/SNAPKITTYWEST) | |
| - [sov-kernel-monster](https://huggingface.co/Snapkitty/sov-kernel-monster) | |
| --- | |
| ## License | |
| Licensed under **AGPL-3.0**. Full text: [LICENSE](LICENSE). | |
| ### πΌ Commercial License | |
| Snapkitty code is free and open under **AGPL-3.0** for open-source use. Building a commercial product or service? A **proprietary commercial license** from Snapkitty Collective LLC lets you ship this code without the AGPL's source-sharing and network-use obligations. | |
| **[β Get a commercial license](mailto:A.parr@belespritdaccord.uk?subject=Commercial%20license:%20snapkitty-papers)** Β· A.parr@belespritdaccord.uk | |