Fin Arcsinh Bs

We derive a closed-form European option pricing formula valid for all spot prices \( S_0 \in \mathbb{R} \), including negative values. The formula replaces the logarithmic transform of Black-Scholes with the inverse hyperbolic sine, yielding a three-term call price \( C = S_+ \Phi(d_+) - S_- \Phi(d_-) - K e^{-rT} \Phi(d) \). The additional term \( S_- \Phi(d_-) \), absent in Black-Scholes, captures the contribution of negative-terminal-value states and vanishes exponentially for large positive \( S_0 \). We prove: (i) the formula satisfies the martingale condition exactly; (ii) the third-term correction is bounded by \( S_- \) and vanishes in the large-positive-price regime, where the pricing formula becomes asymptotically Black-Scholes; (iii) it admits a local Bachelier limit when the transform linearizes near zero; (iv) Delta is closed-form and Gamma is bounded everywhere; (v) put-call parity holds through zero; (vi) all no-arbitrage conditions are satisfied. The algebraic framework — martingale conditions, coefficient identities, derivative bounds, and structural reductions — is formally verified in Lean 4 with zero sorry obligations. The Gaussian integration step follows the standard Black-Scholes derivation pattern. The pricing formula is exact for the transformed terminal-distribution model used in the paper; the associated local-volatility SDE provides a continuous-time interpretation linking the Black-Scholes and Bachelier regimes.