Re-certifying the Viridis OS Decision Kernels: A Lean Proof of the Restoration Critical-Nucleus Core

Working paper, not peer reviewed. Nothing in this record is field-validated. Scope and novelty. Project P2 re-proves the formal cores of Viridis OS decision kernels so that anyone can re-check them with the current public Lean 4 toolchain. These are classical, elementary results, not new theorems: the first, Carbon Continuity, is the 2x2 case of the Collatz-Wielandt characterisation of the Perron root of a nonnegative matrix (A. Berman and R. J. Plemmons, Nonnegative Matrices in the Mathematical Sciences, SIAM 1994, doi:10.1137/1.9781611971262). Each result holds only inside its stated model. It says nothing about coefficient values for any site, whether deployed kernel code implements the rule faithfully, or any carbon-credit or treatment outcome. Viridis OS runs decision kernels whose formal cores were checked by tools that can no longer be re-run. This program restates each kernel's formal core as a sealed, self-contained Lean 4 statement and re-proves it under a pinned toolchain (Lean v4.28.0, Mathlib 8f9d9cff). This revision treats the Restoration kernel, which decides whether a planted cluster on degraded land is large enough to grow into forest. Its formal core is the classical-nucleation cubic G(r) = -Delta mu r^3 + a sigma r^2 in the cube-root order parameter r = n^(1/3). We give a Lean proof of the sealed statement P2.Restoration. For positive Delta mu, a and sigma, the critical radius r* = 2 a sigma/(3 Delta mu) is positive and is the unique maximiser of G on r >= 0. For positive Delta mu, the barrier satisfies G(r*) = (1/2) Delta mu (r*)^3. The proof is a restructured port of the archived canon proof and rests on the factorisation G(r*) - G(r) = Delta mu (r - r*)^2 (r + r*/2). We also observe that the canon proof replays verbatim under the pinned toolchain, and that the half-barrier identity does not need its positivity hypothesis. We set out what the theorem settles, namely the go/no-go geometry inside the model, and what it leaves to field evidence: the parameter values, the adequacy of classical nucleation theory for tree-cluster establishment, nucleation rates and stochastic establishment, the seed-allocation result in the same canon file, and conformance of the deployed code. The earlier Carbon Continuity result and the three statement proposals are retained. Verification. a Lean 4 proof of P2.Restoration, a statement fixed before the proof attempt, machine-checked against Mathlib and replayed through the Lean kernel using only the standard axioms Run record, certification page and reproducible package: https://github.com/jdhart81/viridis-research/tree/main/runs/2026-10-31_P2 AI use: this version was drafted by an AI research agent (Claude, by Anthropic) running the Viridis research engine. Formal claims are checked by the Lean 4 kernel and labelled by an automated verifier. Justin D. Hart directs the research and is the accountable author. No AI system is listed as an author.