Theorems as Instrument Design: Formal Guarantees and Statistical Contracts in a Generative Musical Instrument

Generative instruments fail differently from other software: their worst defects are not crashes but slow statistical lies — a melodic register drifting off the usable range over minutes, variety collapsing into repetition, multi-scale structure whitening into noise while every individual note remains legal. None of this is visible in a demonstration or caught by example-based testing. We argue that the playability claims of a generative instrument should therefore be treated as design theorems: stated precisely as properties of the underlying stochastic process, proved formally where the mathematics is tractable, and mechanized as continuous-integration gates in every case — with statistical properties published as measurement protocols whose acceptance bands are derived once and then frozen. We develop the argument through the Fenophone, a browser-based instrument built on a Markov-switching multifractal cascade, whose engine enforces this discipline end to end: a register-gravity stability theorem with a closed-form stationary deviation and a mandatory "two-minute drift" gate; layer-invariance obtained by construction through per-layer seed substreams; monotone perceived controls verified by behavioral sweeps; and a detrended-fluctuation-analysis contract applied to every shipped and future community sound pack. We discuss what generalizes to other stochastic-process instruments, what does not (taste), and what the discipline costs. Part of the Feno program. The source repository is private; the reproduction materials for this record are contained in the record itself.