The Forest Nucleation Theorem: A 'Concentrate, Don't Broadcast' Design Law for Drone Afforestation

Staged thematic record of the Viridis Canon (route: standalone NEW-CATEGORY). The Intelligence-Bound spine is unchanged (frozen at v10.0.0, record 20801185); this record links to it via isDerivedFrom the concept DOI 10.5281/zenodo.19317982. The afforestation design law, from classical nucleation theory reparametrized by the cube-root order parameter r:=n^{1/3}. The critical nucleus r*=2aσ/(3Δµ) is the unique global maximizer of the polynomial free energy G(r)=−Δµ·r³+aσ·r², with the half-barrier identity ΔG*=½Δµ·n*. The Dispersal–Establishment Paradox: colonized area is uniquely maximized at the critical deposition number n* and broadcasting colonizes zero — concentrate, don't broadcast. Candidate seed for an Afforestation series. The 4 core theorems are machine-checked in Lean 4 (Aristotle, zero sorry, axioms ⊆ {propext, Classical.choice, Quot.sound}, statements verbatim and non-vacuous). Scope: the Lean proofs certify the validity of the discrete reasoning, not empirical magnitudes. Working record; paper pending; not peer-reviewed.