Accumulator-copy analyzer misses the fold/list_append specimen: gate_red_quadratic_rejects red on main (dark long-lane row)

dag/gunbc/explicit_witness_admission.dag

@@ -386,12 +386,36 @@ data explicit_witness_admissions: List<ExplicitWitnessAdmission> = [
     dissolution: unbound_dissolution(description: "the local wet receipt greens under gunbc_falsifier_self_host_wet_receipt_wall_budget; this row deletes and the green wet SelfHostWetReceiptBinding restores")
   ),
   known_red_probe(
-    entry: "src/v2/test/claim/long/accumulator_copy_compile_gate_test.dag",
-    f: "gate_red_quadratic_rejects",
+    entry: "src/v2/test/claim/long/accumulator_copy_fold_analysis_test.dag",
+    f: "let_alias_is_proven_suspect",
     kind: CorpusWitnessKind,
     budget: SubstrateLongLaneEvalBudget,
-    reason: "THE DISCRIMINATING RED OF A REQUIRED LENS, FAILING ON MAIN, FOUND ONLY BECAUSE gunbc#11073 RAN IT. gunbc.v2_compile_obligation_census accumulator_copy_obligation names this witness as its discriminating red and claims MechanicallyPreventable, but its home test/claim/long/ is a gunbc.ci_layer_roots witness_exclusion_frontier pattern, so no required run had ever planned it. Its first real execution failed on srv3-02 with no thrash. The failure is not a wrong reason and not an upstream refusal: measured with a three-way discriminator, the specimen normalizes and accumulator_copy_compile_gate ACCEPTS it, because v2.lens.complexity_accumulator_copy.analyze accumulator_copy_findings returns NO suspect for fold(xs, init: 0, f: fn(acc, x) { list_append(left: acc, right: x) }) -- the shape the lens exists to refuse. Verified latent rather than regressed: one binary, same functions, FAIL against origin/main and FAIL against the PR head, with both sibling controls PASS on both sides. The class is gunbc.recurring_failure_mode required_lens_red_control_never_executes_from_its_home, which also records that the census rung is asserted rather than established and is downgraded in the same change. Owner: the accumulator-copy analyzer lane." as NonEmptyStr,
-    dissolution: unbound_dissolution(description: "v2.lens.complexity_accumulator_copy.analyze accumulator_copy_findings returns a NON-EMPTY suspects list for the fold-append accumulator specimen, and accumulator_copy_compile_gate consequently refuses that tree with reason accumulator_copy_poly2_suspect. That fact is FALSE TODAY and was measured false by execution on both origin/main and this head, so the trigger cannot be satisfied by anything short of the analyzer change; it is deliberately NOT keyed on this witness greening, since editing the specimen or the control would green the witness without the capability. When the analyzer lands, this row deletes in that same change and the unchanged witness promotes to ordinary discovery as the permanent regression control per DESIGN 4b(4)")
+    reason: "THE SUBJECT NEVER REACHES THE LENS: THE FIXTURE IS REFUSED BY PARSE. Measured by staged probe on the exact let_alias_snippet bytes, tokenize ACCEPTS and v2.compiler.parse parse_module REJECTS, so normalize never runs, findings are Empty, and the witness's `Absent => false` reports a STAGE REFUSAL as though the lens returned no suspect. The refusal is shape-specific and was narrowed by a six-cell ingest matrix over the same harness rather than guessed: `let grown = acc` followed by the call REFUSES; the same body with the binder renamed to `g` REFUSES; `let grown = mystery` (an unbound name) PARSES; `let seed = 0` PARSES; the transitive form `let g = acc` then `let h = g` then the call PARSES; and the identical alias with the `let` on the fn-literal's own line PARSES. So it is neither the binder name nor the statement count nor the RHS being an identifier -- the refusing combination is a let whose RHS names the fn literal's bound parameter standing immediately before a call statement. THIS ROW IS NOT A CLAIM ABOUT THE LENS. Whether the analyzer would prove the alias suspect is UNKNOWN and unmeasurable while parse refuses the specimen, and the sibling let_transitive_alias_is_proven_suspect -- which does parse -- PASSES, so the aliasing closure itself is exercised and green at the two-binding grain. THE ROW EXISTS BECAUSE THE WITNESS ONLY BECAME VISIBLE NOW: the whole module was dark on main with a NormalizedTree/.root type drift that this same PR repairs, so all 21 of its witnesses were unexecuted, and this red is pre-existing and unmasked rather than introduced -- established on a control worktree carrying ONLY the .root repair with the lens change absent, where it fails identically. Owner: the .dag grammar lane, not the complexity lens lane.",
+    dissolution: unbound_dissolution(description: "v2.compiler.parse parse_module ACCEPTS a fn-literal body whose let binds the literal's own parameter and is followed directly by a call statement, sufficient for the let_alias_snippet bytes to reach normalize -- the capability is the grammar admitting that statement shape, NOT any artifact contributing to it: a new fixture spelling, a reworded snippet, or a diagnostic variant retires nothing, because rewriting the fixture to a shape that already parses would delete the only executing evidence that this shape does not. When parse admits it, this witness reaches the lens and either greens or reds on a LENS fact for the first time; this row deletes in that same change and the assertion becomes an ordinary permanent regression control for the single-binding alias case")
+  ),
+  known_red_probe(
+    entry: "src/v2/test/claim/long/accumulator_copy_fold_analysis_test.dag",
+    f: "let_fresh_binding_is_provably_clean",
+    kind: CorpusWitnessKind,
+    budget: SubstrateLongLaneEvalBudget,
+    reason: "A FALSE REFUSAL, WHICH FAILS CLOSED AND CONTAINS THE HARM, WHICH IS WHY IT IS A ROW RATHER THAN A FIX HERE. This fixture DOES ingest -- measured, unlike its let_alias sibling -- and the analyzer returns exactly one finding, ^copied_port_computed_argument, where the witness asserts zero. So a provably fresh binding (`let seed = 0`, a pure literal RHS, then list_append(left: seed, right: x)) is reported as undecidable residue instead of clean. The direction matters for the ladder: the lens over-refuses rather than under-refuses, so no copied accumulator is admitted by this defect and the compile gate cannot be made to ACCEPT a quadratic through it -- ^copied_port_computed_argument rides the Accepted diagnostics channel, counted and non-gating, so the cost is a noisy ledger and a stopped-line audit entry, not a silent pass. Attribution is measured on both sides: it fails identically on a control worktree carrying ONLY the NormalizedTree/.root repair with this PR's port_reading change absent, so it is pre-existing and unmasked by un-darkening the module, not introduced by the named-argument fix. The adjacent sibling let_fresh's BindsFresh path is declared in v2.lens.complexity_accumulator_copy resolve_port_reading, so the suspicion is that the let-spine resolution does not reach this binder rather than that BindsFresh is wrong, but that is a HYPOTHESIS and is deliberately not asserted here. Owner: the complexity lens lane.",
+    dissolution: unbound_dissolution(description: "v2.lens.complexity_accumulator_copy.analyze distinguishes a provably fresh let-binding from an unresolved alias at the copied port, so a binder whose RHS is a pure literal resolves to PortPureLiteral through resolve_port_reading and the specimen yields NO finding at all -- the capability is the analyzer deciding freshness for the single-binding let spine, not the mere existence of the BindsFresh constructor, which is already declared and already reachable for other shapes and therefore retires nothing. When it lands this assertion greens with no edit to the witness and this row deletes in the same change")
+  ),
+  known_red_probe(
+    entry: "src/v2/test/claim/long/accumulator_copy_fold_analysis_test.dag",
+    f: "named_step_fold_refuses_accumulator_unread",
+    kind: CorpusWitnessKind,
+    budget: SubstrateLongLaneEvalBudget,
+    reason: "A SILENT FAIL-OPEN (DESIGN section 5), AND THE MOST SERIOUS THING THIS LANE FOUND: the lens does not see the fold at all, rather than refusing it. For `fold(xs, init: 0, f: step)` -- a fold whose step is passed BY NAME rather than as an fn literal -- the normalized tree measured by probe contains NO lowered Loop and NO surface fold call, and v2.lens.complexity_accumulator_copy.analyze count_fold_sites returns 0. The witness asserts the honest arm, ^fold_accumulator_unread, which v2.lens.complexity_accumulator_copy.analyze fold_family_carrier mints when the seam refuses to yield a carrier; that refusal is never reached because the traversal never recognises a fold site to refuse ABOUT. This is the failure arm widening into silence rather than refusing: a fold the source declares is absent from the lens's domain, so its accumulator is neither proven, nor refused, nor counted -- and unlike the named-argument defect this same PR repairs, nothing in the ledger records that a subject was skipped. The class is filed at gunbc.recurring_failure_mode.fold_shape_visible_to_no_lens. Attribution is measured: identical failure on a control worktree carrying ONLY the NormalizedTree/.root repair with this PR's lens change absent, so pre-existing and unmasked rather than introduced. NOT FIXED HERE ON A DELIBERATE RULING (eager-raven-113): the repair is plausibly in v2.compiler.fold_lowering or v2.compiler.body_lowering_fold rather than in the lens, and is therefore unbounded inside a PR whose subject is the port reading. Owner: dispatched from the recurring-failure-mode row.",
+    dissolution: unbound_dissolution(description: "v2.lens.complexity_accumulator_copy.analyze OBSERVES every fold the source declares, at every lowering shape a fold-family call can take -- including a step passed by name, which today lowers to neither a Loop nor a surviving surface fold call -- so count_fold_sites counts the site and the carrier-unread case reaches its ^fold_accumulator_unread refusal instead of vanishing. The capability is totality of the lens's fold domain over declared fold shapes; a diagnostic variant, a roster row, or a lowering that merely reports the shape retires nothing unless the site becomes VISIBLE to the traversal. When it lands this assertion and its report_counters sibling green with no edit and both rows delete in the same change")
+  ),
+  known_red_probe(
+    entry: "src/v2/test/claim/long/accumulator_copy_fold_analysis_test.dag",
+    f: "report_counters_state_the_domain",
+    kind: CorpusWitnessKind,
+    budget: SubstrateLongLaneEvalBudget,
+    reason: "THE SAME DEFECT AS ITS named_step_fold_refuses_accumulator_unread SIBLING, MEASURED AT THE COUNTER GRAIN, and rostered separately because it is a separate executing assertion rather than because it is a separate fact. The witness asserts the lens's domain census over two specimens: folds_seen 1 and carriers_bound 1 for the fold/list_append quadratic, and folds_seen 1 with carriers_bound 0 for the named-step fold. The first conjunct holds -- measured directly, count_fold_sites over the quadratic is non-zero in both the bound and unbound readings. The second does not: for `fold(xs, init: 0, f: step)` count_fold_sites returns 0, not 1, because the site is invisible to the traversal rather than seen-and-unbound. That is exactly the distinction the counters exist to publish -- a fold whose carrier could not be read is supposed to be COUNTED and unbound, and a fold that is not counted at all is the lens silently narrowing its own domain -- so this witness is the instrument that would have caught the fail-open had it ever executed. It never did: the module was dark on main with the NormalizedTree/.root drift this PR repairs. Attribution measured on a control worktree carrying ONLY that repair: identical failure with this PR's lens change absent. Class: gunbc.recurring_failure_mode.fold_shape_visible_to_no_lens.",
+    dissolution: unbound_dissolution(description: "the same capability its sibling row names -- v2.lens.complexity_accumulator_copy.analyze observes every fold the source declares at every lowering shape, so a named-step fold is counted by count_fold_sites with carriers_bound 0 rather than being absent from the census. This row deletes together with the named_step_fold_refuses_accumulator_unread row when that lands; neither retires on a counter being renamed, a specimen being changed, or the assertion being split")
   ),
   known_red_probe(
     entry: "src/v2/test/claim/long/production_qualification_origin_probe_witness_test.dag",

dag/gunbc/recurring_failure_mode/fold_shape_visible_to_no_lens.dag

@@ -0,0 +1,18 @@
+module gunbc.recurring_failure_mode.fold_shape_visible_to_no_lens
+
+import std.types { NonEmptyStr }
+import gunbc.recurring_failure_mode { RecurringFailureMode }
+
+data fold_shape_visible_to_no_lens: RecurringFailureMode = RecurringFailureMode {
+  identity: "fold_shape_visible_to_no_lens" as NonEmptyStr,
+
+  receipts: [
+    "a fold shape that lowers to NEITHER a substrate Loop NOR a surviving surface fold call, so no lens can see it: the site is absent from the analyzer's domain rather than refused inside it, and the accumulator it carries is neither proven, nor refused, nor counted (DESIGN section 5 -- a failure arm must refuse, never widen; here it widens into silence)",
+    "SPECIMEN AND INSTRUMENT, 2026-09-12. `fold(xs, init: 0, f: step)` -- a fold-family call whose step is passed BY NAME rather than as an fn literal. Ingested through tokenize / parse_module / normalize, the normalized tree contains no ComputationNode Loop and no surface fold call, and `v2.lens.complexity_accumulator_copy.analyze` `count_fold_sites` returns 0 in both the bound and unbound readings. The instrument is the fixture itself: `named_step_snippet` in `src/v2/test/claim/long/accumulator_copy_fold_analysis_test.dag`, whose two witnesses `named_step_fold_refuses_accumulator_unread` and `report_counters_state_the_domain` are the executing evidence and are rostered red at `gunbc.explicit_witness_admission`.",
+    "WHAT MAKES IT THIS CLASS RATHER THAN A MISSING FEATURE: the lens ALREADY CARRIES the honest arm for this exact situation and it is unreachable. `v2.lens.complexity_accumulator_copy.analyze` `fold_family_carrier` mints ^fold_accumulator_unread precisely when the seam refuses to yield a carrier -- the named-step case is named in its own carrier note as a Stage B callee-resolution fact -- but the refusal is never reached, because the traversal never recognises a site to refuse ABOUT. So the corpus contains a written, correct, located refusal that no input can trigger, which reads to every reader as coverage. The tell is a domain counter that reports 0 where the source visibly declares 1, and it is only detectable if the counter is asserted SEPARATELY from the verdict.",
+    "WHY IT SURVIVED, and it is a property of the evidence rather than of the defect. Both witnesses live in a module that was DARK: `ingest` passed the sealed NormalizedTree carrier where a Node is wanted (missing `.root`, dead since the BL-1 seal), so all 21 witnesses of that file failed at the type level and none of them ever evaluated its subject. The fail-open and the instrument that would have caught it were disabled by the same unrelated defect, which is why un-darkening a module is a discovery operation and not a formality: 17 of those 21 came back green, and the 4 that came back red were pre-existing -- established on a control worktree carrying only the `.root` repair.",
+    "THE RUNG, stated with its ceiling because a fold the lens cannot see is BELOW the floor rather than low on it: found at below-the-floor, since the complexity lens is a required root gate at the compile door and a subject invisible to it is admitted in silence regardless of how the gate is enrolled. The ceiling is STRUCTURALLY GUARANTEED, and it is reachable: fold-family lowering is a closed, decidable set of declared shapes, so a lowering total over that set makes the invisible site unwritable rather than merely detected. NEXT-RUNG TRIGGER, named as a capability: every fold-family call the source declares lowers to a shape the lens's traversal enumerates -- suspected home `v2.compiler.fold_lowering` or `v2.compiler.body_lowering_fold` rather than the lens, which is why the repair is dispatched as its own item and was deliberately NOT attempted inside the port-reading fix that found it. A diagnostic variant, a roster row, or a lowering that merely reports the shape retires nothing unless the site becomes visible to the traversal.",
+  ],
+
+  evidence: [],
+}

dag/gunbc/recurring_failure_mode/lowering_accessor_collapses_a_sequence_operand.dag

@@ -0,0 +1,18 @@
+module gunbc.recurring_failure_mode.lowering_accessor_collapses_a_sequence_operand
+
+import std.types { NonEmptyStr }
+import gunbc.recurring_failure_mode { RecurringFailureMode }
+
+data lowering_accessor_collapses_a_sequence_operand: RecurringFailureMode = RecurringFailureMode {
+  identity: "lowering_accessor_collapses_a_sequence_operand" as NonEmptyStr,
+
+  receipts: [
+    "a lowering accessor that silently narrows a MULTI-ELEMENT operand to its first element: the caller asks what an argument is and receives a proper part of it, with no refusal and nothing counted, so every consumer downstream reasons about a subset of the program the source actually wrote (DESIGN section 5 -- a failure arm must refuse, never widen)",
+    "SPECIMEN AND SYMBOL, 2026-09-12. `v2.compiler.body_lowering_fold` `body_lower_operand_ref_optional`, reached from `body_lower_named_arg_value_optional` via `body_lower_arg_operand_optional`: on a node that is a sugar sequence pair it recurses into `pair.left` ALONE. For the argument `left: seed + acc` it returns the operand for `seed` and drops `acc` entirely. The narrowing is unconditional and unreported -- no diagnostic, no counter, no typed arm distinguishing `this is the whole operand` from `this is the first of several`.",
+    "HOW IT SURFACED, WHICH IS THE PART WORTH KEEPING: not in the compiler, but in a CONSUMER that happened to need the whole answer. The accumulator-copy lens censuses the identifiers an argument mentions. Its first repair reached the same shape by a different route (a first-match DFS for the argument's first `^dag_surface_primary_expr`) and inherited the identical narrowing, which review 64393 caught: `left: seed + acc` censused as `[seed]`, one identifier, so a `BindsFresh` `seed` resolved the port to `PortPureLiteral` and a COPIED ACCUMULATOR CLASSIFIED CLEAN with the carrier invisible. Two independent implementations of `the argument's value` converged on the same wrong answer, which is the evidence that the defect is in the shared fact rather than in either caller.",
+    "WHY NO EXISTING WITNESS HELD IT, stated as a property of the corpus: every fixture in the accumulator-copy suite used a single-identifier or single-call argument, where narrowing to the first element and returning the whole operand agree. The class is only observable at arity two or more on one port, and nothing in the suite wrote that until the review asked for it. A collapse that is invisible on every fixture in the suite is not a tail case -- it is an unexercised axis.",
+    "RUNG FOUND AT: below the floor, because the loss is SILENT -- `values inhabit declared types` and `applications bind in exact bijection` are floor sentences, and an operand silently replaced by a proper part of itself is neither refused nor recorded. CEILING: structurally guaranteed, and reachable -- the operand carrier cannot be narrowed without a typed refusal once the accessor returns a shape that can represent a multi-element operand, at which point dropping an element has no constructor. NEXT-RUNG TRIGGER, NAMING THE CAPABILITY: `body_lower_named_arg_value_optional` preserves the full sequence an argument names, so a caller asking for an argument's value receives all of it or a located refusal -- not its first element. A diagnostic variant, a counter, or a second accessor beside it retires nothing; the narrowing itself must become unwritable. When it lands, `v2.lens.complexity_accumulator_copy.analyze` `arg_value_node` dissolves into that accessor and its stated-divergence annotation deletes with it.",
+  ],
+
+  evidence: [],
+}