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_efficiency_cubic_in_drive_over_tension — efficiency scales as the cube of the drive; (ii) site_prep_halving_sigma_eightfolds_efficiency — halving the site-preparation tension σ multiplies efficiency by exactly 8 = 2³, the headline stewardship lever; (iii) homogeneous_limit_recovers_fnt — the barrier equals ½ Δμ nStar, recovering the Forest Nucleation Theorem in the homogeneous limit; (iv) sower_IB_ceiling — the Sower’s seeding-information rate obeys the Intelligence-Bound ceiling rate ≤ P D / (k_B T ln 2), finite and binding because the denominator is strictly positive (the twenty-fifth Intelligence-Bound self-application); and (v) seeding_efficiency_eq_cos2_theta — 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_eco) 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.