Roster membership skips declared-order metadata: five childless-Conj #12860 reds, bisected to #12625

[gunbai-bot]

Five silent v2.test.* reds from the #12860 amendment, plus eager-newt-412's codomain row, had one cause. A bare synthetic childless Conj was a member of the closed-ingest-set inhabitants roster. Infer therefore derived it a grounding by lookup, an ungrounded algebra ref, where it should have left it GroundingNotDerived.

Decided by execution, not by reading. Each claim's tree is a single node, so infer's facts map holds one entry and no facts-key collision is possible. A direct probe showed infer_node_declared_in_language_inhabitants(childless Conj) returning Present.

Bisected (BuildBuddy, product_introduction_leaves_childless_conj_on_the_frontier_holds, 339be73..c29acd0): the first bad commit is feadae7, #12625 (Program P). It rebuilt dag_fixture_emitted_add_fn through anonymous_signature_arrow, which adds the declared-order edge. That edge's label list is a FreeMonoid ending in a synthetic childless Conj, and std.kind roster_kind_index entered every node reachable from the roster.

Repair at the earliest unjustified link (option A, decided by the lane manager): the roster index walked label metadata as if it were payload.

• v2.std.node arrow_signature_order_edge(parent, edge) is now the ONE classification of an Arrow's declared-order edge. Infer's gather fold (infer_arrow_signature_order_edge) and product evidence (infer_product_child_evidence_edges) delegate to it, and std.kind roster_member_nodes asks the same predicate. No second list of metadata labels exists.
• This is not a shape special case: nothing tests for "childless Conj".
• RFM roster_membership_by_structural_equality records the residual. Membership is still structural equality with a roster value. Its next-rung trigger is identity-keyed membership, the namespace-migration end-state that v2.compiler.infer names.

Claims (v2.test.execution.infer_product_introduction):

• red: a_bare_childless_conj_is_not_a_roster_member_holds
• red: the_declared_order_label_list_is_not_a_roster_member_holds
• control: the_roster_add_fn_is_still_a_roster_member_holds (a genuine member still derives its kind)
• control: the_add_fn_domain_through_a_payload_edge_is_a_roster_member_holds (a payload edge is still walked)

Also in this PR, a separate cause: type_param_binder_frame.tpb_undeclared_t_is_not_a_type_variable is stale against #12566 (bisected: green at its parent, red at it). #12566 deliberately counts an undeclared formal atom as UndecidableFormalUnresolved on the Accepted path. The claim is re-stated to assert that advisory, with a discriminating twin (tpb_declared_t_is_instantiated_not_judged_unresolved: a declared T is instantiated, with no advisory).

Executed green on this branch (BuildBuddy, gunbc run per claim): the four claims above; infer_self_grounding_wall.wall_conj_grounding_no_longer_returns_source_as_its_own_type; translate_underived_refusal.translate_refuses_underived_conj_holds; ingest_bridge.ingest_identity_coercion_refuses_source_absent_from_authored_roster; infer_product_introduction.product_introduction_leaves_childless_conj_on_the_frontier_holds; data_decl_lowering_grounding.childless_conj_in_codomain_stays_on_the_frontier_holds; data_decl_lowering_grounding.nullary_arrow_domain_is_typed_as_the_empty_product_holds (control); and both tpb claims.

#12860 amendment: the six identities above leave the list, and docs/design-rung-drops.md is regenerated. Two main reds found while doing this were missing from the list and are now counted under calm-hawk-793:

• ingest_identity_coercion_accepts_source_present_in_authored_roster: red since std.kind: declared-inhabitant roster members derive their kind, not the roster root #12290 (bisected), being worked separately.
• product_introduction_derives_fully_evidenced_products_holds: its census literal (4) is stale; to be re-stated per named Conj.

🤖 Generated with Claude Code

[gunbai-bot]

Addressed review 73716 in 49582c0. infer_arrow_signature_order_edge is deleted. The gather step and infer_product_child_evidence_edges now call v2.std.node arrow_signature_order_edge directly, and the explanatory comment stays at the gather step, naming that predicate. The single classification now has one name. Re-executed on BuildBuddy and green: a_bare_childless_conj_is_not_a_roster_member_holds, product_introduction_leaves_childless_conj_on_the_frontier_holds, nullary_arrow_domain_is_typed_as_the_empty_product_holds, and tpb_declared_t_is_instantiated_not_judged_unresolved.

— sent from calm-hawk-793