The Afforestation Stewardship Theorem: Cubic Optimal Seeding and an Intelligence-Bound Ceiling for Nucleation-Limited Reforestation

Standalone thematic-series record of the Viridis Canon (Afforestation). The core Intelligence-Bound canon spine is unchanged (frozen at v10. 0. 0, record 20801185) ; this record links to the spine via isDerivedFrom the concept DOI 10. 5281/zenodo. 19317982. We formalize the analytic core of the Afforestation Stewardship Theorem (AST), “the Sower”: a model of reforestation in which establishment is limited by nucleation, not seed count. A candidate site is a nucleation gamble — an ecological drive Δμ (suitability) works against an edge hostility or surface tension σ (competition, exposure, herbivory), with a shape constant a. Classical nucleation theory then gives the critical nucleus nStar = (2 a σ / 3 Δμ) ³, the barrier 4 (aσ) ³ / 27Δμ², and the seeding efficiency eff = C (3Δμ / 2aσ) ³ = C / nStar (established canopy per seed). The stewardship problem — where a finite seed budget goes and what site preparation pays off — is a non-convex allocation over a field of such sites, plus a cubic optimal-seeding law. AST is the first non-convex member of the shadow-price water-filling family, of which the prior convex results are the homogeneous limit. Five results are machine-checked in Lean 4 (Aristotle, zero sorry, axioms ⊆ propext, Classical. choice, Quot. sound), namespace Viridis. Afforestation. AfforestationStewardship: (i) establishmentₑfficiencycubicᵢndriveₒverₜension — efficiency scales as the cube of the drive; (ii) siteₚrepₕalvingₛigmaₑightfoldsₑfficiency — halving the site-preparation tension σ multiplies efficiency by exactly 8 = 2³, the headline stewardship lever; (iii) homogeneousₗimitᵣecoversfnt — the barrier equals ½ Δμ nStar, recovering the Forest Nucleation Theorem in the homogeneous limit; (iv) sowerIBceiling — the Sower’s seeding-information rate obeys the Intelligence-Bound ceiling rate ≤ P D / (kB T ln 2), finite and binding because the denominator is strictly positive (the twenty-fifth Intelligence-Bound self-application) ; and (v) seedingₑfficiencyₑqcos2ₜheta — the seed–site alignment efficiency ⟨n, m⟩² / (∥n∥² ∥m∥²) = cos²Θ lies in 0, 1 by Cauchy–Schwarz, with forcing debt 1 − cos²Θ = sin²Θ. All conclusions are non-vacuous (t³, factor-8, the ½-identity, a finite ceiling, and a cos² bound strictly inside 0, 1 in general). This record pairs with the Forest Nucleation Theorem (record 20982979), its convex sibling — the two afforestation records that would seed a dedicated Afforestation series at the three-record trigger. The combinatorial-optimization layer (bang-bang knapsack, greedy ½-approximation) and the (β, Tₑco) phase diagram are deferred and are not part of this record. Scope. The Lean proofs certify the validity of the reasoning, not empirical magnitudes. Working paper; not peer-reviewed.