An Audited Contract Boundary for COS Caplet Pricing

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. Ten Rust test functions pass. Three comparison tests cover five caplet cases, a ten-caplet semiannual cap, and four swaptions against Black/reference calculations; the remaining tests check narrower numerical properties. The accompanying formal artifact contains 55 theorem declarations and 13 explicit inputs. A declaration-level audit classifies 7 results as substantive conditional algebra, 30 as arithmetic or definitional checks, 16 as imported aliases, and 2 as tautologies. The artifact replays successfully with zero sorry or admitted proof holes in those declarations, conditional on the 13 explicit inputs. It does not formalize the finite COS series, a model-specific characteristic function, exponential coefficient decay, Jamshidian decomposition, analytical differentiation, or the Rust implementation. We therefore make one main claim: the combined artifact provides a reproducible numerical benchmark and a manually audited boundary around selected machine-checked scalar consequences. This is smaller than a verified pricing engine, but it is precise, testable, and suitable as a foundation for stronger future formalization. Maturity: Working Paper. Target venue: Journal of Computational Finance. Part of The Latent research program. Related papers in this program: Universal.