Seed floor: collection vs nominal product is judged as a relation, not a property of one side

dag/gunbc/recurring_failure_mode/a_census_is_cited_wider_than_the_closure_its_instrument_compiles.dag

@@ -0,0 +1,28 @@
+module gunbc.recurring_failure_mode.a_census_is_cited_wider_than_the_closure_its_instrument_compiles
+
+import std.types { NonEmptyStr }
+import gunbc.recurring_failure_mode { RecurringFailureMode }
+
+data a_census_is_cited_wider_than_the_closure_its_instrument_compiles: RecurringFailureMode = RecurringFailureMode {
+  identity: "a_census_is_cited_wider_than_the_closure_its_instrument_compiles" as NonEmptyStr,
+
+  receipts: [
+    "**a census is reported at corpus grain when its instrument only ever compiled one closure, so a count that is exactly right for what ran is cited as a fact about the whole tree.** The measurement is not wrong and the instrument is not broken; the SCOPE SENTENCE around the number is wider than the population that produced it. INVALID STATE: a phrase of the form `N across the whole tree` standing on a run whose instrument reaches a proper subset of the tree, with nothing in the report naming the subset.",
+
+    "DISTINGUISHING IT FROM ITS TWO NEAREST NEIGHBOURS, both of which are about a DIFFERENT defect in the observation itself. `empty_observation_narrow` is an observation that could not express what changed being rendered as a verdict -- an absent reading treated as an answer. This row's reading is PRESENT, specific and correct; only its stated reach is inflated. `doctrine_safety_claim_stated_wider_than_the_census_that_delivers_it` is a normative sentence in the design authority outrunning a ruling's declared subset -- the claim lives in doctrine and the gap is authored. Here the claim lives in a PR body or a status message, the gap is incidental, and the author is usually the same person who ran the instrument correctly.",
+
+    "MEASURED SPECIMEN, 2026-09-22, gunbc#12045, and the author caught it on himself rather than a reviewer catching it. A new declared-type inhabitance wall was censused by the required floor lane and reported as `exactly one new refusal across the whole tree`, with that phrase carried into the PR body as the headline evidence that the wall was correctly scoped. It was true of the floor's closure. It was not true of the corpus: merging main and running `claim_executor --required-regen` surfaced a SECOND refusal, in `v1.compiler.emit_rust`, because the regen round runs a v2 SELF-COMPILE phase whose closure the floor lane never reaches. Two populations, one of them reported as the tree.",
+
+    "WHY IT SURVIVED THE OBVIOUS CHECK, which is the transferable part: the second refusal could not appear until the wall was IN THE BUILT BINARY, because the self-compile phase runs the built compiler over the seed's own sources. Every earlier regen on that branch ran an instrument built before the wall landed in its mirror, so the phase that would have refused was executing a compiler that could not refuse. The census was therefore honest at every point it was taken and became incomplete only once the instrument caught up -- which is the same instrument-vintage hazard that governs any `gunbc` measurement, arriving through a phase boundary rather than through a stale binary on PATH.",
+
+    "HARM. A scope sentence is what a reader carries forward. `one new refusal, and it is a real defect` reads as a closed census and invites the reviewer's next question to be about that one site rather than about the boundary; the second site then surfaces at merge time, when the cost of discovering it is highest. It also corrupts the ratio that made the change look correctly scoped: one false-positive-free refusal across a corpus is strong evidence a wall is well aimed, and the same number across a subset is not the same evidence.",
+
+    "RUNG FOUND AT: mitigatable -- the number is recoverable and the fix is a sentence. CEILING: mechanically preventable, not structural. The populations are modeled facts, so an instrument can print the closure it compiled beside its count, and a report that names the instrument (DESIGN section 6: name the instrument, never transcribe its output) inherits that scope automatically. It cannot be made structurally impossible, because the inflation happens in PROSE that no Accepted program reads (section 4c).",
+
+    "NEXT-RUNG TRIGGER, NAMED AS A CAPABILITY: every census-producing instrument states the closure it compiled as part of its own output, so a citation that names the instrument carries the scope with it and a reader cannot silently widen it. Sufficient for making `across the whole tree` either true by construction or absent. NOT satisfied by an author remembering to qualify a sentence, which is what failed here.",
+
+    "NOT CLAIMED HERE: how many other phases have closures the required floor does not reach. The self-compile phase is the one this specimen found by execution; the regen round has several phases and nothing enumerated their closures against the floor's. That enumeration is the honest next measurement and would tell any lane citing the floor as `the tree` exactly what it is citing.",
+  ],
+
+  evidence: [],
+}

dag/gunbc/recurring_failure_mode/declared_type_wall_keyed_on_the_value_being_a_kernel.dag

@@ -17,6 +17,12 @@ data declared_type_wall_keyed_on_the_value_being_a_kernel: RecurringFailureMode
 
     "MEASURED SPECIMEN TWO (2026-09-10, gunbc#10952, found by review 63271): `data bmc_rotation_route_disposition: Disposition = SingleAuthority`, where `SingleAuthority` is an arm of `ConstructionMechanism` and `Disposition` declares only `Terminal` and `Scaffold`. It rode FOUR GREEN REQUIRED CHECKS. Two independent observations that it compiled rather than being skipped: a `gunbc run` over that closure resolved it and failed only on a wrong function name, and the pull request was green on all four required checks with the row present.",
 
+    "MEASURED SPECIMEN THREE (2026-09-22, main ff2110b7e24, `quiet-ibex-229` from a `neat-boar-16` measurement, discovered by `loyal-swift-608` while demoting `lively-bat-737`'s construction wall): A COLLECTION AND A NOMINAL PRODUCT WERE MUTUALLY ADMITTED AT A DECLARED POSITION, IN BOTH DIRECTIONS. THE SIX-CELL GRID, each cell one `gunbc run --source-root dag --source-root src/v2 --source-root <probe> --entry <probe>.dag --function probe` over a one-module fixture. ADMITTED, body ran and returned: `type Rec { a: String }` with `fn takes_rec(r: Rec)` given `fn a_list() -> List<String>`; and the dual, `fn takes_list(xs: List<Int>)` given `fn a_rec() -> Rec`. REFUSED, so the direct-call seam demonstrably runs on these fixtures: `Int <- String`, `Int <- List<Int>`, `Rec <- Other` (a second record), `Rec <- Optional<Int>`. The two admissions are therefore a hole in the relation, not an unreached position.",
+
+    "THE CHAIN FOR SPECIMEN THREE, re-derived per DESIGN section 6b rather than patched at the symptom. `v1.compiler.infer` `declared_type_inhabitance`, declared=`Rec`, produced=`List<String>`: the optional arm does not fire; declared is not generic; both names resolve; `declared_realizes_as_kernel_numeric` no; `collection_at_scalar_declared_type` REFUSES ONLY WHEN THE DECLARED BASE PEELS TO A KERNEL SCALAR and `Rec` does not, so false; `record_at_scalar_needs_identity` wants a kernel declared, no; `coproduct_at_record_declared_type` wants a coproduct produced, no; `refinement_inhabitance` Absent; `kernel_value_declared_type_mismatch` false because the actual is not a kernel -- THE EXACT GUARD THIS ROW NAMES; `coproduct_payload_where_parent_required` no; `nominal_product_inhabitance_refusal` asks `nominal_product_head_name(produced)`, which answers the empty string for a collection BY DESIGN, so none. The relation then reaches its TERMINAL ARM, `Inhabits`, BY FALLTHROUGH. The dual falls through the same way with the roles swapped. THE EARLIEST UNJUSTIFIED BOUNDARY is that the relation's terminal arm is ACCEPTANCE while no arm ever judged collection-versus-nominal-product disjointness: every arm keys on the kind of ONE side, which is this row's recognition rule seen in a second vocabulary -- `is_kernel_type` on the actual is one instance of it and `node_is_collection` on the produced is another.",
+
+    "WHAT SPECIMEN THREE'S REPAIR IS, AND WHAT IT IS NOT. gunbc#12045 replaces `collection_at_scalar_declared_type` with `collection_versus_established_identity`, a RELATION BETWEEN THE TWO SIDES: exactly one side is an element or keyed collection after `peel_nominal_alias_identity` on BOTH sides, and the other side is an ESTABLISHED non-generic identity -- kernel scalar, nominal product or coproduct by `expected_type_head_exposure`. It is a replacement rather than a sibling arm precisely because a second relation keyed on products is the fork this row exists to prevent. THAT IS STILL NOT THIS ROW'S NEXT-RUNG TRIGGER. The trigger names ONE JUDGMENT FROM THE FORMAL'S DECLARATION FOR AN ACTUAL OF ANY KIND, sufficient for removing the offending-value guards entirely; the repair removes one such guard and leaves `kernel_value_declared_type_mismatch` and the head-name arms standing. The row stays open, and a future change may retire it only by landing exactly the trigger.",
+
     "HARM, AND IT IS THE SECOND SPECIMEN THAT SHOWS THE SHAPE. The review that found it concluded `the module therefore does not compile, and with it the whole witness closure` -- reasonable, and false. So the defect does not merely admit a wrong value: it makes a reader who assumes the floor holds derive a WRONG CONSEQUENCE from a correct observation. The author had four green checks saying the row was fine and a reviewer saying the module was absent, and neither was true.",
 
     "DISTINGUISHING FACTS: this is NOT the evidence-overreach family (a receipt supporting more than its instrument established) -- nothing here is a receipt, and the claim is not about coverage. It is NOT `check_subject_shape_cannot_represent_the_state_the_check_detects` -- the relation can represent the state perfectly; it declines to look. The tell is a wall whose guard names a property of the OFFENDING VALUE (`is_kernel_type`) where the property under test is a RELATION between the value and its declared type.",

dag/gunbc/recurring_failure_mode/meaning_fork.dag

@@ -29,6 +29,7 @@ data meaning_fork: RecurringFailureMode = RecurringFailureMode {
     "Second specimen of the consumer-varying form (the EffectPlan bash If/Let/Call climb for gunbc-private#60): `v2.std.orchestration::Predicate` carries `StrEq { lhs: String, rhs: String }` and siblings, and `v2.compiler.05_emit_orchestration` reads an operand as a RAW SHELL SPELLING (its authors write `lhs: \"\\\"$X\\\"\"`), while `v2.workflow.effect_plan_bash_materialize` reads the same field as a VALUE and single-quotes it. Hold the input constant and the two consumers disagree on whether `$X` expands. The silent arm was the value reading applied to a spelling-trained author: `[ '\"$X\"' = ... ]` compares four literal characters and never errors. Disposition taken: the value-reading consumer refuses any operand carrying a POSIX quoting or expansion character (`PredicateOperandCarriesShellSpelling`), so the fork surfaces as a typed refusal in the one consumer where it would otherwise be silent; the raw-spelling consumer is unchanged. Rung: MITIGATABLE by that refusal; ceiling STRUCTURALLY IMPOSSIBLE once Predicate operands are `Expr` (`ExprLit | ExprVarRef | ExprCmdSubst`), which already exists beside them in the same module -- a variable reference then has a typed arm and a literal is unambiguous, and the refusal and the fork delete together. That Expr migration is the next trigger; it is also what gunbc-private#60's pin check (`Let` a captured revision, `If` on it) needs to be authorable, so the trigger has a demanding consumer.",
 
     "A NEAR MISS THAT THIS ROW DELIBERATELY EXCLUDES, recorded because it was proposed as an instance and the row's own rule refuses it: the word `fabric` names both compute fabric (`gunbc.fabric_control_plane` and siblings) and network interconnect (`gunbc.spark.fabric_rail_apply`, `fabric_switch_observed`, `fabric_reach`). That is one spelling in two explicitly distinct module scopes, which the scoping carve-out above names as legitimate reuse, not a fork. What is real there is the specimen above -- a TYPE crossing the boundary -- not the adjective sitting on both sides of it.)",
+    "Third specimen, the hidden-state form at the SEED'S BUILTIN SURFACE (gunbc#12045): `with` is two contracts under one spelling. `v1.compiler.infer_method::builtin_function_registry` declares it as the MAP insert (`m, key, value` returning a Map), while the corpus also writes the RECORD UPDATE `with(base, { field: value })`, which returns the base's product type. Hold the spelling constant and vary the receiver, and the result type changes, so the name has forked. It stayed silent because every consumer just passed the Map-typed result along. The first consumer that had to decide was the generalized collection-versus-identity inhabitance relation, and it refused a Map at a product formal (`v1.compiler.emit_rust`'s `with(emit_info, { movable: ... })`): correct on a false premise. Disposition taken: `v1.compiler.infer::infer_tier2b_builtin_with_kernel_diags` picks the contract by the RECEIVER'S TYPE, not the arity. A keyed-collection receiver keeps the registry's Map answer, an established-product receiver returns the product, and anything else keeps the registry answer. So the fork is now distinguishable at type inference; it is not resolved. Rung: MITIGATABLE, since the spelling is still shared across the registry, `v1.compiler.languages` (the `bridge_method_overrides` entry mapping it to `with_update`), `v1.compiler.parse` and `v1.compiler.emit_rust`, and each special-cases it separately. Ceiling: STRUCTURALLY IMPOSSIBLE. This row does not yet decide between the two ways to get there: ONE polymorphic functional update over keyed structures (by key and by field), which is DESIGN section 2's horizontal move and dissolves the fork by unifying, or two distinct names, which is section 3's split. Next trigger: that decision, taken in v2 where the builtin surface is modeled rather than in the frozen seed, after which both arms of the receiver test and the per-stage special cases delete together. Controls: `test.claim.declared_type_inhabitance_direct_call_witness_test` `w_a_record_update_inhabits_its_bases_declared_type` (goes red when the receiver arm's product branch is disabled) and `w_a_genuine_map_at_a_product_formal_still_refuses`.",
   ],
 
   evidence: [
@@ -37,5 +38,7 @@ data meaning_fork: RecurringFailureMode = RecurringFailureMode {
     DeclarationRef { module_path: "gunbc.harness.harness_seat", decl_name: "harness_seat_partition", field: WholeDeclaration },
     DeclarationRef { module_path: "v2.std.orchestration", decl_name: "Predicate", field: WholeDeclaration },
     DeclarationRef { module_path: "v2.workflow.effect_plan_bash_materialize", decl_name: "effect_plan_bash_predicate_operand_shell_spelling_chars", field: WholeDeclaration },
+    DeclarationRef { module_path: "v1.compiler.infer_method", decl_name: "builtin_function_registry", field: WholeDeclaration },
+    DeclarationRef { module_path: "v1.compiler.infer", decl_name: "infer_tier2b_builtin_with_kernel_diags", field: WholeDeclaration },
   ],
 }