Research
ML research on neural network compression, formal verification with Lean 4, and empirical methodology that can falsify its own claims. All experiments run on RTX 3060 12GB — hardware constraints are the motivation, not the limitation. Current focus: MoE weight quantization with machine-checked invariants. Research supplements and informs engineering work on LLM agent infrastructure.
Papers
Phase-Collapse Defragmentation: Provable Bounds on 1-bit KV-Cache Quantization in MoE
Moment-ratio gauge construction that determines — from weight statistics alone, before inference — whether 1-bit KV-cache quantization is achievable for a given layer. MoEGauge and JensenFloor theorems proved in Lean 4 with zero sorries. Evaluated on OLMoE-1B-7B.
Verified Neural Compilation: Formal Symmetries and Impossibility Boundaries
Machine-checked proofs of RoPE commutant classification and block-diagonal frequency boundaries in Lean 4. Formalizing zero-cost compilation invariants and proving the impossibility of key-only routing under standard MoE interfaces.
RoPE-Provenance: Subspace-Split Positional Encodings for Token-Role Auditing
Allocating a low-frequency subspace of RoPE positional encodings to serve as an out-of-band role channel. Applied to SmolLM2-135M to dynamically isolate instruction execution from untrusted data payloads. Pre-registered benchmarks evaluate selectivity (SEP scores) and instruct compliance under adversarial injection.
Other Research
Falsifying LoRA Alignment Geometry: srank as Overfitting Signature in DPO Fine-Tuning
Pre-registered study of whether DPO fine-tuning leaves a geometrically distinct fingerprint in LoRA weight updates. Two claims killed: the orthogonal-complement hypothesis (directional violation) and cross-probe srank (length-bias artifact). Interactive microsite with d3 exploration widgets.
A Survey of Symmetries Compression Must Respect
Living catalogue of algebraic invariants — RoPE, SignPhase, BoundedArithmetic, DenseSparse, dormancy — that any compression scheme must preserve to avoid silent correctness failures. Lean 4 coverage across 152/161 symmetry claims.
Methodology
The empirical methodology used across these projects — pre-registration, kill ladders, τ-baselines, theorem-screened experiments — is documented as a standalone series. It borrows from clinical trial design and applies it to solo ML research. Start with Notes on a Methodology Transition or the Compression Falsification Ladder.
Blog series
The Geometry of MoE Compression (Part E)
Expanding on Phase-Collapse: β transfer in FFNs, formal Softmax soundness, and recovering dense performance from quantized layers.
- The β-lift and FFN Transfer: MoE Compression Part E
- Formalizing the Softmax and Hessian: Lean 4 Soundness Proofs
- Dense Activation-Fit Recovery: Healing Quantized Layers
Notes on a Methodology Transition
Moving from selectionist ML research (run many probes, kill the bad ones) to physicist-mode research (theorem first, two parameters per probe, universality over coverage). A live chronicle.
- What Experimental Design Actually Means
- Hypothesis Testing from Scratch, and Its Bayesian Analogue
- Two Research Modes, and Why the Second One Needs Lean 4
- Naming What Fails: The Obstacle Taxonomy
- Theorem-Screened Experiments
- The Five-Minute Daily Drift Check