Re-certifying the Carbon Continuity Threshold: A Lean Proof of the Two-Pool Regenerative Coupling Condition under a Pinned Toolchain

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. The live Viridis OS kernel Carbon Continuity decides whether a two-pool carbon portfolio (a living pool and a durable pool) can be kept from shrinking across disturbance-recovery cycles. One cycle maps (L, D) to (aL + rD, pL + dD), with retention fractions a, d in [0,1) and transfer rates r, p > 0. The kernel's formal core states that a strictly positive portfolio that one cycle does not shrink in either pool exists exactly when (1 - a)(1 - d) <= rp. Until now this rested on a certificate from a retired checker. We restate the theorem as the sealed statement P2.CarbonContinuity and give a short Lean 4 proof under Lean v4.28.0 and a pinned Mathlib. The proof is ported from the archived canon release (Zenodo 10.5281/zenodo.21855690). Sufficiency uses the explicit witness (r, 1 - a). Necessity multiplies the two leakage inequalities and cancels the positive product LD. We say exactly what the theorem settles: the threshold logic the kernel applies. We also say what it does not settle: any coefficient value, the adequacy of the linear two-pool model, or any ecological or carbon-credit outcome. Those depend on field evidence. Verification. a Lean 4 proof of P2.CarbonContinuity, 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-29_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.