Latest Work

We introduce the Structured Latent Basis (SLB) framework, a perspective on supervised learning that unifies feature engineering and modeling as a single problem: selecting a mathematical basis in which the target function is linear.

We introduce the Smooth-Step Spectral Method (S³M), a structured basis regression approach that unifies smooth spectral features with learned threshold features for tabular data.

Baluyot, Goldston, Suriajaya, and Turnage-Butterbaugh [BGST23] proved the first unconditional asymptotic for Montgomery's pair-correlation function $F(\alpha, T)$, with error $O(1/\sqrt{\log T})$ uniformly for $\alpha \in [0,1]$.

We pre-register and test a spectral-error-mitigation prediction for the two-qubit gate fidelity of Quantum Inspire's Tuna-9 9-qubit transmon processor and execute it in four cryptographically timestamped stages.

We prove that the triangle-plus-center central configuration of the planar four-body problem with masses $(1, 1, 1, \mu)$ undergoes an exact stability transition at the critical mass ratio $$\mu^* = \frac{81 + 64\sqrt{3}}{249},$$ the unique positiv

We present formal proofs of six foundational theorems in integer arithmetic: commutativity of addition and multiplication over ℤ, absorption of zero under multiplication, non-negativity of squared differences, and the dichotomy that every natural number is either zero or positive. All results are machine-verified in the Lean 4 proof assistant.

We introduce the **PDE Tensor Algebra**, a framework that represents any PDE system as a triple $(D, C, P)$ of tensors encoding dissipation, nonlinear coupling, and geometric constraints. The decomposition converts qualitative PDE questions — existence, uniqueness, regularity, stability — into computable algebraic conditions on the tensors.

The Z₃ Ansatz $\sqrt{m_r} = a(1 + b\cos(\theta_0 + 2\pi r/3))$ with $b^2 = 2$ is a parametrization — not a dynamical model — that encodes the Koide mass relation $Q = 2/3$.

We present a machine-verified derivation chain connecting the E₈ Lie algebra to the electromagnetic fine structure constant $\alpha \approx 1/137$.

The Birch and Swinnerton-Dyer conjecture predicts that for an elliptic curve $E/\mathbb{Q}$ the Mordell-Weil rank equals the order of vanishing of the Hasse-Weil $L$-function at $s = 1$, and that the leading Taylor coefficient is expressed by an expl

Gene Regulatory Network Dynamics — Stability, Inference & Latent Connection. This paper presents 50 machine-verified theorems building on 3 established facts and 54 hypotheses.

This paper presents 0 machine-verified theorems. All results are formally verified in the Lean 4 (629 verification units, 102 proved statements) and exportable to Lean 4. <!-- TODO: Write a proper abstract summarizing the key contributions -->

Neural Manifold — Spectral Dimension Bound, Optimal Decoding & BCI Theory. This paper presents 47 machine-verified theorems building on 5 established facts and 32 hypotheses.

Wright-Fisher Population Genetics — Spectral Convergence + Latent. This paper presents 24 machine-verified theorems building on 0 established facts and 35 hypotheses.

American Basket Gym — ProofEnv proofs (eigen-COS / FW / GH error bounds). This paper presents 67 machine-verified theorems.

This paper presents 0 machine-verified theorems. All results are formally verified in the Lean 4 (97 verification units, 20 proved statements) and exportable to Lean 4. <!-- TODO: Write a proper abstract summarizing the key contributions -->

Bayes decision — ProofEnv encoding of BayesClassifier / MAPClassifier (Lean BayesDecision). This paper presents 58 machine-verified theorems.

Bayesian Risk — clean ProofEnv proof. This paper presents 51 machine-verified theorems.

Bellman — ProofEnv: DP value bounds, MDP Bellman operator, contraction lemmas. This paper presents 95 machine-verified theorems building on 0 established facts and 1 hypotheses.