RFM: classify the three residual reds (single_arm_match regressed by #13056)

[gunbai-bot]

Fifth PR of the floor-unimported-bare-provider triage: the three residual reds, classified. RFM rows only; no code changes and no repairs.

witness module	on main	classification	where recorded
v2.test.claim.body_lowering.single_arm_match	4 of 6	v2 regression, bisected to #13056: 6 of 6 pass at 28ad904 and 6571276; two_arm_match_still_accepts_holds and three_arm_match_keeps_every_arm_holds fail from fd30a50. The two-arm source parses and normalizes Accepted; conserved_normalize rejects on a dropped atom reference.	receipt appended to match_arms_after_the_second_are_dropped_at_v2_body_lowering, whose 4b(4) evidence is now red
v2.test.long.cwc_resolution_probe	7 of 9	the malformed-coproduct pair is a claim and its own negation (stale expectation shape); cwc_cwc_module_resolve_accepts is a regression candidate (lve_anonymous_record_expected_type_not_record), not bisected	new row anonymous_record_literal_refused_against_a_declared_record_type
v2.test.long.accumulator_copy_fold_analysis	5 of 24	lost supported classification: the Loop is still found, but no Poly2Suspect appears on the positives, and the lens likely refuses (Unclassifiable) rather than answering clean. The 19 failures are a mixed population; not bisected	new row accumulator_copy_lens_binds_no_carrier

Masked failure: the single_arm_match identities sit in a CENSORED floor_cost_debt chunk, which asserts no verdict. Proposal: an observed semantic FAIL must not stay represented only as a cost/censored row. A check at admission and restoration is snapshot-limited, so it supplements the existing execution obligation rather than replacing it.

Instrument: claim_batch over every test fn, run on BuildBuddy with GUNBC_MEMORY_BUDGET_BYTES forwarded. The diagnostic reasons came from temporary probe claims, which are not in this diff.

🤖 Generated with Claude Code

[briansrls]

REQUEST_CHANGES at exact head 01234d88492b4eff7c7e1c042b98fbcafe315b4f, against DESIGN.md §§3, 4b(1)/(3), 5 and 6b. These are corrections to the RFM classification and proposed restoration conditions, NOT a request to move the separately dispatched compiler/lens repairs into this PR.

The reported single_arm_match bisect is useful and the CWC contradictory pair is present in source: the two claims return P and !P for the identical input. Keeping the CWC resolve cause unbisected and the comma-versus-newline discriminator unestablished is appropriate. Two load-bearing statements in the new rows do not match their owning interfaces.

1. accumulator_copy_lens_binds_no_carrier conflates 'no Poly2Suspect' with 'clean/no finding', and its restoration trigger can already be satisfied by the broken path.

At this exact head, v2.lens.complexity_accumulator_copy.analyze::analyze_lowered_loop handles an absent carrier by emitting:

Unclassifiable { at: node, cause: ^fold_accumulator_unread }

The surface-fold absent-carrier branch in analyze does likewise. accumulator_copy_report retains the findings, and finding_is_suspect deliberately returns false for Unclassifiable while finding_is_refusal returns true. Consequently a failed has-suspect assertion does NOT establish that the lens answered clean. The row's sentence 'A lens that cannot bind answers clean' and silent-wrongness classification need either correction to a loss of supported classification with a refusal, or an identified downstream consumer that actually discards that refusal. Do not assign that latter defect to the lens without the consumer evidence.

The same row says every clean control passes, but its own five-pass roster excludes let_fresh_binding_is_provably_clean, an existing clean-control test in the named module. Preserve the actual mixed population rather than using the blanket claim to infer one mechanism for all 19 failures. report_counters_state_the_domain is also a conjunction over two different snippets, not a standalone observation that carriers_bound is zero.

Most importantly, 'binds the carrier ... OR refuses that Loop by name' is not a sufficient restoration trigger for the lost positive classification: the current absent-carrier branch already refuses that Loop by name. Require restoration of binding and discriminating classification for the supported inline-fold positives, while retaining the distinct clean and unsupported/refused controls. Narrow unresolved causal claims rather than requiring a bisect to land this record.

2. The cost-row recommendation reintroduces a meaning the debt authority expressly rejects.

v2.workflow.floor_cost_debt distinguishes PROVEN passing/over-cost evidence from CENSORED interruption before verdict. Its header explicitly records and retracts the former universal claim that every enrolled witness passes. This PR nevertheless states 'A cost row asserts the claim would pass given time.' That is false for the censored chunk implicated here.

The useful proposed policy is narrower: an observed semantic FAIL must not remain represented solely as a cost-only/censored disposition; an interrupted run still establishes no semantic verdict. State that without promoting unknown to passing. A run at admission and restoration supplies evidence at those revisions, but cannot catch a regression introduced while the row remains withheld—the very temporal gap this incident illustrates. Mark that proposal's coverage as snapshot-limited and retain the existing broader execution/restoration obligation, rather than implying these two checkpoints prevent the intervening masked regression. No new gate implementation is requested in this RFM-only cut.

Reviewed the complete four-file diff, exact-head DESIGN, cost-debt authority, witness predicates and analyzer paths. The PR's execution/bisect numbers remain author-reported receipts; I did not execute local tests or reproduce the bisect. Exact-head witnesses run 37245335040 was still in progress at review.

[briansrls]

APPROVE at exact head ff46b2a02eb094825321166d87d74974cc3e9c44, against DESIGN.md §§3, 4b(1)/(3)/(4), 5 and 6b. Both blockers from review 5408873037 are closed.

Compared the complete one-commit, two-file correction from 01234d88492b4eff7c7e1c042b98fbcafe315b4f and re-read the full four-file PR diff. DESIGN.md, the analyzer, witness predicates and cost-debt authority are unchanged from the prior review.

1. The accumulator row now distinguishes absence of Poly2Suspect from a clean result. It names the existing Unclassifiable/fold_accumulator_unread refusal, does not invent a downstream consumer that discards it, and records the 19 failures as a mixed population including positive, refusal, clean and conjunctive controls. The carrier-binding explanation and #13028 attribution remain hypotheses, not a measured common cause for every failure. The restoration trigger now requires carrier binding AND Poly2Suspect for the supported inline-fold positives, preserving clean and unsupported/refusal controls. The already-existing named refusal can no longer satisfy that trigger.

2. The cost-row proposal now preserves the authority's PROVEN-versus-CENSORED distinction: interruption supplies no semantic verdict, and an observed FAIL must not remain represented solely as cost/censored debt. Admission/restoration checks are explicitly snapshot-limited and supplement, rather than replace, the existing execution/restoration obligation. No implemented gate or continuous coverage is claimed.

The unchanged single_arm_match bisect report and CWC diagnosis retain their prior disposition; this approval does not independently reproduce those measurements or establish the unbisected causes. The PR records the residual defects and restoration requirements only. It does not repair the compiler/lens, discharge the outstanding controls, or approve a new gate implementation; those remain separate work.

Source review only; no local tests or bisect runs performed by this reviewer. Exact-head witnesses run 37246356964 is still in progress. No semantic blocker remains on this RFM-only change; land after the required exact-head checks pass.