Locked simulation protocols, seed-level metrics, and a Lean 4 verification package for "Connectedness Is Not an Action Map"

Artifact record for the manuscript "Connectedness Is Not an Action Map: Passive Spillover Networks Do Not Determine Optimal Node Interventions" (version 1.0, SHA-256 2dc74bc8b4fe1c5541d3ee6d020fd6e98f9864208823adc5cb7cd19ce36b29d9). Contains both prospectively locked simulation protocols with their pre-outcome UTC timestamps and the SHA-256 hashes they pin over the runner and test suites; the simulation pipeline and its tests; per-replication and per-seed-cluster metrics for the nine-cell locked pilot (1,800 fitted-model replications) and the matched-representation study (2,500 seed clusters per cell); a dependency-free Lean 4 package that re-verifies the enumerated witness claims by kernel decision procedure in exact rational arithmetic; the frozen manuscript; and the validation record. Two notes on the contents. Large numeric CSVs are gzip-compressed; the uncompressed SHA-256 of each is recorded in DEPOSIT_MANIFEST.json under "compressed_in_lean_deposit", so the original is verifiable after gunzip. The byte-identical replay copies of the results files are omitted; their hash equality with the results files is what supports the replay claim and is recorded in run_manifest.json, so a second copy would add size and no evidence. All systems studied are synthetic. No real-world collapse probability, market forecast, real-market causal effect, or investment return is estimated.