Machine-Verified Proofs

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.

An elementary representation route for sums of correlated lognormals; published with DOI and stated for review.

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**.

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

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

We introduce a grade decomposition of the Gevrey energy balance for the incompressible Navier-Stokes equations. The physically correct model uses $\mathbb{C}$-valued Fourier coefficients with a factor of $i$ in the advection; the real-coefficient model trivializes all grade-3 terms.

We present a reusable algebra for machine-checked certificates in declared engineering models, where supplied equations, inequalities, monotonicity directions, and perturbation bounds imply an encoded safety, lifetime, stability, or performance predicate.

Saddle-point approximations replace an action by its quadratic part, but transferring a quantitative error statement between applications requires an explicit remainder estimate.

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 establish conditional bounds in a stylized antitone threshold model of recursive AI self-improvement. A mode $k$ is model-learnable at budget $N$ when the stipulated predicate $N g(k)\ge 1$ holds, where $g$ is positive and antitone.

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*.

We present a machine-checked source containing 78 named real-arithmetic declarations that occur as local steps in standard analyses of stochastic gradient descent (SGD). This declaration count includes support identities, recovery variants, and direct restatements; it is not a count of novel or publication-credit theorems.

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).

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 give a short conditional reduction of the Riemann Hypothesis to three classical inputs — Kronecker-Weyl equidistribution, the Bessel I₀ product identity, and Mertens' divergence theorem — plus a cited pair-correlation step.

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).

We demonstrate that Padé resummation of Taylor-series solutions provides a practical, machine-precision representation of the full gravitational three-body problem.

We present a bounded verification case study for COS caplet pricing. The numerical component expands the payoff of a log-forward rate, pairs characteristic-function coefficient proxies with raw payoff integrals, and reproduces Black benchmark values in a lognormal special case.