Module addition is one action: refuse when the partition authorities are incomplete

[gunbai-bot]

Starting standing

Adding one extdeps module to the tree required three separate hand commits, each discovered by its own CI round trip:

1. ci.yml's heal exclusion list
2. the stage0 seed .rs
3. the crate partition roster plus a lib.rs mod line

Throughout all three, generated_artifact_gate main_wet reported zero drift while the crate would not compile. Precedent for the same class: #7865.

The defect is not what "the gate lies" first suggested

The gate does not miss drift. Within its registered roster it regenerates every artifact and compares bytes, and it is complete. Its roster simply does not cover the emitted stage0 seed or the partition-crate lib.rs files — those belong to regen_stage0, a different binary.

So zero drift never meant the tree is consistent. It meant the artifacts I am registered for match — a scope statement read as a tree statement. That is why every verdict here carries its own extent: a clean answer that omits its denominator invites exactly that misreading, and the misreading is not a reader error when the verdict withheld the population.

The invariant took three wrong candidates

Each is recorded in the carrier, because each would have shipped a gate that refuses correct rows:

Candidate	Why it is wrong
every emitted module is in some crate roster	75 of 138 emit-plan modules are legitimately unassigned and live in the monolith crate
a crate's modules reference only roster-mates	use crate::NonEmptyVec names a type, not a module
...reference only its own pub mod set	crates reach each other through glob re-exports (pub use v1_stage0_std_core::*)

What survives: reference closure over the reexport-transitive set — a module owned by crate C may only reference modules reachable from C, where reachable is C's own modules plus, transitively, the modules of packages C re-exports.

Both reference sources are imprecise, in opposite directions — measured, not assumed

• Import lists UNDER-approximate. dag/std/syntax.dag, coercion.dag and http_path.dag declare zero imports while referencing std_types. An empty import list is the maximal under-approximation, so an import-list check finds nothing unreachable and passes while the crate cannot resolve — the same fail-open this gate closes, one authority over.
• The .dag binding graph OVER-approximates the emitted crate's needs. It proposed four unreachable targets on clean main and all four are false: three name modules the emitter produces no file for, and std_pareto -> std_logic is a .dag reference the emitter never turned into a use crate:: line.

Neither alone is the emitted crate's requirement. So the binding graph is a candidate generator and the emitted artifact confirms exactly. This is a narrowing by an exact check, not a widening failure arm — a confirmed defect is still typed, located and counted.

Reading emitted Rust is a declared realization-side observation, admitted because the structure is genuinely absent upstream: which .dag references become emitted use lines is the emitter's decision and is not recoverable from the .dag graph. Dissolve-on: the emitter exposes its per-module emitted reference set, at which point the confirmation reads that fact and the text scan deletes.

Authorities consumed, not forked

• Edges: dependency_resolution_facts_live, whose own contract states "do not add a second edge producer beside it; the swap replaces its body" — so this is correct today (import ∪ reference facts) and after the accepted-binding cutover, with no edit here.
• Emitted spelling: stage0_module_emit_basename. Hand-spelling dots-to-underscores would have been a second naming scheme for something an authority already names (§3), and a per-character walk over a quadratic primitive besides.

Evidence — green by execution, all seven

Positive controls

• w_live_corpus_partition_closure_holds — the live corpus HOLDS. This is what reds if any of the three discarded candidates is reintroduced.
• w_transitive_reexport_is_reachable — std-surface reaches std-core modules.
• w_reachability_is_not_universal — a crate re-exporting nothing does not see another crate's modules, so reachability cannot be vacuously true.
• w_verdict_carries_its_extent — both arms report crates, modules and edges considered.

RED controls (a roster row removed from a copy of the live rows — the incident shape, not a synthetic)

• red_missing_roster_row_refuses — a missing roster row REFUSES. If this holds, the gate is the lie it replaces.
• red_refusal_names_the_incomplete_authority — the refusal names the importer, the owning package, the target, and which of the two hand authorities is short a row.
• red_reports_every_incomplete_authority_in_one_run — two missing rows are BOTH reported in one run. A refusal that stops at the first would re-serialise exactly the round trips this gate exists to collapse.

Displaced cost

	before	after
CI round trips to add one module	3	0 — one local run names every incomplete authority
gate verdict on a non-compiling tree	zero drift	typed, located refusal naming module, crate, target and authority

Bounds, stated rather than left to be discovered

• The verdict costs ~5m20s wall, dominated by the corpus-wide resolve the edge producer performs. That is the same order as the measured 5m35s front-door cost that closed a per-PR consumer, so this belongs on the regen/gate path that already resolves the tree, not as a new per-PR step. Not enrolled in the per-PR floor in this PR.
• Scope is the partition-closure question only. It does not verify unique crate ownership — v1_compiler_artifact currently appears in two crate rows, so a uniqueness assertion would refuse main today. Naming that as unmeasured rather than implying coverage.
• The crate-layout derivation program (DESIGN's emitted-crate-partition thread) is untouched; assignment stays hand-listed.