v2 resolve/infer: the dotted-path decision keeps its binding kind, and projection inference stops calling an unretrievable declaration a fieldless receiver

dag/gunbc/generic_binder_field_projection_deficit.dag

@@ -77,7 +77,7 @@ data generic_binder_field_projection_sites: List<GenericBinderProjectionSite> =
   GenericBinderProjectionSite {
     site: decl_ref(
       module_path: "v2.test.claim.fold_lowering",
-      decl_name: "lowered_loop_binds_carrier_binder"
+      decl_name: "lowered_loop_carrier_is_a_generated_slot_not_the_authored_binder"
     ),
     index_coverage: OutsideDeclIndexTestWitnessModule,
     scrutinee_type: "Optional<Node>",

dag/gunbc/non_fold_residue.dag

@@ -175,6 +175,9 @@ data nfr_reason_typed_census_undetermined_node_kind: String = "the v1 checker le
 
 data nfr_reason_landed_after_typed_census: String = "a top-level wildcard arm over a closed coproduct that landed on main after the ca5ed1724b typed census, while that census's roster was still in review (#12980); the floor's diff-scoped typed walk named it on the roster PR's own run. Un-migrated modeling (DESIGN §6), rostered so the ratchet stays armed at unrostered=0"
 
+data nfr_reason_eval_projection_receiver_not_aggregate: String = "field projection at eval: RuntimeAggregate is the one RuntimeValue variant that carries named fields, and every other variant refuses with the same located eval_rejected_projection_receiver_not_aggregate; enumerating them would clone one refusal arm per variant. Landed with gunbc#12506's field-projection eval route; declared at landing so the ratchet arms with the code"
+
+data nfr_dissolve_eval_projection_receiver_not_aggregate: DissolutionCondition = unbound_dissolution(description: "RuntimeValue exposes a typed field-bearing projection (derived from its declaration, dag/std/algebra) so eval reads fields without a per-variant match, and this row deletes")
 
 data non_fold_residue_frontier: List<FrontierRow> = [
   FrontierRow { subject: PathSubject { path: "dag/gunbc/instruments/fabric_control_plane_live_probe.dag::fci1_slot_prestate_equal" }, reason: nfr_reason_fci1_prestate_equal, dissolution: nfr_dissolve_fci1_prestate_equal },
@@ -1934,6 +1937,11 @@ data non_fold_residue_frontier: List<FrontierRow> = [
   FrontierRow { subject: PathSubject { path: "src/v2/compiler/body_lowering_fold.dag::body_lower_where_leaf_atom_optional" }, reason: nfr_reason_landed_after_typed_census, dissolution: nfr_dissolve_owning_fold },
   FrontierRow { subject: PathSubject { path: "src/v2/compiler/body_lowering_fold.dag::body_lower_where_predicate" }, reason: nfr_reason_landed_after_typed_census, dissolution: nfr_dissolve_owning_fold },
   FrontierRow { subject: PathSubject { path: "src/v2/std/qualified_name.dag::lexical_reference_label_optional" }, reason: nfr_reason_landed_after_typed_census, dissolution: nfr_dissolve_owning_fold },
+  FrontierRow {
+    subject: PathSubject { path: "src/v2/compiler/05_eval.dag::eval_field_projection_of_receiver" },
+    reason: nfr_reason_eval_projection_receiver_not_aggregate,
+    dissolution: nfr_dissolve_eval_projection_receiver_not_aggregate,
+  },
 ]
 
 fn non_fold_residue_frontier_units() -> List<String> {

dag/gunbc/recurring_failure_mode/infer_child_context_cannot_depend_on_a_sibling_result.dag

@@ -0,0 +1,26 @@
+module gunbc.recurring_failure_mode.infer_child_context_cannot_depend_on_a_sibling_result
+
+import std.types { NonEmptyStr }
+import std.decl_ref { DeclarationRef, WholeDeclaration }
+import gunbc.recurring_failure_mode { RecurringFailureMode }
+
+data infer_child_context_cannot_depend_on_a_sibling_result: RecurringFailureMode = RecurringFailureMode {
+  identity: "infer_child_context_cannot_depend_on_a_sibling_result" as NonEmptyStr,
+  receipts: [
+    "INVALID STATE: v2.compiler.infer infers every child subtree independently before its parent's behavior row executes. A Loop domain's SYNTHESIZED element type is required to instantiate the step member formal's fresh type variable, but no inference traversal can carry one child's settled result into another child's inference context. The fold encoding compounds it by storing the step BEFORE the domain (v2.compiler.fold_lowering fold_recurrence_encoding emits Positional step as child 0 and the named loop_domain_edge as child 1), so ordinary left-to-right child order cannot supply the relation either. HARM: the valid helper `fold(root.children, init: false, f: fn(found, e) { found || g_tree_has_arrow_body(root: e.target) })` is refused at `e.target` with infer_reason_projection_receiver_declares_no_fields -- `e` stays typed as its fresh variable instead of Edge, although the Loop domain carries `root.children: List<Edge>` and Edge declares `target: Node`. The refusal is typed and located and nothing is fabricated, so this is a capability gap on the loud side of the ladder, never a silent wrong answer.",
+    "DISTINGUISHING FACTS: this is NOT a missing loop_domain_edge reader, NOT cross-module declaration retrieval, and NOT a projection-classification defect -- each of those was measured and excluded. v2.std.node fold_node carries SYNTHESIZED results only from child to parent (step: fn(R, Edge, R) -> R, whose third argument is the child's already-folded result, computed by a recursive call that receives nothing from the parent). v2.std.node fold_node_topdown carries INHERITED context only from parent to child, and its child_context: fn(Node, A, Edge) -> A receives the parent node, the inherited context and the current edge -- no folded sibling result. So neither algebra expresses `infer the domain child, derive the member instance, then infer the step child under it`, and converting infer's gather from NodeFold to NodeFoldTopDown is a DISPROVEN route rather than the trigger: it would change the shape of the stage's single walk across all behavior arms and still not carry the fact. Adding the role reader, the domain consumer or the List<T> element relation before the traversal exists would make each declaration unreachable from any production verdict, which is the dangling modeling DESIGN section 3c forbids. The three facts the repair consumes already exist and are cited below: the fresh variable is minted by v2.std.anonymous_binder fresh_type_variable, the existing lambda-parameter route correctly derives the member formal AS that variable (v2.compiler.infer infer_lexical_reference_facts, reading the binding v2.compiler.resolve recorded in ResolvedTree.lexical_bindings), and the receiver rule that refuses is infer_projection_receiver -- so no second parameter-typing route may be introduced; the existing variable must be instantiated.",
+    "RUNG FOUND AT: mitigatable -- the compiler refuses rather than fabricating a field-bearing type, but valid fold programs cannot type. ATTAINABLE CEILING: structurally guaranteed -- the element relation is decidable from the domain's own type, and every fact it needs is already established by a stage that runs before the step subtree is judged; what is missing is one driver whose behavior-specific child schedule can infer a dependency child once, derive a scoped context from its settled result, and infer the dependent child once under that context. NEXT-RUNG TRIGGER, stated as the capability: an infer-local dependent-child driver schedules the Loop domain before the step, derives the collection-fold member instance from the domain type, extends a lexical TypeVariableInstance frame FOR THE STEP SUBTREE ONLY, and preserves the existing behavior rows, SUFFICIENT FOR the unchanged production helper to establish `e: Edge` and `e.target: Node`. Its discriminating red is a mutation deleting the domain-to-step context join, which must make that control fail. The element relation must be scoped by FOLD REALIZATION rather than by assuming every Loop is List<T>, and the role authority (the step callable's actual 0 is the carrier and actual 1 is the domain member, stated today in v2.compiler.fold_lowering) belongs in one decoder rather than being re-read per consumer.",
+  ],
+  evidence: [
+    DeclarationRef { module_path: "v2.compiler.infer", decl_name: "infer_entries_for_tree", field: WholeDeclaration },
+    DeclarationRef { module_path: "v2.compiler.infer", decl_name: "infer_gather_fold_algebra", field: WholeDeclaration },
+    DeclarationRef { module_path: "v2.compiler.infer", decl_name: "infer_gather_loop_row_on_entries", field: WholeDeclaration },
+    DeclarationRef { module_path: "v2.std.node", decl_name: "fold_node", field: WholeDeclaration },
+    DeclarationRef { module_path: "v2.std.node", decl_name: "fold_node_topdown", field: WholeDeclaration },
+    DeclarationRef { module_path: "v2.compiler.fold_lowering", decl_name: "fold_recurrence_encoding", field: WholeDeclaration },
+    DeclarationRef { module_path: "v2.test.parse.expression_bodied_fn_decl_parse", decl_name: "g_tree_has_arrow_body", field: WholeDeclaration },
+    DeclarationRef { module_path: "v2.compiler.infer", decl_name: "infer_lexical_reference_facts", field: WholeDeclaration },
+    DeclarationRef { module_path: "v2.compiler.infer", decl_name: "infer_projection_receiver", field: WholeDeclaration },
+    DeclarationRef { module_path: "v2.std.anonymous_binder", decl_name: "fresh_type_variable", field: WholeDeclaration },
+  ],
+}

dag/gunbc/rung_drop/match_arm_binder_typing_lost_to_lexical_carrier.dag

@@ -0,0 +1,51 @@
+module gunbc.rung_drop.match_arm_binder_typing_lost_to_lexical_carrier
+
+import std.types { NonEmptyStr }
+import gunbc.rung_drop { RungDrop, Standing, TypedDeclaration, DeletedWithoutReplacement }
+import gunbc.guarantee_rung { Mitigatable, StructurallyGuaranteed }
+
+// THE DECLARED RUNG DROP for match-arm binder typing (DESIGN 4b(3)), landed in gunbc#12506 under
+// calm-boar-904's ruling of 2026-10-02.
+//
+// WHAT IS DROPPED. gunbc#12641 typed a match-arm binder as the matched variant field's type at the
+// scrutinee's instantiation, so `artifact.tree` inside `Accepted { value: artifact, ... } => ...` was a
+// typed projection: an undeclared field off the binder refused, and the match was typed by its arms. That
+// typing rode on v2.compiler.infer infer_parameter_scope_search's arm-binder variants. gunbc#12766
+// restricted that search to lambda parameters, and main's lexical-reference cut (gunbc#12947) deleted it,
+// recording each binder's use in ResolvedTree.lexical_bindings instead -- with no declared type for a
+// pattern binder. So today the binder's use is underived, the arm body that projects off it is accepted at
+// the frontier with infer_match_arm_body_type_underived at its own locus, and the match is untyped.
+//
+// WHY StructurallyGuaranteed -> Mitigatable. Before, a field read off a match-arm binder that its variant
+// does not declare was refused by the compiler from the modeled payload. Now it is not judged at all: the
+// arm body is reported underived, typed and located, and nothing is fabricated -- the loud side of the
+// ladder, below the rung it held.
+//
+// THE TRIGGER NAMES THE CAPABILITY, and the population rows below are its executing evidence: each asserts
+// today's state EXACTLY (the binder's use underived, and in the match_binder rows the reason symbol at the
+// binder projection's locus), so an unrelated refusal reds it rather than greening it, and each flips back to its
+// #12641 assertion when the capability lands.
+data match_arm_binder_typing_lost_to_lexical_carrier: RungDrop = RungDrop {
+  identity: "match_arm_binder_typing_lost_to_lexical_carrier" as NonEmptyStr,
+
+  subject: "match-arm binder typing (gunbc#12641): a binder bound by a coproduct arm pattern is typed as its variant field's type at the scrutinee's instantiation, so projections off it are judged",
+
+  declared: "2026-10-02",
+
+  standing: Standing,
+
+  declaration: TypedDeclaration {
+    previous: StructurallyGuaranteed,
+    temporary: Mitigatable,
+    reason: DeletedWithoutReplacement,
+    population: [
+      "gunbc#12641 subject: v2.compiler.infer typing of match-arm binders through the scope search's arm-binder arms",
+      "v2.test.claim.match_binder.match_binder_typing mbt_binder_is_not_yet_typed_and_its_arm_body_is_reported_holds",
+      "v2.test.claim.match_binder.match_binder_typing mbt_match_is_not_yet_typed_at_the_binder_arm_holds",
+      "v2.test.claim.match_binder.match_binder_typing mbt_an_underived_arm_body_is_a_counted_frontier_holds",
+      "v2.test.claim.field_projection.field_projection_stages fps_a_match_binder_receiver_is_not_yet_typed_holds",
+      "v2.test.claim.field_projection.field_projection_stages fps_a_match_binder_projection_is_in_the_resolved_tree_holds",
+    ],
+    restoration_trigger: "match-arm binder typing through the lexical-binding carrier (N7-3): v2.compiler.resolve records a pattern binder's binding with the variant field it binds, and v2.compiler.infer types the binder's use from that binding at the scrutinee's instantiation, SUFFICIENT FOR mbt_binder_is_not_yet_typed_and_its_arm_body_is_reported to flip to the binder's use typed ParseArtifact, mbt_match_is_not_yet_typed_at_the_binder_arm to the match typed ParseTree, and a field off a match-arm binder its variant does not declare to refuse. Observed at retirement: those rows are flipped in the same change and pass on the required floor."
+  }
+}

dag/gunbc/rung_drop/roster.dag

@@ -121,6 +121,7 @@ import gunbc.rung_drop.typed_statement_let_refuses_until_the_bind_annotation_car
 import gunbc.rung_drop.python_to_typescript_compile_inhabitance_off_the_required_gate { python_to_typescript_compile_inhabitance_off_the_required_gate }
 import gunbc.rung_drop.edited_bin_witness_wet_rows_not_executed_by_ci { edited_bin_witness_wet_rows_not_executed_by_ci }
 import gunbc.rung_drop.shared_index_residency_asserted_after_the_run { shared_index_residency_asserted_after_the_run }
+import gunbc.rung_drop.match_arm_binder_typing_lost_to_lexical_carrier { match_arm_binder_typing_lost_to_lexical_carrier }
 
 data rung_drop_roster: List<RungDrop> = [
   floor_cut_heal,
@@ -225,6 +226,7 @@ data rung_drop_roster: List<RungDrop> = [
   shared_index_residency_asserted_after_the_run,
   dag_emit_round_trip_new_witness_eval_step_cost,
   dag_emit_real_grammar_round_trips_off_floor,
+  match_arm_binder_typing_lost_to_lexical_carrier,
 ]
 
 // THE DERIVATION THE PROJECTION USES, so "standing today" has one authority and not two. The