Machine-Verified Proofs

We define the **Latent** of a smooth system as the basis-free element of a graded Hilbert tensor algebra that completely characterizes the system's distributional, dynamic, and functional properties.

Derivative pricing has a clear mathematical target: compute the discounted risk-neutral value of a payoff under a specified model. For European vanilla contracts this target is often analytic or nearly analytic.

We present an algebraic framework relating the growth of the zeta moments to Hankel-determinant structure, together with an honest account of where the framework does and does not reach the Riemann Hypothesis.

The equity premium puzzle of Mehra and Prescott (1985) is the observation that the standard consumption-based asset pricing model, calibrated to plausible risk aversion and the observed smoothness of aggregate consumption, predicts an equity premium

**Theorem A (Main result, conditional).** Conditional on the 20 named Tier A–D hypotheses of §7.1 — in particular the three Tier-D perturbative-QFT inputs (`tomboulis_formula`, `b_zero_from_feynman`, `beta_1_rge_def`) — we establish that Yang-Mills t

This paper studies **harvestability** as a horizon object for portfolio allocation within a CRRA investor model facing Ornstein-Uhlenbeck eigenmodes.

We turn the gradient-descent account of in-context learning (ICL) into machine-checked mathematics and falsifiable predictions about real transformers. The formal target is the linear-attention regression identity: a forward pass can implement one gradient-descent step on an implicit least-squares objective.

Expected Shortfall backtesting under Basel III/IV suffers from an unmeasured structural weakness: Monte Carlo estimation of ES injects computational noise into the Acerbi-Székely (2014) test statistic, but the magnitude of this contamination has not

The Latent Theorem guarantees that any smooth system has a finite representation whose size depends on regularity and accuracy, not on ambient dimensionality. We extend this result to **families** of smooth systems.

We present the Eigen-COS method, a deterministic algorithm that computes exact Value-at-Risk, closed-form Expected Shortfall, and the full CDF/PDF for weighted sums of correlated lognormal assets — without Monte Carlo simulation.

The CDF of a weighted sum of correlated lognormal random variables has lacked a tractable characterization since Fenton (1960). We show that eigenvalue conditioning of the correlation matrix, followed by Fourier-cosine inversion, yields an analytic, grid-free $N$-term spectral representation of that CDF: the **Spectral Lognormal Distribution**.

A speculative grade-ratio model for fundamental constants, with formalized arithmetic components and explicit physical assumptions.

Every formula in quantitative finance — CAPM, Markowitz, VaR, Sharpe ratio, GARCH — takes returns as input. Yet the standard definitions of return fail when prices cross zero: log-returns are undefined, and simple returns produce sign errors.

We present a deterministic, semi-analytical framework for computing the complete distribution of a portfolio's terminal value at horizon $T$ for correlated lognormal assets. Unlike traditional approaches, this method requires no Monte Carlo simulation.

The companion core paper establishes, and machine-checks, a single identity: a transformer's forward pass can implement one gradient-descent step on an implicit least-squares objective (the ICL=GD mechanism). This satellite asks what that verified identity forces to be true about *representational capacity and scaling*.

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]$.