The Symbiotic Corridor Theorem: Co-Design Dominance and a Single Broadcast Price for Mutualistic Corridor Networks

Series S5 (Corridors & Spatial) of the Viridis Canon. The core Intelligence-Bound canon spine is unchanged (frozen at v10.1.0 “The Keystone Wave”, record 21223021); this record links to the spine via isDerivedFrom the concept DOI 10.5281/zenodo.19317982, and references the S5 series anchor, the Corridor Siting Theorem (record 20777068). Conservation corridors linking two or more mutualistic species have lacked a formal answer to a governance question: should the species' corridor networks be designed jointly, or can each be optimized in isolation and simply overlaid? The Symbiotic Corridor Theorem (SCT), “the Loom,” the 31st Intelligence-Bound self-application, proves that the joint per-edge objective is concave (so a unique co-design optimum exists), derives a clean sign law for when geometric-mean coupling between species is supermodular, and shows co-design strictly dominates siloed design exactly when that supermodularity condition holds — with demand across the coupled network governed, as in the single-species case, by one broadcast shadow price. Five results are machine-checked in Lean 4 (Aristotle, zero sorry, axioms ⊆ {propext, Classical.choice, Quot.sound}), namespace Viridis.SymbioticCorridor: (i) joint_objective_concave — the per-edge joint objective is concave; (ii) coupling_sign_law — geometric-mean coupling is supermodular iff μ ≥ 0; (iii) codesign_dominates_siloed_iff_supermodular — co-design strictly dominates siloed allocation iff supermodular; (iv) coupled_waterfilling_single_price — the decoupled limit recovers the prior single-species corridor result, with demand antitone in one broadcast price; (v) sct_nonvacuous — an explicit strict interior mutualistic witness. Deferred (measure-dependent, not in this record): the NODF-nestedness / critical-coupling argmax layer, and a tracking-rate-dynamics extension flagged for duplicate/vacuity risk against the IB core. Scope. The Lean proofs certify the validity of the reasoning, not empirical magnitudes. Working paper; not peer-reviewed.