3 new papers in-repo — GDR-9, LiquidOps, Sovereign Entropy — feedback welcome
We just landed three new LaTeX papers in the sovereign-engine-v2 repo. Sharing here for early feedback before submission.
1. Sovereign Entropy (FM / CAV target)
Formally Verified 0.20-Nat Bound for Deterministic Agent Outputs
The entropy-constrained router in BURT-IMMA and sovereign-memory-twin enforces H(alpha) <= 0.20 nats. This paper is the machine-checked Lean 4 proof that the bound holds, backed by a SPARK Ada contract and wired into the ERE gate. 394 lines, clean.
Key theorem: routing entropy is bounded by a constant derived from the Goldilocks window — the same inequality appears in Weil bounds / RH for finite fields as a lemma.
2. LiquidOps (PLDI / ICFP target)
Refinement-Verified NAND-Canonical Kernel for Data-Plane ISA Compilation
NAND-canonical verified compiler. LiquidHaskell refinement types enforce correctness end-to-end through the P4 backend. 566 lines. The NAND decomposition is the same algebraic core used in the he-binary-functor module.
3. GDR-9 (SC / MLSys target)
Formally Verified Generalized Delta Rule Kernel Stack Across Nine ISA Targets
Nine ISAs: CUDA, NASM, RISC-V, ARM, WASM, APL, Haskell, Lean 4, P4. One generalized delta rule with drain invariants. Cross-ISA equivalence proved in Lean 4. 460 lines. Built on an RTX 3080 (sm_86). This is the kernel stack that underlies the BURT-IMMA CUDA layer.
Context: These sit on top of 8 papers already published to Zenodo (PIRTM, octonions, Coxeter/Weyl, PH-DAE, EmojiScript, Goldilocks, Resonance disclosure, DMZ F2 decomposition). 11 papers total across the stack.
Questions for the community:
- The entropy bound paper — does FM/CAV make sense or would LICS/CSF be a better fit?
- LiquidOps — anyone working at the LiquidHaskell/P4 intersection? Would love a second read.
- GDR-9 — SC vs MLSys: the cross-ISA Lean 4 equivalence proof is novel but the SC reviewers may not know Lean 4. Thoughts?
Code: https://github.com/SNAPKITTYWEST/sovereign-engine-v2
Dataset: https://huggingface.co/datasets/SNAPKITTYWEST/sovereign-training-corpus