refactor(program): a direction carries what a consumer reads, not the check the loader makes

docs/reference/reading.md

@@ -87,7 +87,9 @@ node's operands, and `where_children()` walks a predicate's. `walk()` yields
 every node under an expression, parents first. `walk_regions()` yields each node
 with the `cases:` regions it stands inside, outermost first.
 
-Every `where` arrives as a `Mask`. Its `.root` is the resolved predicate. The
+Every `where` arrives as a `Mask`. Its `.root` is the resolved predicate. One
+member of the `Predicate` union never reaches you. Lowering rewrites every
+`ArithmeticComparison` into an `ExpressionComparison`. The
 mask also answers four questions:
 
 - `.conjuncts` flattens the `AND` spine, and stops at an `OR` or a `NOT`.

src/math_spec/program.py

@@ -266,7 +266,7 @@ class Pullback:
 
     The dims ``direction`` consumes go and the dims it produces arrive, one
     value per coordinate because the read takes value columns at a key the
-    result fixes (``Direction.is_single_valued``). The join fans out, many
+    result fixes, which the loader checks. The join fans out, many
     produced tuples sharing one consumed tuple — at each coordinate of the
     joined columns, which the operand carries and the result keeps.
     """
@@ -499,11 +499,6 @@ def produced_dims(self) -> tuple[str, ...]:
     def joined_dims(self) -> tuple[str, ...]:
         return tuple(self.dim(role) for role in self.joined)
 
-    @property
-    def is_single_valued(self) -> bool:
-        """Whether the read is one value per coordinate: the key lies inside what is fixed."""
-        return set(self.relation.key) <= {*self.joined, *self.produced}
-
 
 @dataclass(frozen=True)
 class Partition:
@@ -1268,8 +1263,10 @@ class Or:
     right: Predicate
 
 
-#: Every resolved predicate node — what a lowered mask's ``root`` is built of.
-#: The parser's ``Unresolved*`` nodes are not members: they live with the
+#: Every resolved predicate node. A lowered mask's ``root`` holds every member
+#: but :class:`ArithmeticComparison`, which lowering rewrites into an
+#: :class:`ExpressionComparison`, so a consumer walking a program never meets
+#: one. The parser's ``Unresolved*`` nodes are not members: they live with the
 #: grammar in :mod:`math_spec._where_parser`, and resolution rewrites them away
 #: before anything here is asked.
 Predicate = (

src/math_spec/resolution.py

@@ -626,15 +626,16 @@ def _direction(
                 )
                 return None
         joined = tuple(r for r in shape.key if r not in from_roles and r not in into_roles)
+        single_valued = set(shape.key) <= {*into_roles, *joined}
         direction = Direction(name, shape, from_roles, into_roles, joined)
-        if not forward and not direction.is_single_valued:
+        if not forward and not single_valued:
             self.errors.append(
                 f"{context}: {call}: at reads one value per coordinate, and '{name}' is not single-valued in "
                 f'{list(from_roles)} at the columns the call lands on ({[*into_roles, *joined]}) — its key is '
                 f'{list(shape.key)}. Key the table by the columns the call lands on, or read the other way.'
             )
             return None
-        if forward and direction.is_single_valued:
+        if forward and single_valued:
             self.errors.append(
                 f'{context}: {call}: this sum lands on the key {list(shape.key)}, so each coordinate has one '
                 f"term and nothing is added up — that is a read, which is at()'s. Write "