affected_set frontier receipts: observe Map by application, not whole-frontier ==

[briansrls]

Summary

Triages and fixes the runtime-false affected_set frontier receipts named in the work item (excluded_propagation_proof, irt1_excluded_propagation_receipt) plus the two same-root-cause dimension_seed receipts that block the IRT-1 leaf suite.

Triage verdict: it is the BROADER map-equality substrate, NOT local mark_excluded/mark_rerun.

ReExecFrontier.decisions is a std Map<K,V>, which is a PartialFunction (v4.std.collection: lookup: fn(K) -> Witness<V>). Over structural (non-String) keys (ExclusionKey), the v2 runtime drops out of the native Value::Map (HashMap<String,Value>) fast path — the map_insert builtin only matches Value::Str keys — and lands on the closure/record form Map { lookup: fn... }. PartialEq for Value has no closure arm, so two such maps compare _ => false, even a value against itself.

Probe receipts: empty_map()==empty_map() true; one structural-key entry == itself false; expected_frontier == itself false; key/proof/Node value equality all true (so values are fine — only the Map == is broken). So mark_excluded/mark_rerun produce the correct structure; the receipts asserted an undecidable whole-frontier ==.

Fix (model-correct, test-only)

A PartialFunction is observed by application. New shared helper frontier_observation.frontier_decision_matches looks the seeded key up via map_get and compares the resolved FrontierDecision (a coproduct over lists/records, which do compare structurally). No lens/std code touched — only src/v4/test/claim/lens_affected_set/. Not wired into any CI gate roster (left to the lens-CI lane).

Perturb-discrimination evidence (committed, reviewable)

Each receipt ships a committed _discriminates witness proving the comparison is a real structural compare, not a tautology that launders broken Map== into a weaker always-true:

• *_excluded_*_discriminates: a single mark_excluded yields rest:[], which must NOT match the accumulated expected decision rest:[proof] → asserts frontier_decision_matches(...) == false.
• *_dimension_seed_*_discriminates: the seeded decision is Rerun, which must NOT match a wrong Excluded decision → asserts frontier_decision_matches(...) == false.

If frontier_decision_matches were a tautology, these would all be false. They are all true, i.e. the wrong expected decision is correctly rejected (perturb-red).

Test plan

target/release/gunbc run --source-root src/v4 --entry <file> --function <fn> --claim-run:

witness	result
excluded_propagation_proof_claim_holds	true
excluded_propagation_proof_discriminates	true (wrong rest:[] rejected)
irt1_excluded_propagation_receipt_claim_holds	true
irt1_excluded_propagation_receipt_discriminates	true
dimension_seed_rerun_claim_holds	true
dimension_seed_rerun_discriminates	true (wrong Excluded rejected)
irt1_dimension_seed_receipt_claim_holds	true
irt1_dimension_seed_receipt_discriminates	true
affected_set_irt1_leaf_claim_suite_holds	true (all six leaves green)

The real structural-key Map== substrate fix (unify Map representation) stays the tracked 🟡 in v4.std.collection — a separate load-bearing std.collection lane, not this PR.

Closes #N (dashboard node adhoc-29b13bdc-60a)