Viridis Compiled Theorem Stack — Canon v10.0.0 (The Core-Extension Wave: SIB + MRAB + Biosphere-Productivity Bridge folded into the spine)

The Viridis Canon — Lean-Checked Conditional Mathematics for the Intelligence Bound. A machine-checked formal corpus underpinning the Viridis research program on the thermodynamics of intelligence and its application to planetary conservation. Its spine is the Intelligence Bound — a Landauer/erasure-grounded limit on the rate of intelligence creation — formalized in Lean 4 and extended through a stack of modules spanning information theory (the D-Score biodiversity metric), graph-theoretic landscape optimality (HDFM / dendritic corridors), thermodynamic economics, alignment-as-feasibility (Goodhart impossibility), the speed-limit shadow-price tower, and the recovered post-Wolpert erasure-side footing. Every theorem's type is machine-verified in Lean 4 (pinned toolchain; axioms audited to {propext, Classical.choice, Quot.sound}). The canon deliberately distinguishes proof validity from physical and empirical validity: it is conditional mathematics with explicit assumptions, not a claim that those assumptions describe nature. Headline results are graded by formal strength in CLAIMS_MATRIX.md via the labels in THEOREM_STATUS_TAXONOMY.md (Derived / Conditional / Definition-expansion / Bridge-assumption / Empirical-hypothesis / Conjecture / Exploratory), with separate formal and interpretive status. Empirical validation is reserved for the companion papers and field studies. Concept DOI 10.5281/zenodo.19317982 always resolves to the latest version. Source mirror: github.com/jdhart81/viridis-canon. Co-authored with Aristotle (Harmonic). This version (v10.0.0). The Core-Extension Wave — the first spine version since the v9 freeze. Folds the three accumulated Intelligence-Bound core-extensions into the verified spine: the Symbiotic Intelligence Bound (two-body generalization; 5 thm), the Multi-Ring Alignment Bound (multi-domain/polymath generalization with the UAIB reduction to the master bound; 10 thm), and the Biosphere-Productivity Bridge (IB ⇄ biosphere-productivity duality). Both newly promoted modules are 0 sorry with axioms ⊆ {propext, Classical.choice, Quot.sound}, added to SPINE_MANIFEST.txt, lakefile defaultTargets, and AxiomAudit.lean. Authorized as an explicit per-instance freeze-break; spine now frozen at v10. See CHANGELOG_v10.0.0.md.