Three Rings III: Certified Koopman–Beltrami Operator with Applications to Non-Combinatorial Scheduling Andrew Strelzoff¹, Benjamin Strelzoff², and Tulio Sulbaran³

The iterative Koopman–Beltrami (K–B) operator extracts slow-mode dynamics from a time-series observation of a dissipative system, one shell at a time, via AMG resolvent inversion. Paper 2a (Three Rings II) showed that the number of shells can be predicted a priori from a single DMD fit using a Jensen–Szegő spectral diagnostic. This paper proves that the extraction converges: under three necessary conditions (Leray dissipation, Weyl spectral-gap persistence, finite Jensen count), each pass contracts the current shell's slow-mode energy by a computable factor η < 1, and the iteration terminates after exactly p passes with bounded residual energy. The proof is formalized in Lean 4 as an independent chain (KostpmOperator) using three classical oracles (Leray 1934, Weyl 1912, Davis–Kahan 1970). No sector decomposition is required — the operator works on shells alone, with sectors reserved for the surrogate-model extensions of Paper 2c (Three Rings IV) and the NS-specific analysis of Paper 3. We demonstrate the operator on five systems of increasing complexity. Two are single-pass: a 179-bus power grid where the operator reproduces the topo-RAS vulnerability ranking, and a multiphysics aircraft where the operator recovers the gateway C/F sensor classification. One is a two-pass system: a cylinder wake at Re = 200 where the operator separates the Kármán shedding mode from the entrainment dynamics. Two are scheduling systems analyzed non-combinatorially: highway construction earned-value management (1 shell — the resolvent energy ranks work packages by schedule impact), and geo-distributed data center workload scheduling (5 shells — the richest structure in the test set, with per-datacenter scheduling-impact ranking and 24-hour carbon-aware forecasting). The construction and data center examples demonstrate the operator's utility beyond physics: the same mechanism that identifies vulnerable grid buses and separates turbulent scales also ranks work packages by EVM impact and data centers by carbon-scheduling significance — all without solving a combinatorial optimization problem. v2 (2026-05-09): code supplement added. Two artifacts now accompany the paper. The first, kostpm-lean-v0.1.0.zip, is the Lean 4 formalization comprising KostpmOperator/ (the certified K–B operator with resolvent-energy bound and convergence proof) and KostpmCerts/ (Lie-algebra structure-constant certificates for SO(3), SL(2,ℝ), SL(3,ℝ), Heisenberg, U(1), and the Standard Model gauge algebra), totaling 26 source files; lake exe cache get note that the empirical results of Three Rings IV (Sobol × KOSTPM sensitivity, Szegő saturation testing, the SustainCluster and EVM validations) are reproduced from this same package — see https://doi.org/10.5281/zenodo.19571618 for the IV companion paper.