The Mutualist Co-Establishment Theorem: Obligate Two-Body Co-Establishment as Joint Mass-Action Nucleation

Paper supported by machine-verified Lean 4. The Mutualist Co-Establishment Theorem (MCET) recasts afforestation as an obligate two-body co-establishment (joint nucleation) problem: a plant and its microbial symbiont must co-arrive at sufficient joint density or neither persists. Its results: (i) co-establishment is feasible if and only if the partners' joint density clears a threshold n_p·n_s≥Θ (the thermodynamic content of obligacy), with a unit-slope log-density separatrix; (ii) the minimum-cost co-inoculation is C*=2√(c_p·c_s·Θ) with an equal-spend optimum; (iii) symbiosis recedes the reachability wall by an absolute-advantage specialization saving that scales with partner dissimilarity (maximal for cross-kingdom plant/fungus pairs, zero for conspecific monoculture) — degraded sites forbidden to monoculture become establishable with a co-introduced partner; (iv) an Intelligence-Bound floor on strain-matching time with a decaying matching regret; (v) a common-mycorrhizal-network portfolio effect; and (vi) co-establishment efficiency equal to cos²Θ. This version (1.0.0) deposits the clean analytic core (15 machine-verified theorems). Derived from the Viridis Intelligence-Bound canon, concept DOI 10.5281/zenodo.19317982.