v2 infer: binary algebra operators derive through inhabitance rows (Bool ||; Int-only add arm deleted)

[gunbai-bot]

Stacked on #13054 (the dag-language inhabitance rows); the base is session/silent-crab-339-dag-inhabitance.

What

v2 infer derives a binary algebra operator through one route. The operator's signature field comes from v2.std.compilers.target_model canonical_operation_from_wire_node, and the bare + token is canonical_operation_op_add. That field must be declared by the operand type's row in v2.extdeps.languages.dag dag_algebra_inhabitance_decls. The result is the operand type, because the binary field's codomain is its inhabitant (algebra_binary_fn_node).

The Int-only arm is deleted in the same change: infer_transform_operator_is_int_add, plus the infer_branch_type_is_int gate on the add path. The arm's own shape check, infer_transform_is_binary_infix_int_add_shape, becomes infer_transform_is_binary_infix_algebra_shape. infer_branch_type_is_int stays, because match scrutinees still use it. Int + now derives through Int's ordered-ring row, and Bool || through Bool's boolean-algebra row, by the same arm. Bool && also derives now, through ^lattice_field_meet on the same boolean-algebra row. That falls out of the single route rather than needing its own arm (review 74570). Any other algebra-primitive operator derives exactly when its operand type's row declares the field.

Why

found || … derived no type at all, the next native wall in N7-1 after the fold driver (#13028). Re-derived, the Int arm was validation standing in for a missing inhabitance fact. #13054 supplies that fact in the operator's own vocabulary, so the arm reads rows rather than hard-coding a type.

Controls (v2.test.claim.algebra_operator_derivation, seed)

control	main	this PR
a || b over Bool declared -> Int refuses arrow_body_does_not_inhabit_declared_return (the join derives Bool)	red	green
a || b over Int refuses infer_transform_operand_type_mismatch	red	green
a + b over Int declared -> Bool refuses (add still derives Int)	green	green
a + b over Bool refuses infer_transform_operand_type_mismatch	green	green
well-typed || over Bool and + over Int are accepted	green	green

For the main column, main's 04_infer.dag was swapped in under the same tests. Int-add behaviour unchanged: an infer-entries digest over six Int-add fixtures (4 inferred, 2 rejected) is byte-identical between main and this head (9,585 bytes).

The two-representation fork this works around without fixing is filed on #13054: algebra_structure_has_two_representations_with_no_declared_mapping.

🤖 Generated with Claude Code

Warm-row debt (amended freeze, sharp-raven-357): this PR restores these floor_cross_claim_pure_producers_warm rows so its own floor passes before #13043 lands. royal-deer-478 drops them when #13043 merges.

• v2.test.claim.algebra_operator_derivation.aod_bool_join_declared_int_reason
• v2.test.claim.algebra_operator_derivation.aod_int_add_declared_bool_reason
• v2.test.claim.algebra_operator_derivation.aod_bool_add_reason
• v2.test.claim.algebra_operator_derivation.aod_int_join_reason
• v2.test.claim.algebra_operator_derivation.aod_bool_join_ok_reason
• v2.test.claim.algebra_operator_derivation.aod_int_add_ok_reason

Since the side-chat objection (inhabitant-mismatch fork), head 47a9c0e

The defect. infer_algebra_field_result_type picked a row by its outer decl.inhabitant, but read the fields from decl.algebra. The #13054 reader threw away that node's own ^inhabitant_edge target. So the row {inhabitant: Int, algebra: boolean_algebra_node(Bool)} made Int || Int derive Int. The inverse row gave Bool the ring fields.

The fix, by construction.

• v2.std.algebra_structure_signature gains algebra_inhabitance_field_reading. It reads the carrier (the ^inhabitant_edge target) and the field answer from the same inhabitance node. Either edge missing or ambiguous is refused as malformed, with its cause.
• algebra_inhabitance_field_declaration is now derived from that reading. It is not a second reader.
• Infer picks the row by the carrier that reading returns. Its answer path no longer reads decl.inhabitant at all. Nothing reconciles two copies, because only one is ever read.
• The rows are now a parameter. Production passes dag_algebra_inhabitance_decls().

Behaviour change. A malformed row is refused with its own cause even when the row is for another type. Before, rows were filtered by the outer field first, so a malformed row was only checked if its outer field matched. With the carrier read from the node, there is nothing to filter on before reading it.

Controls: three supplied-row mutation controls, each with an outer inhabitant that disagrees with its own ^inhabitant_edge. They supply rows at the derivation's own interface (DESIGN §3 witness rule). Claims (1)-(4) remain the real-path inhabitance: the production rows run through assemble and infer.

• aod_outer_inhabitant_lends_no_join: outer Int over a Bool boolean algebra. Int with || is not carried.
• aod_outer_inhabitant_lends_no_add: outer Bool over an Int ordered ring. Bool with + is not carried.
• aod_embedded_carrier_selects_the_row: the same mismatched row derives Bool for Bool with ||. This is the positive arm: the fix does not pass merely by refusing every mismatched row.

Red before the fix. At this diff, with only the old selection by decl.inhabitant restored, all three FAIL (local claim_batch, 3/3 FAIL). That proves they discriminate.

Green after the fix, local claim_batch: 18/18 PASS.

• the 8 aod claims, including (1)-(4);
• the 10 dai claims from dag language: primitive algebra inhabitance rows (signature world, witnessed by std values) #13054, whose reader is now the projection.

Cost. The new claims cost 4997, 2998 and 2184 eval steps, all far under the 72,300 budget, and need no roster rows. The aod real-path claims are unchanged and already in the floor's warm list.

Main merged. The only conflict was in floor_pure_producer_share.dag: both sides added warm-list entries, and I kept both sides' entries.

Not in this PR. AlgebraInhabitanceDecl.inhabitant still duplicates the embedded edge (DESIGN §3). It has other users: about 12 language models produce it, and v2.lens.leaf_model_verification rebuilds an inhabitance from both fields. Deleting it is a de-fork across those producers, so it is a separate change. This PR removes it only from the operator answer path.

[gunbai-bot]

Both findings in review 74481 are fixed at 3e54e3c.

1. The field check now reads the declared field set, not a node search. v2.std.algebra_structure_signature gains algebra_inhabitance_declares_field, added on dag language: primitive algebra inhabitance rows (signature world, witnessed by std values) #13054 where the signature lives and merged here. It reads the inhabitance's ^algebra_edge structure, collects its binders, and enters only binder types that are themselves structures. That is how ordered_ring composes ring, and boolean_algebra composes bounded_lattice. It never enters an operation's signature (an Arrow) or the carrier. infer_signature_declares_field is deleted, and infer_algebra_field_result_type calls the accessor.
   • Route, not only the answer: dag language: primitive algebra inhabitance rows (signature world, witnessed by std values) #13054's witness now reads the accessor too, and gains dai_a_name_inside_an_operation_signature_is_not_a_declared_field. It builds a structure whose one operation's argument type binds ^lattice_field_join and asserts the field is NOT declared. A node search finds the name there, so the control goes red if the reading ever falls back to a search.
   • The aod controls (5/5) and the dai witness (4/4) pass on the seed.
2. The comment above the derivation is rewritten to describe the one-route algebra-primitive derivation. The add-only wording and its dissolve-on are gone. The doc comment on infer_algebra_field_result_type now also says why the result is the operand type: every binary primitive these structures carry is closed on the carrier. The earlier text claimed the field's codomain is the inhabitant via algebra_binary_fn_node, which is true for the lattice join but not literally for ring add, a composed abelian group.

— sent from silent-crab-339

[gunbai-bot]

Fixed at 74246ba (review 74715): the census row for the deleted infer_transform_operator_is_int_add is removed from dag/gunbc/non_fold_residue.dag in the same PR that deletes the function, so X's authority ends in one motion.

On the new helpers: infer_binary_algebra_field, infer_operator_is_plus_token, infer_wire_algebra_field, infer_canonical_operation_field and infer_algebra_field_result_type have NO wildcard arm. An earlier commit on this PR made every match over a closed coproduct exhaustive (CanonicalOperation's five variants, Optional Present/Absent, AlgebraFieldDeclaration, InferAlgebraFieldResult). The census rosters only wildcard arms over closed coproducts, so none of them needs a row.

I checked the whole census for rows naming a function that no longer exists on this head. The only other stale row is dag/gunbc/auth/credentials.dag::gcp_oauth_access_token_adc_for_path. It is stale on main as well, so it is not this PR's.

— sent from silent-crab-339

[gunbai-bot]

The side-chat objection (inhabitant-mismatch fork) is fixed at 47a9c0e.

Rows are now picked by the carrier that the inhabitance node itself is over, read by the new algebra_inhabitance_field_reading from the same node as the field answer. decl.inhabitant is no longer read on this path.

Three supplied-row mutation controls cover it:

• an outer Int over a Bool algebra gives || nothing;
• the inverse gives + nothing;
• the positive arm derives Bool.

All three FAIL with the old selection restored, and the local claim_batch passes 18/18 with the fix. Main is merged. Details are in the PR description; it needs a fresh review on this head.

— sent from calm-boar-904