arXiv subjects

Raphael Coelho

Publications and source records attributed to Raphael Coelho.

6 recordsLinked to original sources

arXiv2026

Reading the Count: Prediction Markets and Brazil's 2026 Presidential Election

We rebuild the public count of Brazil's 2026 presidential runoff minute by minute from the electoral court's section-level records and compare it with every trade on Kalshi and Polymarket. A projection published live on the night gave the eventual winner, Lula, a probability of 0.998 from 19:15, with 1.6% of sections counted. The markets reached 0.9 at 20:24, with 46% counted. Read as the projection's central estimate with a wider uncertainty, their prices imply a standard deviation of the final margin about four times the live projection's, and about twice that of a section-level projection calibrated on the 2018 runoff, the earlier night with the largest errors. Valued at these projections, takers' purchases of Lula after the count resumed had an expected profit of 4 to 18 cents per Kalshi contract after fees; valued at a state-level extrapolation of the count, it was zero. During a two-hour suspension of the count the markets gave Lula 0.25 to 0.44, below every reading we compute afterwards from the sections then public, none of which was available live. On the first-round night, when the headline count showed the eventual leader ahead from its first file, the same markets were faster than our projection.

q-fin.TR↗

arXiv2026

Comparing tail forecasts: the number of exceedances is the sample size

When two forecasts of a tail, such as prediction intervals at high coverage, extreme quantiles or expected shortfall (ES), are compared by a consistent score, the score difference is known in advance except on the days on which the outcome falls beyond a forecast. The number of these exceedances, not the number of observations, is the effective sample size. For intervals at miscoverage level $α$, the number of observations a comparison needs grows like $1/α$ while the number of exceedances it needs does not, and for some pairs of forecasts no test can do better. A confidence sequence that is valid at all times and needs no distributional assumption attains this rate; Hoeffding-type procedures, calibrated by the range of the score difference, need $1/α$ times more. When exceedances are scarce, the Diebold-Mariano test declares the less conservative forecaster better with at least, asymptotically, the probability of observing no exceedance, whichever forecaster is actually better; the usual small-sample corrections do not remove this, while a bootstrap-t version largely does. For (value-at-risk, ES) forecasts, a less conservative ES can be shown without assumptions to be worse on the days on which it is less conservative, but never to be better without an assumption on the loss tail. In 250-day windows of 97.5% forecasts for seven stock indices, 18.4% of significant Diebold-Mariano results favouring the less conservative model contradict the ranking on the remaining days, against 6.9% of those favouring the more conservative one.

q-fin.MF↗

arXiv2026

A Formally Verified Library of Mathematical Finance in Lean 4

We describe a library of mathematical finance built in the Lean~4 proof assistant, on top of Mathlib and the BrownianMotion package. It is broad: more than three hundred sorry-free theorems across eleven areas, from the measure-theoretic foundations of continuous-time stochastic calculus through derivative pricing to applied risk, portfolio, and fixed-income theory. To our knowledge it is the most comprehensive machine-checked development of mathematical finance to date. Two things make it more than a catalogue. It reaches into the continuous theory far enough to construct the $L^2$ Itô integral as a bounded linear isometry and to derive, rather than assume, the risk-neutral pricing measure. And it audits its own faithfulness: every result is classified by how its Lean statement relates to the mathematics it claims, and a build-enforced gate pins the axioms each proof actually uses, so a reader can see precisely what has been proved and what has only been proved under added hypotheses. We close with a finding: a formal base over classical financial mathematics yields certified unification of known results rather than new financial theory. The contribution is therefore methodological and infrastructural (reusable verified foundations for mathematical finance, together with the faithfulness audit above), not a new financial result.

q-fin.MF↗

arXiv2026

A Machine-Checked Itô Calculus for Brownian Motion

We develop the Itô calculus of Brownian motion, machine-checked in Lean~4 over Mathlib and the \lean{BrownianMotion} package. On a bounded interval $[0,T]$ the Itô integral is built as a Hilbert-space isometry, from a predictable-rectangle $π$-system through the density of simple adapted processes. Realized as a process, it is a continuous $L^2$ martingale. One structural identity drives this: the integral at time $t$ is the conditional-expectation projection of its terminal value onto $\F_t$, and from it adaptedness, the martingale property, the contraction bound, and both the terminal and time-indexed Itô isometries follow as corollaries. On this integral we prove Itô's formula for $C^3$ functions with bounded derivatives, including the time-dependent form $df = f_x\,dB + (f_t + \tfrac12 f_{xx})\,dt$, by a discrete-to-continuous argument through weighted quadratic variation with explicit $L^2$ remainder bounds. We then pass from the $L^2$ theory to the pathwise. The integral process has an almost-surely continuous modification, and its everywhere-continuous representative is a local martingale for the null-augmented Brownian filtration; gluing the bounded-horizon representatives along the half-line yields the Itô integral as a continuous local martingale on all of $\R_{\ge 0}$, the form it takes in the classical theory. To our knowledge these are the first machine-checked constructions of the Itô integral and of Itô's formula in any proof assistant, and the first to reach a pathwise-continuous local martingale. The boundary is explicit. The $L^2$ integral and Itô's formula are developed on $[0,T]$ with bounded-derivative integrands; the unrestricted $C^2$ formula, integrators beyond brownian motion, and right-continuity of the filtration lie outside the development.

q-fin.MF↗

arXiv2026

The Fundamental Theorem of Asset Pricing, Formalized in Lean 4

The Fundamental Theorem of Asset Pricing states that a market is free of arbitrage exactly when it admits an equivalent martingale measure. We formalize it in Lean 4 over Mathlib in three settings: a finite-state market over a finite horizon (Harrison-Pliska), a one-period market on an arbitrary probability space with a single scalar return (Follmer-Schied), and a one-period market with finitely many assets. The finite case is the geometry of a separating hyperplane; the scalar one-period case is an elementary change of measure. In the $d$-asset case the equivalent martingale measure is constructed explicitly, as the minimiser of the smooth convex potential $\mathbb{E}[\log(1+e^{\langleθ,Y\rangle})]$: absence of arbitrage is precisely coercivity of the potential, its first-order condition is the martingale property, and the minimiser's logistic weight is the density of the measure. The construction uses no Hahn-Banach theorem, no $L^0$-closedness argument, no measurable selection, and no non-redundancy hypothesis. To our knowledge this is the first machine-checked Fundamental Theorem of Asset Pricing in any proof assistant. The boundary is explicit: the general multi-period Dalang-Morton-Willinger theorem lies outside the development. Every theorem is sorry-free, each headline result's axioms are pinned to Mathlib's classical defaults by a build-enforced gate, and the whole is reproducible from a pinned toolchain.

q-fin.MF↗

arXiv2026

Three-Currency HJM for Brazilian Credit Markets

This paper develops a three-currency Heath-Jarrow-Morton framework in which corporate credit is treated as a separate economy, connected to the nominal and real economies through synthetic inflation and credit exchange rates. The framework produces a testable identity. Under joint no-arbitrage, the credit spread of an issuer expressed over the inflation-rateindexed risk-free curve equals the same issuer's credit spread expressed over the nominalrate-indexed risk-free curve plus the model-implied breakeven inflation forward at the same maturity. The identity holds within any single calibration of the framework. It is empirically falsifiable across two parallel corporate-bond segments of the same market, in a segmented market the two segments may price different corporate credit economies, and the gap between their implied corporate forwards measures the failure of the shared-credit-economy assumption. Applied to Brazilian debenture markets, the framework delivers a sharp empirical finding. Fifteen large issuers placed paper in both the CDI-indexed general-purpose segment and the IPCA-indexed infrastructure segment between January 2021 and February 2026. The within-issuer triangle residual at the 3-year tenor averages 640 basis points, with crosssectional standard deviation of 26 basis points across the 15 issuer means, and remains stable through both the 2021-2023 BCB tightening cycle and the 2024-2026 easing phase. A retail post-tax indifference benchmark anchored on Lei 12.431 closes the bulk of the residual. The remainder is consistent with institutional participation on the CDI side, contractual asymmetries between debentures with different use-of-proceeds restrictions, and segment-specific liquidity gaps.

q-fin.MF↗