Viridis Compiled Theorem Stack — Canon v5 (Dendritic Corridor Formation)

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 (v5). Added EcoChain dendritic-corridor formation (18 modules). Superseded as head by v9.1.1; the concept DOI resolves to the latest version.