The Mutualistic Inference Network Theorem: Lifting Symbiotic Inference to N-Agent Predictive Commons under the Intelligence Bound

Standalone record of the Viridis Canon (Mutualistic Inference Networks). 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. We formalize the Mutualistic Inference Network Theorem (MINT), “the Mutualist” — the 27th Intelligence-Bound self-application. MINT lifts the Symbiotic Inference Theorem (SIT, a two-agent result) to an N-agent predictive commons: a network of agents that share partial information about a shared environment, each paying an inference cost and each drawing a synergistic subsidy from the group's redundancy and synergy structure. Six results are machine-checked in Lean 4 (Aristotle, zero sorry, axioms ⊆ {propext, Classical.choice, Quot.sound}), namespace Viridis.MutualisticInference: (i) mint_network_ledger_no_penalty — the predictive commons never penalizes a participant relative to going it alone; (ii) mint_dyad_recovers_sit — the N=2 floor recovers the certified SIT dyad value exactly (3/2), pinning the network result to prior canon and witnessing non-vacuity; (iii) mint_pid_subsidy_nonneg_le_total — the synergistic subsidy is well-defined and bounded, 0 ≤ S ≤ I_total; (iv) mint_group_markov_blanket_ceiling — an additive group Markov-blanket ceiling; (v) mint_efficiency_eq_cos2_theta — allocation efficiency is a discrete cos²Θ alignment measure in [0,1] via Cauchy–Schwarz; (vi) mint_mutualist_IB_ceiling — the headline result: the group's total information-acquisition rate is Intelligence-Bound-limited, and open, mutual prediction strictly beats solo inference whenever the subsidy is positive. MINT sits alongside the Universal Water-Filling Meta-Theorem (UWMT) and Geodesic Saturation Theorem (GST), both admitted to spine v10.1.0, as a downstream application of the water-filling/shadow-price machinery to the cognitive-modeling × symbiosis domain, rather than a domain-defining extension itself — hence its standalone (not spine) routing. Scope. The Lean proofs certify the validity of the reasoning, not empirical magnitudes. Working paper; not peer-reviewed.