GST Core V2: Mathematical Foundations and Lean 4 Formalization

Abstract

This work presents the coherent mathematical core of Guided Symbiosis Theory (GST) and a Lean 4 formalization of its principal results. It develops the research programme introduced in the original conceptual work, The Theory of Guided Symbiosis (DOI: 10.5281/zenodo.17195102), and subsequently advanced in the mathematical core dated 10 September 2026 (DOI: 10.5281/zenodo.22704652). The present version removes background resource self-replenishment and investigates the consequences for optimal control, long-term preservation of useful capability, and the value of external replenishment. The model is a deterministic infinite-horizon optimal control problem with two state variables: a stock of currently useful capabilities and a cooperation resource. Bounded effort produces useful capability while consuming the resource, which is replenished by a constant external source. The objective accounts for discounted costs of deviation from a target capability level and expenditure of effort. The principal results are: • Existence of an optimal control under the general assumptions of the model. • Necessary optimality conditions with canonical costates defined by integrals along the future trajectory. • A sufficient condition for global optimality and almost-everywhere uniqueness, together with a quantitative objective gap bound. • An explicit parameter region ensuring the corresponding optimality and uniqueness conditions, and a separate result for fixed coefficients with an arbitrary nonnegative external source. • Convergence of the useful capability stock to zero under every admissible control when replenishment is absent. • A necessary and sufficient criterion for preserving prescribed positive lower bounds on both states from every point in the corresponding region. • Strict improvement of the optimal objective value under any positive external source relative to a zero source, with all other parameters and initial conditions held fixed. The publication includes the English mathematical paper, the Lean 4 formalization archive, its SHA256 checksum, and materials from a fresh verification build. The paper provides an explicit correspondence between its mathematical results and the formal theorems. The formalization concerns the precisely specified model and its assumptions. It does not automatically establish the broader conceptual claims of the original GST or the optimality of a particular superintelligence (SI) system. Applying the model to human–SI interaction requires a separate justification of the relationship between its mathematical variables and observable processes. The editorial revision dated 11 October 2026 updates the abstract, references to earlier works, and licensing information. The mathematical statements and formalization archive remain unchanged. The author’s original materials are released under Apache License 2.0 within the scope specified in LICENSING_SCOPE.txt.