Route-gap admission partition: undeclared enrollment refuses; suppressed enrollments named per identity

dag/gunbc/floor/floor_route_gap_seed_growth.dag

@@ -5,16 +5,16 @@ import gunbc.seed_growth { SeedGrowthJustification }
 import std.decl_ref { DeclarationRef, WholeDeclaration }
 
 // FORWARD-FREEZE RECEIPT for the typed route-gap expectation consumed by the required floor.
-// The modeled authority is v2.workflow.floor_route_gap FloorRouteGapExpectation; these three
+// The modeled authority is v2.workflow.floor_route_gap FloorRouteGapExpectation; these four
 // declarations are its seed-side realization at the interpreter boundary, not a second policy.
 data floor_route_gap_seed_growth_justification: SeedGrowthJustification = SeedGrowthJustification {
   hand_authored_declarations: [
-    DeclarationRef { module_path: "v1_compiler.cli_run", decl_name: "FloorRouteGapExpectedGround", field: WholeDeclaration },
-    DeclarationRef { module_path: "v1_compiler.cli_run", decl_name: "FloorRouteGapExpectation", field: WholeDeclaration },
-    DeclarationRef { module_path: "v1_compiler.cli_run.required_floor_runner", decl_name: "floor_route_gap_expectation_mismatch", field: WholeDeclaration }
-  ],
-  reason: "WHY RUST IS STILL NEEDED: the required floor executes in the seed, and v1_compiler.cli_run is the boundary that receives v1_interpreter.HermeticEffectGround after a claim executes. v2.workflow.floor_route_gap owns the expectation vocabulary and population; the Rust realization decodes that authority and refuses when the observed operation or closed ground differs, instead of letting an identity-only enrollment absorb changed evidence. A modeled row without this consumer cannot constrain the host terminal ledger.\n\nWHY IT IS ADMITTED AGAINST THE v1 FREEZE: gunbc.v1_maintenance_standing v1_seed_standing admits work serving the v2 self-host program. The required floor is the instrument guarding that program, and this change strengthens a pre-existing route-gap debt roster from identity-only agreement to operation-and-ground agreement. It adds no language behavior, compatibility route, escape hatch, seed feature, or emitted public surface.\n\nHAND-ITEM DELTA: +3, exactly the closed ground mirror, the decoded expectation record, and the pure mismatch classifier enumerated above. All other Rust edits are inside existing declarations and are ExistingSeedItemModified.\n\nHAND-LOC DELTA AT THIS RECEIPT: src/v1/stage0/src/cli_run.rs +223/-49 and src/v1/stage0/src/bin/claim_executor.rs +5/-5 against origin/main. The latter adds no declaration. The item observation producer is currently absent, so these diff-derived figures remain review evidence rather than a mechanically joined admission.",
+    DeclarationRef { module_path: "v1_compiler.cli_run.required_floor_runner", decl_name: "ROUTE_GAP_ADMISSION_PARTITION_ENTRY", field: WholeDeclaration },
+    DeclarationRef { module_path: "v1_compiler.cli_run.required_floor_runner", decl_name: "route_gap_suppressed_rows_value", field: WholeDeclaration },
+    DeclarationRef { module_path: "v1_compiler.cli_run.required_floor_runner", decl_name: "route_gap_declared_map_value", field: WholeDeclaration },
+    DeclarationRef { module_path: "v1_compiler.cli_run.required_floor_runner", decl_name: "route_gap_admission_decode_and_enforce", field: WholeDeclaration }
+  ],  reason: "WHY RUST IS STILL NEEDED: the required floor executes in the seed, and v1_compiler.cli_run is the boundary that receives v1_interpreter.HermeticEffectGround after a claim executes. v2.workflow.floor_route_gap owns the expectation vocabulary and population; the Rust realization decodes that authority and refuses when the observed operation or closed ground differs, instead of letting an identity-only enrollment absorb changed evidence. A modeled row without this consumer cannot constrain the host terminal ledger.\n\nWHY THE ADMISSION PARTITION IS MODELED, WITH FOUR COUNTED HAND ITEMS: the partition decision — INCLUDING the membership judgment — is modeled on the authority itself: v2.workflow.floor_route_gap.floor_route_gap_admission_partition, the single implementation of the route-gap admission decision, receives the discovery walk's declared-identity index WHOLE AS A KEYED MAP and asks map_contains_key per suppressed row, so refuse-if-undeclared is decided by the .dag relation, not by the marshal. The runner does no membership test: a Rust-side contains_key would BE the judgment made outside the authority, and flattening the index into a list for the .dag to linearly re-scan was the corpus-sized join this shape retires (a per-row linear contains over the required-run census — declared in the tens of thousands, suppressed in the hundreds — is millions of interpreted string comparisons per required run, the cost-shape defect DESIGN.md §6 always fixes; the keyed map keeps the judgment in .dag at one O(1) lookup per suppressed row). An earlier revision carried a Rust classifier (route_gap_suppressed_undeclared) beside the modeled relation; it was DELETED rather than kept beside the .dag call, so the decision — membership and arms both — has one implementation and the seed decision surface shrank by that classifier. What feeds the relation and enforces its answer could not vanish with it: the entry name the run site and the pairing witness share (ROUTE_GAP_ADMISSION_PARTITION_ENTRY), the shared suppressed-row marshal (route_gap_suppressed_rows_value), the shared declared-index marshal (route_gap_declared_map_value, which spells the index's disposition values through required_floor_disposition_label), and the shared production decode+enforce (route_gap_admission_decode_and_enforce, extracted from run_required_floor so the misnamed fixture's refusal flows through the actual production branch) are four new module-scope seed items, counted in the delta below. The row marshal's ground decoding is inlined in that marshal, the arm-for-arm spelling after v2.workflow.floor_route_gap FloorRouteGapSuppressionGround, so a rename on either side breaks the pairing instead of forking the vocabulary.\n\nWHY IT IS ADMITTED AGAINST THE v1 FREEZE: gunbc.v1_maintenance_standing v1_seed_standing admits work serving the v2 self-host program. The required floor is the instrument guarding that program, and this change strengthens a pre-existing route-gap debt roster from identity-only agreement to operation-and-ground agreement, and closes its undeclared-enrollment hole. It adds no language behavior, compatibility route, escape hatch, seed feature, or emitted public surface.\n\nHAND-ITEM DELTA: +4, all in v1_compiler.cli_run.required_floor_runner and all enumerated above: the shared entry name (ROUTE_GAP_ADMISSION_PARTITION_ENTRY), the shared suppressed-row marshal (route_gap_suppressed_rows_value), the shared declared-index marshal (route_gap_declared_map_value), and the shared production decode+enforce (route_gap_admission_decode_and_enforce — the branch run_required_floor executes on the partition's answer, extracted so the pairing test drives the SAME function and the misnamed fixture produces the actual REQUIRED-FLOOR REFUSAL cause=RouteGapEnrollmentUndeclared). The arm spelling inside the suppressed-row marshal is inlined (no nested hand declaration). All other Rust edits are inside existing declarations and are ExistingSeedItemModified.\nHAND-LOC CENSUS, BEFORE AND AFTER, AT THIS RECEIPT: against origin/main, `git diff --numstat origin/main..HEAD` over the eight files of this PR re-derives 1164 insertions and 15 deletions; the seed realization's own line count in v1_compiler.cli_run/required_floor_runner.rs moves by +638/-7 (production +256/-7, the #[cfg(test)] pairing witness and its tests +380). The item observation producer is currently absent, so this diff-derived census remains review evidence rather than a mechanically joined admission.\n\nHAND-LOC DELTA AT THIS RECEIPT, all eight files: src/v1/stage0/src/cli_run/required_floor_runner.rs (call-site marshals + modeled-partition call + shared decode+enforce, per-identity measurement record, refusal, pairing witness through run_in_context_with_args, tests), src/v2/workflow/floor_route_gap.dag (contract amendment + the modeled partition), src/v2/workflow/required_floor.dag (one exact-grain authored-module row for test.claim.route_gap_partition_witness), src/v2/test/fixture/route_gap_admission_partition.dag (the shared fixture: four rows, both arms, all three grounds), dag/test/claim/route_gap_partition_witness_test.dag (the floor-side route witness), dag/gunbc/floor/floor_route_gap_seed_growth.dag (this receipt), dag/gunbc/recurring_failure_mode/an_unimported_bare_name_binds_differently_per_realization.dag (the unimported-bare-name divergence row), docs/plans/route-gap-dormant-observation.md (the finding doc). The item observation producer is currently absent, so these diff-derived figures remain review evidence rather than a mechanically joined admission.",
   owning_dissolution_lane: "v1-hand-queue-drain" as RoadmapNodeId,
-  trigger: "Delete the three seed declarations when the self-emitted claim executor executes the required floor and consumes v2.workflow.floor_route_gap FloorRouteGapExpectation directly; the modeled expectation then remains the sole authority and the hand-written decode/classifier disappears with the v1 floor bridge.",
-  current_boundary: "v2.workflow.floor_route_gap FloorRouteGapExpectation -> v1_compiler.cli_run FloorRouteGapExpectation -> v1_compiler.cli_run floor_route_gap_expectation_mismatch -> v1_compiler.cli_run run_required_floor"
+  trigger: "Delete the four seed declarations when the self-emitted claim executor executes the required floor and consumes v2.workflow.floor_route_gap FloorRouteGapExpectation directly; the modeled expectation, the modeled admission partition, and its declared ground coproduct then remain the sole authorities and the hand-written decode/classifier disappears with the v1 floor bridge.",
+  current_boundary: "v2.workflow.floor_route_gap FloorRouteGapExpectation and floor_route_gap_admission_partition -> v1_compiler.cli_run FloorRouteGapExpectation -> v1_compiler.cli_run.required_floor_runner floor_route_gap_expectation_mismatch and the run-site marshals -> v1_compiler.cli_run run_required_floor"
 }

dag/gunbc/recurring_failure_mode/an_unimported_bare_name_binds_differently_per_realization.dag

@@ -0,0 +1,24 @@
+module gunbc.recurring_failure_mode.an_unimported_bare_name_binds_differently_per_realization
+
+import std.types { NonEmptyStr }
+import gunbc.recurring_failure_mode { RecurringFailureMode }
+
+// AN UNIMPORTED BARE VALUE NAME IS RESOLVED TWICE -- once per realization of the language -- and
+// the two resolutions have different fallback rules, so one name can mean two functions. The
+// interpreter's search over declaring modules and the emitter's mapping to runtime builtins are
+// two realizations of one resolution decision, and nothing forces them to agree: where the
+// arities happen to differ the emitted build refuses (loud, costly, caught late), and where they
+// happen to match the program compiles and SILENTLY runs the wrong function in one realization.
+// The wall is the authored import: an imported name has one binding by construction, while a
+// bare name with no import anywhere is a resolution the author never made.
+data an_unimported_bare_name_binds_differently_per_realization: RecurringFailureMode = RecurringFailureMode {
+  identity: "an_unimported_bare_name_binds_differently_per_realization" as NonEmptyStr,
+  receipts: [
+    "SPECIMEN, FOUND 2026-10-05. `v2.workflow.floor_route_gap.floor_route_gap_admission_partition` (PR #13376) called `contains(xs: declared, item: row.identity, eq: floor_route_gap_string_eq)` WITHOUT importing `contains`. The interpreter resolved the bare name to `v2.std.algebra.contains` (the generic list-membership function, src/v2/std/algebra.dag:201) and every .dag-level claim and pairing lib test evaluated green. The emitter resolved the same bare name to `v1_rt::contains` -- the 2-parameter String substring builtin (src/v1_rt.rs:332) -- and lowered the call as `v1_rt::contains(declared.clone(), row.identity.clone(), floor_route_gap_string_eq)`, failing the emitted build with error[E0061] 'this function takes 2 arguments but 3 arguments were supplied' at emitted src/v2_workflow_floor_route_gap.rs:2139:106; the String/Rc<im::Vector<String>> type note was the tell that the bound function was the substring builtin, not list membership.",
+    "WHY THE LOCAL BATTERY COULD NOT SEE IT: the interpreter's resolution is the only resolution every .dag-level check exercises, so a bare name that binds differently per realization evaluates consistently green on every interpreted lane; emission is the only lane that runs the emitter's fallback, which made CI's emit-build the sole discriminator. A green interpreter run is not evidence that a name means the same thing in the other realization.",
+    "WHY THE CORPUS DID NOT CATCH IT AT REVIEW: the corpus always imports this name (src/v2/lens/coverage.dag:3, src/v2/workflow/vocab.dag), so the unimported form contradicted the convention but enforced nothing -- a reader who assumed the convention was a rule saw nothing wrong in the module text.",
+    "REMEDY AT THE SOURCE: author the import so the name has one binding (`import v2.std.algebra { contains }`); in the specimen's final shape the call itself was retired by the keyed-map membership fix (side-chat review 5424676896 / review 76768), which is why the class guard is import discipline plus a resolution-time refusal, not any one call site. The class guard this row asks for, NARROWED TO THE FAILING CLASS: a bare VALUE name that has no local declaration, no import, and no admitted intrinsic -- a name that would otherwise bind through a realization-specific FALLBACK (the interpreter's declaring-module search, the emitter's runtime-builtin mapping, the two rules this specimen caught diverging) -- refuses at resolution time with a typed, located cause ('bare name X is not imported and names no intrinsic'); bare names the language admits as intrinsics in every realization (map, fold, count, the emitter-handled builtins) are legitimate unimported and stay outside the guard, as does any name imported somewhere visible. The existing ambiguity wall (claim_scope_for's AmbiguousBareNameRead) fires only when two declarers are visible, and an unimported non-intrinsic name with one declarer visible per realization is not ambiguous, just different.",
+    "NEXT-RUNG TRIGGER: the loader's bare-channel decision carried as a substrate fact -- per declined bare name, the declining arm and the declaring module -- is the observation that would make 'resolved by fallback' readable at one authority (the bare_reference_channel_outcome_seed_growth trigger); the resolution-time refusal above is what closes the class."
+  ],
+  evidence: [],
+}