Stochastic Portfolio Theory, Machine-Checked: What Is Proven, What Is Sealed Against Mathlib, and What Stays a Modeling Assumption

Stochastic Portfolio Theory provides a model-free framework in which functionally generated portfolios track the market index up to two terms: a boundary term in the generating function and the time-integral of an excess growth rate. We formalize the logical skeleton of this framework in a proof kernel and report, with deliberate precision, which parts are derived and which are assumed. Three tiers result. (i) The elementary algebra of diversification — that a component-weighted average variance dominates the corresponding diagonal basket variance — is derived from first principles as a sum-of-squares certificate, generalized term-by-term beyond the two-asset case; with full correlation, the excess growth of an arbitrary portfolio is a non-negatively weighted sum of pairwise return-difference variances, \gamma^{}_\pi = \tfrac12\sum_{i