Consolidate structural_similarity into the intent_linearity registry as a row (one engine, two binders)

[gunbai-bot]

Per the consolidation map in docs/plans/self-applying-lenses.md (#5584): the redundancy lenses become rows of one anti-unification engine, not peers. This realizes structural_similarity as Row 2 of the intent_linearity registry.

What changed

• structural_similarity.dag — realized. It was an Unrealized scaffold (no predicate). Now it carries type_decls_anti_unify, the type-decl binder over the shared congruent kernel imported from simulated_relationship: a type-declaration forest is redundant iff ≥2 decls share one skeleton (collapse to one generic — Int8..Int128 = one Compose axis; byte-identical enums = the §3 nickname). Per the consolidation trigger, the dead bespoke scaffold (StructuralSimilarityVerdict/TypeShape/VariantShape/FnShapeUnrealized, ~33 lines) is deleted; the live ConstructionJustification stays (now in realized form).
• intent_linearity.dag — Row 2 added + binder made first-class. dup_type_to_generic_rule joins unroll_to_fold_rule in linearity_registry(). Per the design draft's "(representation walked)" parameter, LinearityRule gains a representation: Representation field (TermChain | TypeForest) — the two binders. The engine (input_is_redundant_for) filters rows by representation, so the type row (threshold-2 congruent) stays off term-chain projections (where two congruent statements are not yet a fold). chain_is_redundant (term) and forest_is_redundant (type) are the two binder entry points over one registry.
• Tests. Removed the obsolete sg_claims_test.dag (asserted the deleted Unrealized verdict). Added structural_similarity/lens_unit/discriminators_test.dag (2 RED + 3 GREEN, two-sided discriminating). Added two consolidation witnesses to intent_linearity proving the type row fires through the shared engine and that binder isolation holds (a type pair is not flagged by the term binder).

Verified by execution

All 13 witnesses green via claim_batch. Discrimination proven by perturbation: reverting the predicate to the old always-false behavior turns the RED witnesses (nickname_pair_is_similar, width_family_is_similar) red while the GREEN witness stays correct. simulated_relationship's 6 witnesses unaffected (additive congruent import).

No .rs touched; no other consumer referenced the deleted scaffold types.

🤖 Generated with Claude Code

[gunbai-bot]

Thanks — valid finding, but already resolved on the current head. That REQUEST_CHANGES reviewed sha 0d2e3c82, which was a mid-merge snapshot the harness auto-pushed with conflict markers still in intent_linearity.dag (the conflict came from integrating #5579's .dag comment-wall). I've since resolved the merge and pushed 9915d57757:

• git show HEAD:src/v2/lens/intent_linearity.dag | grep -c '<<<<<<<|>>>>>>>' → 0 (the prior sha had 8).
• The conflict was driven by Parser-wall: remove DAG comment trivia rules (fail-closed by construction) #5579 making // unparseable in .dag; I stripped all comments from the 5 touched files and folded the explanatory prose into the construction_justification carriers.
• Rebuilt gunbc/claim_batch against the merged (comment-wall) parser; all 13 witnesses parse and pass green by execution (5 structural_similarity + 8 intent_linearity, incl. the binder-isolation discriminator).

Please re-review the current head. — sent from nimble-dove-287

[gunbai-bot]

Thanks for the approve. On the representation_eq note — agreed it's a dissolution candidate in principle, but leaving it as-is: it follows the established idiom for registry-internal coproduct equality (lens_id_v0_eq in v2.lens.registry is the same hand-written match over the lens-id coproduct), and there's no derived-eq mechanism in the substrate today to dissolve it into. When such a mechanism lands it should dissolve both sites together (one fix, both rows), so I'd rather not fork a one-off here now. — sent from nimble-dove-287

[gunbai-bot]

Same situation as before — already resolved on the current head. Review 31967 (REQUEST_CHANGES) was on sha 02ea7659, a mid-merge snapshot the harness auto-pushed with conflict markers still present. This was a second, larger integration: main landed #5599 (anti-unification extracted into v2.std.anti_unification, congruent removed) plus an any/for_all refactor of intent_linearity. I resolved both and pushed 062069b328:

• git show HEAD:src/v2/lens/intent_linearity.dag | grep -c '<<<<<<<|>>>>>>>' → 0; chain_is_redundant is defined once.
• structural_similarity is rebuilt on the new v2.std.anti_unification kernel: the type-decl binder now fires on fillings_all_leaves (all variance at leaf positions → type parameters). Unlike the term binder it does not require template_has_hole, so byte-identical decls (the hole-free section-3 nickname) are still caught.
• intent_linearity reconciled with main's any/for_all refactor, keeping the Representation-tagged two-binder registry.
• Rebuilt gunbc/claim_batch against the merged tree; all 13 witnesses parse and pass green by execution (a file with conflict markers could not parse, so the green run is itself proof the markers are gone).

Please re-review 062069b328. — sent from nimble-dove-287