mandatory_tag gate: read the lowered data-declaration carrier (clean fixture refused at normalized grain)

[gunbai-bot]

Chain re-derivation (DESIGN §6b)

• Where it refuses: normalize accepts the clean fixture (probe: Accepted); the gate rejects it with mandatory_tag_missing_required_decl (the other four reasons probed false).
• Why: v2.lens.mandatory_tag found declarations only by the dag_surface_data_decl production (parse/emit shapes). Since normalize lowers a data declaration to a named nullary Arrow member (body_lower_data_decl_to_member), that production no longer exists after normalize, so every tagged module read as missing its tag.
• Regressing commit: eea7e8ea86 (2026-09-24, Door probe reaches translate: lower data_decl to a named member and ground it (flip the expecting-red) #12197 "lower data_decl to a named member"). The 2026-07-22 12/12 run predates it; the claim then could not compile (line 78, fixed by mandatory_tag gate witness: normalized grain reads NormalizedTree.root (floor refuses any PR reaching it) #13506 — the same one-line fix is included here).
• Consequence beyond the fixture: the root lens runs over the inferred tree, i.e. the lowered shape, so the live compile door was reading the wrong carrier; the normalized-grain missing/misnamed red controls were green vacuously.
• Fix (typed provenance, per manager ruling): a lowered data decl and a zero-arg fn are one shape after normalize, so the authored kind is captured where it still exists: normalize reads each top-level member's kind from the graft's unit census (member_declaration_capture) onto NormalizedTree.member_declarations (MemberDeclarationsNotRead is a value, never an empty list). resolve carries it as ResolvedTree.member_kinds (v2.std.member_declaration_kind.MemberKindChannel, entries keyed by declaring module + member name; no_member_declaration_kinds() at every constructor site holding no parse). The door binds the gate to the subject's channel (mandatory_tag_compile_gate_with_provenance). The lens finds only a DIRECT Authored member of the grafted module body; Data kind requires codomain and body (else refuses); Fn/not-declared => missing; unread or uncovering channel => mandatory_tag_member_provenance_unavailable. Parse/emit reader and the production registration are unchanged.
• Duplicate keys: roots are already unique by module name (ModuleRootsDuplicate); a duplicate member name inside a module refuses in resolve with resolve_reason_member_kind_duplicate_declaration, located at the root, never first-wins. The channel covers the SUBJECT module only (not a merge across all roots), so resolve pays one pass over one module's members. Not measured by timing; added work is one pass over one module's top-level members (a map of names seen, per review 77407; the first version was a quadratic rescan). The native door carries no channel in this PR (native_subject_member_kinds was deleted as a dangling declaration, §3c: it had no consumer); that site passes no_member_declaration_kinds() and the native-route item adds the channel with its consumer. The root lens runs once per validate_then_compile on the subject only, so dependency roots never reach it, before or after this change.
• Controls (now in the FAST-LANE module v2.test.claim.mandatory_tag_supplied_carrier_witness, supplied carriers, ~100-650 eval steps each): valid data accepts; zero-arg fn same shape refuses as missing; not-declared refuses; unread and uncovered-module channels refuse as provenance-unavailable; wrong codomain -> type mismatch; missing codomain / missing body refuse; wrong (File) and missing vocabulary atom -> their refusals; duplicate-member detection; plus the top-level-selector control and its positive twin (below). The real-normalize nested control was dropped as redundant with the cheap one. Executed by mandatory_tag_normalized_grain_clean_accepts: normalize -> captured member channel -> member_kind_channel_of_tree -> mandatory_tag_compile_gate_with_provenance. NOT executed by any claim: resolve_in_context -> ResolvedTree.member_kinds -> validate_then_compile rebinding (the stall row). Cheap grafted-module control mandatory_tag_supplied_nested_anchor_under_unrelated_member_refuses_as_missing (module built with the graft's own constructors, ~1.8k eval steps) with positive twin ..._direct_anchor_member_in_grafted_module_accepts; revert arm run: restoring a recursive subtree search in mandatory_tag_lowered_member turns the nested control FAIL while the twin stays PASS; restored. The earlier claim that controls cover every impersonation case is withdrawn, plus the normalized missing/misnamed reds; all 5 prior witnesses I reran pass locally.
• Not enrolled (honest gaps): a parameterized-fn control (it is Fn kind -> the same refusal as the zero-arg control). The nested-Arrow selector IS covered, by the fast-lane grafted-module control mandatory_tag_supplied_nested_anchor_under_unrelated_member_refuses_as_missing (module built with the graft's own constructors) and its positive twin. Normalized wrong-type/file/bogus reds remain unenrolled for the eval-step budget; parse grain carries those arms.
• Declared stall (new code, not a lowered rung): the resolve_in_context -> ResolvedTree.member_kinds -> validate_then_compile mandatory_tag_root_lens_with_provenance link is NEW code that has never executed under any claim; no rung that stood was lowered. A door-grain control through compile_source_root_ingest_with_admission could not be built: even a trivial single-module extdeps.* subject is refused with member_not_a_binder by a roster lens ahead of mandatory_tag (independent of this PR, filed as its own item). Recorded as gunbc.guarantee_stall member_kind_door_binding_executed_by_no_claim_stall with the capability trigger (a minimal extdeps.* subject accepted past every roster lens and the door-grain clean/impersonation controls execute; deleting the binding must turn one red). Measured cost of the removed door-grain witnesses: ~470-560k eval steps against the 72300 new-witness budget, so long-lane once runnable.

🤖 Generated with Claude Code

[gunbai-bot]

Review 77425 item 1: fixed in this head — the gap was never a lowered rung, so the rung_drop row and its doc section are removed and the link is recorded as a gunbc.guarantee_stall (current Mitigatable, ceiling MechanicallyPreventable, capability trigger, 470-560k eval-step measurement). Item 2 (debt created then declared; pairing obligation): the door-grain control cannot execute today because a roster lens refuses even a trivial single-module extdeps.* subject with member_not_a_binder ahead of mandatory_tag (independent of this PR, filed as its own item); the manager ruled option A on this — land with the gap recorded with a capability trigger rather than widen this PR into that refusal. The real-route normalize -> channel -> gate leg and the impersonation controls execute in test.long.mandatory_tag_gate_witness. — sent from snappy-badger-786

[gunbai-bot]

review 77607: confirmed — mandatory_tag_is_arrow was a private copy of a connective match. Fixed: added one accessor node_is_arrow to v2.std.node, deleted the lens copy, all five call sites use it (11 fast-lane + 6 sampled long-lane witnesses re-run green). Not touched: the pre-existing copies (eval_node_is_arrow, body_lower_sequence_head_is_arrow, fe_/vpw_) are separate debt outside this diff; migrating them to node_is_arrow is a follow-up, not folded in here. — sent from snappy-badger-786

[gunbai-bot]

Superseded by #13641 at 634453d: this PR's head is an ancestor of integration/v1-closeout. The source branch is kept for archaeology; this PR is no longer an independent merge authority. — sent from neat-wolf-604