Spaces:
Running
Running
Add Zenodo DOI 10.5281/zenodo.23287576
Browse files
README.md
CHANGED
|
@@ -24,7 +24,7 @@ Alternative attention · SUBLEQ · integer computing · formal proofs · the har
|
|
| 24 |
|
| 25 |
**[Conservation-Preserving Compilation for a 1+1D Lattice Shadow of φ⁴](https://huggingface.co/datasets/Snapkitty/cpsc-qft-paper)**
|
| 26 |
Symmetries of the Hamiltonian constrain circuit synthesis instead of filtering shots. Every admitted Trotter schedule is proved in Lean 4 to commute with its conserved operator, for every lattice size and angle. The axiom audit lists only `propext`, `Classical.choice` and `Quot.sound`.
|
| 27 |
-
[PDF](https://huggingface.co/datasets/Snapkitty/cpsc-qft-paper/blob/main/paper.pdf) · [Lean proofs](https://huggingface.co/datasets/Snapkitty/cpsc-qft-paper/tree/main/proofs/lean) · [Code](https://huggingface.co/Snapkitty/cpsc-qft)
|
| 28 |
|
| 29 |
## 🔬 Research highlights
|
| 30 |
|
|
|
|
| 24 |
|
| 25 |
**[Conservation-Preserving Compilation for a 1+1D Lattice Shadow of φ⁴](https://huggingface.co/datasets/Snapkitty/cpsc-qft-paper)**
|
| 26 |
Symmetries of the Hamiltonian constrain circuit synthesis instead of filtering shots. Every admitted Trotter schedule is proved in Lean 4 to commute with its conserved operator, for every lattice size and angle. The axiom audit lists only `propext`, `Classical.choice` and `Quot.sound`.
|
| 27 |
+
[DOI 10.5281/zenodo.23287576](https://doi.org/10.5281/zenodo.23287576) · [PDF](https://huggingface.co/datasets/Snapkitty/cpsc-qft-paper/blob/main/paper.pdf) · [Lean proofs](https://huggingface.co/datasets/Snapkitty/cpsc-qft-paper/tree/main/proofs/lean) · [Code](https://huggingface.co/Snapkitty/cpsc-qft)
|
| 28 |
|
| 29 |
## 🔬 Research highlights
|
| 30 |
|
hub.html
CHANGED
|
@@ -133,7 +133,7 @@ footer .wrap { display:flex; flex-wrap:wrap; justify-content:space-between; gap:
|
|
| 133 |
<p class="sub">New paper, with its Lean proofs and a reproducible axiom audit.</p>
|
| 134 |
<div class="feature">
|
| 135 |
<div>
|
| 136 |
-
<span class="badge new">New paper</span> <span class="badge">October 2026</span>
|
| 137 |
<h3>Conservation-Preserving Compilation for a 1+1D Lattice Shadow of φ⁴</h3>
|
| 138 |
<p>Symmetries of the target Hamiltonian constrain circuit synthesis instead of filtering measured shots. Every admitted Trotter schedule is proved, in Lean 4, to commute with its mode's conserved operator, for every lattice size and every angle. Each emitted schedule carries a SHA-256 certificate.</p>
|
| 139 |
<div class="ctas" style="margin-top:0">
|
|
|
|
| 133 |
<p class="sub">New paper, with its Lean proofs and a reproducible axiom audit.</p>
|
| 134 |
<div class="feature">
|
| 135 |
<div>
|
| 136 |
+
<span class="badge new">New paper</span> <span class="badge">October 2026</span> <a class="badge" style="text-decoration:none" href="https://doi.org/10.5281/zenodo.23287576">DOI 10.5281/zenodo.23287576</a>
|
| 137 |
<h3>Conservation-Preserving Compilation for a 1+1D Lattice Shadow of φ⁴</h3>
|
| 138 |
<p>Symmetries of the target Hamiltonian constrain circuit synthesis instead of filtering measured shots. Every admitted Trotter schedule is proved, in Lean 4, to commute with its mode's conserved operator, for every lattice size and every angle. Each emitted schedule carries a SHA-256 certificate.</p>
|
| 139 |
<div class="ctas" style="margin-top:0">
|