Refuse a product value at a kernel-scalar (or refined) declared type

dag/gunbc/recurring_failure_mode/product_value_at_a_scalar_formal_is_accepted.dag

@@ -20,13 +20,13 @@ data product_value_at_a_scalar_formal_is_accepted: RecurringFailureMode = Recurr
 
     "RUNG FOUND AT: outside the ladder -- arm (1) silently wrong, arm (2) counted by a non-blocking advisory. CEILING: structurally guaranteed. Both identities are established in the modeled facts, a product never inhabits a kernel scalar or a refinement of one, and the invalid program is authorable in source, so impossibility is not available. NEXT-RUNG TRIGGER, named as the capability: the seed's declared-type inhabitance judges a product against a scalar formal from the existing resolved type-head exposure at every declared-type position -- record_at_scalar_needs_identity re-derived to refuse DeclaredTypeNotInhabited when that exposure establishes a product against a kernel scalar, AND a refined declared type judged through its base carrier when the produced value is unrefined. No new identity producer is part of this capability. SUFFICIENT FOR: all three enrolled reds in test.claim.declared_type_product_at_kernel_scalar_formal_witness_test to refuse, the positive control and a refined value at its own base to stay accepted, and the whole-corpus census of newly refused sites to be dispositioned. A spelling check or a per-name exemption is not this capability. OWNER: none yet.",
 
-    "NOT FIXED HERE, and why: this PR files the class and enrolls its evidence. Each repair moves the seed's blocking population across the compiler-source corpus -- gunbc#9706 withdrew a blocking arm on exactly that census -- so it lands as a separate follow-up that carries its own corpus census, not inside the filing.",
+    "CLIMBED (gunbc#13391) to structurally guaranteed at the seed. v1.compiler.infer record_at_scalar_needs_identity, which declined with UndecidableProducedIdentityErased, is deleted; product_at_scalar_declared_type refuses RefusedProductAtScalar, a blocking DeclaredTypeNotInhabited. Both heads are read from expected_type_head_exposure, which is keyed on the declaring file plus name of the RESOLVED declaration, so the produced identity at the binding edge is the declaration identity gunbc#9706 found missing when that judgment read a bare head -- the FilePath homonym pair is two census keys, not one spelling. The refinement seam is closed by declared_head_is_kernel_scalar_through_refinement, which peels a where-refined declared type through where_refinement_chain to its base before asking for a kernel head. The same pair is handed to declared_type_obligation_diags from declared_type_conformance_diags_core, so the declared-return, let, data and record-field positions are judged by the one relation the direct-call argument uses. EVIDENCE: the three test.claim.declared_type_product_at_kernel_scalar_formal_witness_test reds and test.claim.sole_constructor_type_head_exposure_witness_test sealed_carrier_at_kernel_formal_refuses PASS and leave v2.workflow.floor_expected_red; they stay enrolled as permanent regression controls (DESIGN 4b(4)). The positive control (the record's EpochMs field at an EpochMs formal) and test.claim.declared_type_inhabitance_direct_call_witness_test w_a_branded_refinement_at_its_own_declared_base_inhabits stay green. RESIDUAL: a produced value that is itself a where-refinement of a product exposes OpaqueTypeHead and is not judged by this arm; that pair belongs to gunbc.recurring_failure_mode absence_classifier_default_bucket.",
   ],
 
   evidence: [
     DeclarationRef { module_path: "v1.compiler.infer", decl_name: "declared_type_inhabitance", field: WholeDeclaration },
     DeclarationRef { module_path: "v1.compiler.infer", decl_name: "refinement_inhabitance", field: WholeDeclaration },
-    DeclarationRef { module_path: "v1.compiler.infer", decl_name: "record_at_scalar_needs_identity", field: WholeDeclaration },
+    DeclarationRef { module_path: "v1.compiler.infer", decl_name: "product_at_scalar_declared_type", field: WholeDeclaration },
     DeclarationRef { module_path: "test.claim.declared_type_product_at_kernel_scalar_formal_witness_test", decl_name: "a_record_at_an_epoch_ms_argument_refuses", field: WholeDeclaration },
     DeclarationRef { module_path: "test.claim.declared_type_product_at_kernel_scalar_formal_witness_test", decl_name: "the_harness_refuses_an_int_at_a_bool_argument", field: WholeDeclaration },
   ],

dag/test/claim/declared_type_inhabitance_direct_call_witness_test.dag

@@ -119,9 +119,12 @@ test fn w_collection_disjointness_keeps_conforming_arguments_admitted() -> Bool
 
 data record_value_at_scalar_source: String = "module probe_inhabit_record_at_scalar\nimport std.types { Int, String }\ntype Box { value: String }\nfn make_box() -> Box { Box { value: \"forty\" } }\nfn takes_text(text: String) -> Int { 1 }\nfn probe() -> Int { takes_text(text: make_box()) }\n"
 
-test fn w_record_typed_value_at_scalar_argument_is_counted_until_identity_is_grounded() -> Bool {
-  violation_count(source: record_value_at_scalar_source, wanted: "DeclaredTypeInhabitanceUndecided") > 0
-    && violation_count(source: record_value_at_scalar_source, wanted: "DeclaredTypeNotInhabited") == 0
+// A record at a kernel scalar formal REFUSES: both heads are read from the identity-keyed type-head
+// census (v1.compiler.infer product_at_scalar_declared_type), so the judgment no longer declines as
+// UndecidableProducedIdentityErased. The undecided count is not asserted: the fixture's closure
+// carries unrelated list-element advisories from std.algebra.
+test fn w_record_typed_value_at_scalar_argument_is_refused() -> Bool {
+  violation_count(source: record_value_at_scalar_source, wanted: "DeclaredTypeNotInhabited") > 0
 }
 
 data coproduct_value_at_record_source: String = "module probe_inhabit_coproduct_at_record\nimport std.types { Int, String }\ntype Box { value: String }\ntype Choice = | ChoiceA { value: String } | ChoiceB\nfn make_choice() -> Choice { ChoiceA { value: \"forty\" } }\nfn takes_box(box: Box) -> Int { 1 }\nfn probe() -> Int { takes_box(box: make_choice()) }\n"

dag/test/claim/declared_type_product_at_kernel_scalar_formal_witness_test.dag

@@ -17,13 +17,13 @@ import std.types { String, Bool, Int }
 // EpochMs`) passed where `read_at_millis: EpochMs` is declared. std.types EpochMs is
 // `Int where range(min: 0)`.
 //
-// Two arms, measured separately because they fail differently. At the EpochMs formal and the EpochMs
-// declared return no arm of v1.compiler.infer declared_type_inhabitance judges the pair and it reaches
-// Inhabits by fallthrough, with no inhabitance diagnostic at all. At a plain Int formal
-// record_at_scalar_needs_identity answers UndecidableProducedIdentityErased, an advisory.
+// Two arms, measured separately because they failed differently before the repair. At the EpochMs
+// formal and the EpochMs declared return no arm of v1.compiler.infer declared_type_inhabitance judged
+// the pair and it reached Inhabits by fallthrough; at a plain Int formal the deleted
+// record_at_scalar_needs_identity answered UndecidableProducedIdentityErased, an advisory.
 //
-// The three RED claims assert the REQUIRED refusal and are carried in v2.workflow.floor_expected_red
-// while the seed accepts; when the wall lands they pass, the roster names them for removal, and they
+// The three RED claims assert the REQUIRED refusal. They were carried in v2.workflow.floor_expected_red
+// while the seed accepted; v1.compiler.infer product_at_scalar_declared_type (gunbc#13391) made them
 // stay here as permanent regression controls (DESIGN 4b(4)). The positive control keeps the wall from
 // over-refusing the record's own EpochMs field, and the harness control proves an Int at a Bool
 // argument refuses through this same census route, so a red here is the seam and not the harness.

dag/test/claim/sole_constructor_type_head_exposure_witness_test.dag

@@ -59,16 +59,11 @@ data sc_sealed_at_payload_red: String = "module probe_sc_sealed_at_payload_red\n
 // this one silent, and a one-direction wall would read as covering the class.
 data sc_payload_at_sealed_red: String = "module probe_sc_payload_at_sealed_red\ntype Inner { v: Int }\ntype Wrapped sole_constructor { root: Inner }\nfn takes_wrapped(x: Wrapped) -> Int { 0 }\nfn f(i: Inner) -> Int { takes_wrapped(x: i) }\n"
 
-// RED 3 -- a sealed carrier at a KERNEL formal, which this repair does NOT close. Measured on the
-// repaired compiler, in the same run that shows the two record positions above now refusing:
-// record_at_scalar_needs_identity reads the exposure this change repairs, so the head is now
-// visible and something ELSE declines the judgment at this position; what that is has not been
-// established and is not guessed at here. This probe asserts the REFUSAL the floor requires, not
-// the accepting answer the compiler gives today, and is therefore enrolled in
-// v2.workflow.floor_expected_red -- where it still executes and is still asserted, its failure
-// counts as agreement, and it REDS THE BUILD the moment it starts passing, naming itself for
-// removal. An earlier revision asserted `!sc_refuses_inhabitance` instead; that made the defective
-// answer required green behaviour, which DESIGN section 4b(4) forbids.
+// RED 3 -- a sealed carrier at a KERNEL formal. The head-exposure repair made the head visible
+// but the kernel position kept accepting: the judgment there declined for want of a produced
+// declaration identity. v1.compiler.infer product_at_scalar_declared_type (gunbc#13391) refuses it
+// from the identity-keyed head census, so this probe left v2.workflow.floor_expected_red and stays
+// as a permanent regression control (DESIGN section 4b(4)).
 data sc_sealed_at_kernel_red: String = "module probe_sc_sealed_at_kernel_red\ntype Inner { v: Int }\ntype Wrapped sole_constructor { root: Inner }\nfn takes_int(n: Int) -> Int { n }\nfn f(w: Wrapped) -> Int { takes_int(n: w) }\n"
 
 // THE NO-FORK CONTROL. Identical to RED 1 except the actual's declaration is not sealed. It