Ground CanonicalOperation beyond OpAdd: arith+comparison+boolean operators by inhabitance from existing algebra (target_model.dag)

[briansrls]

Track-A operation-grounding (cargo-green keystone)

Grounds CanonicalOperation (LOAD-BEARING target_model.dag) beyond OpAdd to the full arith + comparison + boolean operator set the self-hosted emitter needs, by inhabitance from v2.std.algebra (§3/§4: no per-operator nicknames; each operator points at the algebra field that provides it).

This restores the full verified scope of #5698 (which this supersedes) — same 3-file shape, same Equivalence<T> mint, same 9 by-execution witnesses — and fixes the non_fold_residue lens red that blocked #5698 (see "Lens" below).

Model — 4 grounded variants

type CanonicalOperation
  = AlgebraPrimitive      { algebra_field: Symbol }                       -- add, mul, negate, and, or, not
  | AlgebraInverseCompose { binary_field: Symbol, inverse_field: Symbol } -- sub = a + (−b);  div = a · (1/b)
  | OrderingComparison    { compare_field: Symbol, predicate: OrderingPredicate }  -- < <= > >=
  | EqualityComparison    { eq_field: Symbol,      predicate: EqualityPredicate }  -- == !=

Grounding (every symbol already exists in algebra.dag):

op	grounding
+ *	^ring_field_add / ^ring_field_mul (AlgebraPrimitive)
unary -	^group_field_inverse (AlgebraPrimitive)
&& || !	^lattice_field_meet / ^lattice_field_join / ^boolean_algebra_field_complement
binary -	AlgebraInverseCompose(^ring_field_add, ^group_field_inverse) — subtraction as the additive-inverse composite, the binary form (not the partial unary field)
/	AlgebraInverseCompose(^ring_field_mul, ^field_field_reciprocal)
< <= > >=	^ordered_ring_field_compare + OrderingPredicate (which Orderings count as true)
== !=	^equivalence_field_eq + EqualityPredicate

Equivalence<T> is minted in src/v2/std/algebra.dag ({ eq: fn(T,T) -> Bool }, with equivalence_type_node/equivalence_node + bool_type_node). Equality grounds on its own algebra — not on ordered-ring compare — so Eq is not conflated with order (a type can have equality without order). This is the structurally-correct grounding the api-review flagged in the earlier 2-variant pass.

AlgebraInverseCompose likewise grounds binary -// on two fields (the forward op + its inverse), so the algebra field names the binary operator, not the partial unary one.

The downstream operator machinery was already generic (catalog keyed on canonical_operation_equal over the decoded wire node; emit via InfixToken/PrefixToken/CallIdent), so the type generalization lights up every operator with zero per-operator emit code — one DRY …_atom_field_from_wire reader, symbol-coded predicates, exhaustive encode/decode.

Lens — non_fold_residue green by construction (the #5698 fix)

#5698 readded four _ => false wildcards over the now-closed CanonicalOperation coproduct in canonical_operation_equal; the non_fold_residue roster gate walls any new unrostered wildcard-over-closed-coproduct, so it red. Here canonical_operation_equal enumerates all cross-variant arms explicitly (no _) — construction, not a wildcard the lens has to catch (§5). Verified: non_fold_residue_no_unrostered_or_stale → Bool(true) by execution.

Witnesses — 9/9 green by execution (…/target_operation_grounding_emit_typescript_test.dag)

Auto-enrolled in the CI floor (*_test.dag with test fns). End-to-end TypeScript emit through the catalog + projection, not just the model:

• emits x - y (sub), x < y (lt), x == y (eq);
• discriminating reds: wrong-token catalog emits x + y (≠ x - y); catalog miss rejects; wire round-trip for all 14 ops; wire discrimination (sub≠add, lt≠gt, le≠ge, eq≠ne);
• OrderingPredicate/EqualityPredicate accept-set units (IsLessOrEqual → [Less, Equal], IsEqual → true, …).

All 9 + the lens verified green locally against the live corpus.

Follow-on

Wiring surface-token → CanonicalOperation ingest (extdeps/languages/dag.dag) and the per-target realization-row catalogs (rust/ts) for - * / < … && || is downstream (separate files/lane) and rides on these constructors.

Supersedes #5698 (orphaned predecessor branch). canonical_operation_op_add() keeps its name/meaning, so existing extdeps/languages/{typescript,dag}.dag callers are untouched.

🤖 Generated with Claude Code