feat(comprehension): the divisive comparative frame — "half as many" as exact integer division (PR-6c)

PR-6c adds the divisive comparative frame: "half as many" read as EXACT INTEGER
DIVISION. It is the divisor twin of PR-5c's multiplicative frame, and moves the
independent R1 gold's r1-02-half from refused → correct.

No serving path touched. No rational/fractional answer support added. Non-exact
division refuses.

Design (ADR-0134 amended — divide made symmetric with multiply):
- `_check_divide` now admits a SINGLE-DEP divide-by-dimensionless-literal
  (item / dimensionless = item), the exact twin of single-dep multiply. The
  2-dep rate-divide path is untouched. This keeps the IR's "literal operands
  are not deps" invariant (proven in PR-6a) uniform across Mul AND Div, so the
  reader builds both without a per-op special case and WITHOUT synthesizing a
  divisor symbol that would pollute the setup-oracle's unit signature.
- `Div(Symbol, Literal)` IR node: "ref / divisor", operation_kind "divide",
  projects to `divide_by`. Divisor-only contract mirrors the scalar-only one.
- Reader: `_DIVISOR_WORDS={half:2}` slots into the same 8-token "<WORD> as many"
  template as the factor words; graph carries only the two entities.
- Gold reconciliation: r1-02 placeholder `times_as_many factor 0.5` → exact
  `divide_by divisor 2` (gold 4). Makes the INDEPENDENT gold integer-faithful.

The wrong=0 boundary — exact divisibility:
  the oracle admits `divide_by` only when `base % divisor == 0`. An odd base
  halved REFUSES (gold_error), never floors to a wrong integer. Divisor must be
  a nonzero int (0, 0.5, 1.5, bool all refuse); divisor=1 is intentionally the
  identity (pinned). admissibility proves DIMENSION; the oracle proves EXACT VALUE.

Meaningful-fail (CLAUDE.md Schema-Defined Proof Obligations), both verified red:
- drop the `% divisor` guard → test_oracle_refuses_non_exact_division fails (returns 3).
- disable the single-dep divide branch → the admissibility test AND the reader's
  `half` test fail (admissibility refuses → reader refuses → half stays refused).

Gates:
  R1 setup:   3 correct / 0 wrong / 7 refused
  R1 answers: 3 correct / 0 wrong / 7 refused / setup_wrong 0 / gold_error 0
  15-case setup: 15 / 0 / 0
  91 PR-6c tests + 60 relational lanes + 56 architectural invariants + 502
  binding-graph/proof-chain/adapter tests green. All 8 SHA-content lanes match
  (serving unmoved; admissibility has no generate.derivation/reliability_gate consumer).

docs/decisions/ADR-0134-binding-graph-admissibility.md

@@ -48,7 +48,7 @@ Add three deliverables under `generate/binding_graph/`:
    | `add` / `subtract` / `compare_additive` / `transfer` | all dep units equal; lhs == that unit |
    | `compare_multiplicative` | dep units cancel; lhs dimensionless |
    | `multiply` | lhs == product of dep units |
-   | `divide` | requires one dividend + one `*__divisor` literal; lhs == quotient |
+   | `divide` | **single dep**: divide by an implicit dimensionless literal, lhs == dividend unit (`x / dimensionless = x`); **two deps**: one dividend + one `*__divisor` literal, lhs == quotient |
    | `apply_rate` | dep with `semantic_role='rate'` carries `X/Y`; other dep carries `Y`; lhs == `X` |
 
    Refusal is typed: every `AdmissibilityError` carries a `reason` from
@@ -170,3 +170,36 @@ None. The binding graph still has no runtime wiring outside
 `generate/binding_graph/`. `chat/runtime.py`, the cognition eval lane,
 the field invariant, the algebra backend, and every other production
 hot path are unaffected. Cognition eval lane byte-equal to main.
+
+## Amendment 2026-06-07 — single-dep `divide` (divide by a dimensionless literal)
+
+**What changed.** `_check_divide` now admits a **single-dep** form in addition
+to the original two-dep `dividend + *__divisor` form: a quantity divided by an
+implicit *dimensionless literal*, with `lhs == dividend unit`.
+
+**Why.** The off-serving comprehension reader's typed expression IR
+(`generate/quantitative_expr.py`, PR-4/5c/6a) carries literal operands *inside*
+the IR and deliberately does **not** make them dependencies — a `Mul(Symbol,
+Literal)` ("twice as many") has `dependencies = {ref}`, and `_check_multiply`
+already admits that single dep (`item × dimensionless = item`). "half as many"
+(`Div(Symbol, Literal(2))`) is the exact divisive twin: same shape, same single
+dep, the divisor is a dimensionless `Literal` in the IR. The original two-dep
+convention (a synthesized `*__divisor` *symbol*) collides with that IR design and
+would force a per-op special case in the reader plus an extra graph symbol. The
+single-dep form makes `divide` **symmetric with `multiply`** so the IR's
+"literal operands are not deps" invariant holds uniformly for both.
+
+**Safety.**
+- The two-dep rate-adapter path (`*__divisor`) is unchanged.
+- Soundness: dividing a unit-bearing quantity by a dimensionless constant
+  preserves the unit by construction — identical to the multiply twin.
+- Exactness (the *value*, not the unit) is the answer oracle's responsibility:
+  `evals.relational_metric.oracle` admits `divide_by` only when
+  `base % divisor == 0`, refusing a non-exact division (an odd base over 2)
+  rather than flooring to a wrong integer. Admissibility proves *dimension*; the
+  oracle proves *exact integral value*.
+- Off-serving: `admissibility.py` has no `generate.derivation` /
+  `core.reliability_gate` consumer; the frozen GSM8K serving metric cannot move.
+- Pinned by `tests/test_binding_graph_admissibility.py`
+  (`test_divide_single_dep_dimensionless_keeps_unit`,
+  `test_divide_refuses_zero_or_three_deps`).

evals/relational_metric/oracle.py

@@ -16,11 +16,16 @@ Supported relation kinds (the v1 + PR-6b forward-substitutable grammar):
 - ``more_than``     : ``entity = ref + delta``
 - ``fewer_than``    : ``entity = ref - delta``
 - ``times_as_many`` : ``entity = ref * factor`` (dimensionless integer scalar)
+- ``divide_by``     : ``entity = ref // divisor`` (exact integer division only)
 - ``sum_of``        : ``entity = sum(parts)``  (part-whole / total)
 
 Every relation's references must already be resolved (forward-substitutable /
-triangular). The oracle refuses anything else, never guesses.  PR-6b keeps this
+triangular). The oracle refuses anything else, never guesses.  PR-6b/6c keep this
-off-serving: it lets setup-correct R1 cases compute answers in the eval lane only.
+off-serving: they let setup-correct R1 cases compute answers in the eval lane only.
+
+``divide_by`` is exact-only: a non-exact division (``base % divisor != 0``, e.g. an
+odd base halved) REFUSES rather than flooring to a wrong integer — the wrong=0 boundary
+for the "half as many" frame (PR-6c).
 """
 
 from __future__ import annotations
@@ -32,7 +37,9 @@ class OracleError(ValueError):
     """Malformed or out-of-grammar case — the oracle refuses, never guesses."""
 
 
-_SUPPORTED = frozenset({"fact", "more_than", "fewer_than", "sum_of", "times_as_many"})
+_SUPPORTED = frozenset(
+    {"fact", "more_than", "fewer_than", "sum_of", "times_as_many", "divide_by"}
+)
 
 
 def oracle_answer(relations: list[dict[str, Any]], query: dict[str, Any]) -> int:
@@ -75,6 +82,17 @@ def oracle_answer(relations: list[dict[str, Any]], query: dict[str, Any]) -> int
             if not isinstance(factor, int) or isinstance(factor, bool):
                 raise OracleError(f"factor must be int: {rel!r}")
             values[entity] = values[ref] * factor
+        elif kind == "divide_by":
+            ref = rel.get("ref")
+            divisor = rel.get("divisor")
+            if ref not in values:
+                raise OracleError(f"forward reference to unresolved {ref!r}")
+            if not isinstance(divisor, int) or isinstance(divisor, bool) or divisor == 0:
+                raise OracleError(f"divisor must be a nonzero int: {rel!r}")
+            if values[ref] % divisor != 0:
+                # Exact-only: refuse rather than floor to a wrong integer (wrong=0).
+                raise OracleError(f"non-exact division {values[ref]}/{divisor}: {rel!r}")
+            values[entity] = values[ref] // divisor
         else:  # sum_of
             parts = rel.get("parts")
             if not isinstance(parts, list) or not parts:

evals/setup_oracle/r1_gold.jsonl

@@ -1,5 +1,5 @@
 {"id": "r1-01-twice", "text": "Anna has 6 apples. Bella has twice as many apples as Anna. How many apples does Bella have?", "relations": [{"kind": "fact", "entity": "anna", "value": 6}, {"kind": "times_as_many", "entity": "bella", "ref": "anna", "factor": 2}], "expected_units": {"anna": "item", "bella": "item"}, "query": {"entity": "bella", "unit": "item"}, "gold": 12, "notes": "Multiplicative: bella = 2 * anna. The reader has no multiplicative template AND 'twice' is non-digit -> must REFUSE, never misread as a fact/additive."}
-{"id": "r1-02-half", "text": "Carl has 8 coins. Dora has half as many coins as Carl. How many coins does Dora have?", "relations": [{"kind": "fact", "entity": "carl", "value": 8}, {"kind": "times_as_many", "entity": "dora", "ref": "carl", "factor": 0.5}], "expected_units": {"carl": "item", "dora": "item"}, "query": {"entity": "dora", "unit": "item"}, "notes": "Multiplicative (factor 0.5). 'half' is non-digit -> must REFUSE."}
+{"id": "r1-02-half", "text": "Carl has 8 coins. Dora has half as many coins as Carl. How many coins does Dora have?", "relations": [{"kind": "fact", "entity": "carl", "value": 8}, {"kind": "divide_by", "entity": "dora", "ref": "carl", "divisor": 2}], "expected_units": {"carl": "item", "dora": "item"}, "query": {"entity": "dora", "unit": "item"}, "gold": 4, "notes": "Divisive: dora = carl / 2 = 4 (exact integer division). 'half as many' fits the [Y has WORD as many UNIT as X] template; the WORD maps to a divisor, not a factor (PR-6c). Exact-divisibility is the wrong=0 boundary: an odd base would refuse, never round."}
 {"id": "r1-03-more-total", "text": "Finn has 10 books. Evan has 5 more books than Finn. How many books do Evan and Finn have altogether?", "relations": [{"kind": "fact", "entity": "finn", "value": 10}, {"kind": "more_than", "entity": "evan", "ref": "finn", "delta": 5}, {"kind": "sum_of", "entity": "total", "parts": ["evan", "finn"]}], "expected_units": {"finn": "item", "evan": "item", "total": "item"}, "query": {"entity": "total", "unit": "item"}, "notes": "Additive + aggregate. 'altogether' (not the bare 'have') may fall outside the strict query template -> likely REFUSE; if read, structure must match exactly."}
 {"id": "r1-04-fewer-total", "text": "Gail has 20 cards. Hank has 6 fewer cards than Gail. How many cards do Gail and Hank have in total?", "relations": [{"kind": "fact", "entity": "gail", "value": 20}, {"kind": "fewer_than", "entity": "hank", "ref": "gail", "delta": 6}, {"kind": "sum_of", "entity": "total", "parts": ["gail", "hank"]}], "expected_units": {"gail": "item", "hank": "item", "total": "item"}, "query": {"entity": "total", "unit": "item"}, "notes": "Additive(fewer) + aggregate. 'in total' qualifier likely outside the query template -> REFUSE expected."}
 {"id": "r1-05-chain", "text": "Ivy has 4 pens. Jon has 3 times as many pens as Ivy. Kim has 2 more pens than Jon. How many pens does Kim have?", "relations": [{"kind": "fact", "entity": "ivy", "value": 4}, {"kind": "times_as_many", "entity": "jon", "ref": "ivy", "factor": 3}, {"kind": "more_than", "entity": "kim", "ref": "jon", "delta": 2}], "expected_units": {"ivy": "item", "jon": "item", "kim": "item"}, "query": {"entity": "kim", "unit": "item"}, "gold": 14, "notes": "Multi-step derived chain: jon=3*ivy (intermediate), kim=jon+2. The multiplicative middle step has no template -> must REFUSE the whole reading, never read a partial/wrong chain."}

evals/setup_oracle/signature.py

@@ -45,6 +45,8 @@ def relation_signature(relations: list[dict[str, Any]]) -> tuple[tuple, ...]:
             out.append((kind, r["entity"], r["ref"], int(r["delta"])))
         elif kind == "times_as_many":
             out.append(("times_as_many", r["entity"], r["ref"], r["factor"]))
+        elif kind == "divide_by":
+            out.append(("divide_by", r["entity"], r["ref"], int(r["divisor"])))
         elif kind == "sum_of":
             out.append(("sum_of", r["entity"], tuple(sorted(r["parts"]))))
         else:  # an unknown relation kind is itself a structural difference, not a crash

generate/binding_graph/admissibility.py

@@ -218,14 +218,30 @@ def _check_multiply(
 def _check_divide(
     dep_units: list[tuple[SymbolBinding, UnitVector]],
 ) -> UnitProof:
-    """Dividend / divisor. Divisor identified by ``__divisor`` suffix.
+    """Dividend / divisor. Two admissible forms:
 
-    Refuses with ``operand_arity`` if dep set is not exactly one dividend
+    - **single dep** — divide by an implicit *dimensionless literal* (the reader's
-    + one ``*__divisor`` literal. The adapter is responsible for naming.
+      "half as many"). The divisor is carried in the reader's typed IR as a
+      dimensionless :class:`~generate.quantitative_expr.Literal`, NOT as a graph
+      symbol, exactly as the multiplicative factor is. This is symmetric with
+      :func:`_check_multiply`'s single-dep dimensionless scaling: the quotient keeps
+      the dividend's unit (``x / dimensionless = x``).
+    - **two deps** — dividend + a ``*__divisor`` literal (the rate-adapter convention).
+      lhs == quotient of the two units. The adapter is responsible for naming.
+
+    Refuses with ``operand_arity`` for any other arity.
     """
+    if len(dep_units) == 1:
+        # Divide by an implicit dimensionless literal — symmetric with single-dep
+        # multiply. No graph divisor symbol exists, so there is nothing to quotient
+        # against; the quotient keeps the dividend's unit by construction.
+        only = dep_units[0][1]
+        return UnitProof(
+            operation_kind="divide", lhs_unit=only, operand_units=(only,)
+        )
     if len(dep_units) != 2:
         raise AdmissibilityError(
-            "operand_arity", f"divide requires exactly 2 deps; got {len(dep_units)}"
+            "operand_arity", f"divide requires 1 or 2 deps; got {len(dep_units)}"
         )
     dividend: UnitVector | None = None
     divisor: UnitVector | None = None

generate/quantitative_comprehension.py

@@ -43,6 +43,7 @@ from generate.binding_graph.units import UnitAlgebraError, parse_unit
 from generate.meaning_graph.reader import Refusal, _split_sentences
 from generate.quantitative_expr import (
     Add,
+    Div,
     Expr,
     Literal,
     Mul,
@@ -154,25 +155,48 @@ class _Mul:
     unit: str
 
 
-#: Word factors for "twice/double/triple ... as many". 'half' (a /2, the divide path)
+@dataclass(frozen=True, slots=True)
-#: is deliberately ABSENT — divide-by-literal is a separate admissibility path, deferred.
+class _Div:
+    """Divisive comparative: entity = ref / divisor (R1, "half as many"). The
+    divisor is a dimensionless integer literal; the quotient keeps ref's unit."""
+
+    entity: str
+    ref: str
+    divisor: int
+    unit: str
+
+
+#: Word factors for "twice/double/triple ... as many" (a multiply by a dimensionless int).
 _FACTOR_WORDS: dict[str, int] = {"twice": 2, "double": 2, "triple": 3, "quadruple": 4}
 
+#: Word divisors for "half ... as many" (a divide by a dimensionless int). The divisive
+#: twin of ``_FACTOR_WORDS``; both slot into the same 8-token "<WORD> as many" template.
+#: 'third'/'quarter' (non-power-of-two surface forms with an article) are deferred.
+_DIVISOR_WORDS: dict[str, int] = {"half": 2}
 
-def _try_multiplicative(entity: str, toks: list[str], detail: str) -> "_Mul | None":
+
-    """Match "Y has <factor-word> as many <unit> as X" or "Y has <N> times as many
+def _try_multiplicative(entity: str, toks: list[str], detail: str) -> "_Mul | _Div | None":
-    <unit> as X" → ``_Mul``. Returns None if the clause is not multiplicative (the
+    """Match the comparative templates → ``_Mul`` (multiply) or ``_Div`` (divide).
-    caller then tries the digit-led fact/additive templates)."""
+
-    # [Y, has, FACTORWORD, as, many, UNIT, as, X]
+    - "Y has <factor-word> as many <unit> as X"  → ``_Mul`` (twice/double/triple/quadruple)
+    - "Y has <divisor-word> as many <unit> as X" → ``_Div`` (half)
+    - "Y has <N> times as many <unit> as X"      → ``_Mul``
+
+    Returns None if the clause is not comparative (the caller then tries the digit-led
+    fact/additive templates)."""
+    # [Y, has, WORD, as, many, UNIT, as, X] — factor and divisor words share this shape.
     if (
         len(toks) == 8
-        and toks[2] in _FACTOR_WORDS
         and toks[3] == "as"
         and toks[4] == "many"
         and toks[6] == "as"
     ):
-        return _Mul(entity, _ident(toks[7], detail), _FACTOR_WORDS[toks[2]],
+        ref = _ident(toks[7], detail)
-                    _resolve_unit(_ident(toks[5], detail)))
+        unit = _resolve_unit(_ident(toks[5], detail))
+        if toks[2] in _FACTOR_WORDS:
+            return _Mul(entity, ref, _FACTOR_WORDS[toks[2]], unit)
+        if toks[2] in _DIVISOR_WORDS:
+            return _Div(entity, ref, _DIVISOR_WORDS[toks[2]], unit)
     # [Y, has, N, times, as, many, UNIT, as, X]
     if (
         len(toks) == 9
@@ -240,6 +264,7 @@ def comprehend_quantitative(text: str, source_id: str = "input") -> QuantCompreh
     facts: list[_Fact] = []
     eqs: list[_Eq] = []
     muls: list[_Mul] = []
+    divs: list[_Div] = []
     queries: list[tuple] = []
 
     try:
@@ -253,6 +278,8 @@ def comprehend_quantitative(text: str, source_id: str = "input") -> QuantCompreh
                 eqs.append(spec)
             elif isinstance(spec, _Mul):
                 muls.append(spec)
+            elif isinstance(spec, _Div):
+                divs.append(spec)
             else:
                 queries.append(spec)
     except _QReject as rej:
@@ -269,6 +296,8 @@ def comprehend_quantitative(text: str, source_id: str = "input") -> QuantCompreh
         unit_of[e.entity], role_of[e.entity] = e.unit, "count"
     for m in muls:
         unit_of[m.entity], role_of[m.entity] = m.unit, "count"
+    for d in divs:
+        unit_of[d.entity], role_of[d.entity] = d.unit, "count"
 
     query = queries[0]
     sum_eq: tuple[str, tuple[str, ...]] | None = None
@@ -288,6 +317,8 @@ def comprehend_quantitative(text: str, source_id: str = "input") -> QuantCompreh
         referenced.update((e.entity, e.ref))
     for m in muls:
         referenced.update((m.entity, m.ref))
+    for d in divs:
+        referenced.update((d.entity, d.ref))
     if sum_eq is not None:
         referenced.add(sum_eq[0])
         referenced.update(sum_eq[1])
@@ -321,6 +352,9 @@ def comprehend_quantitative(text: str, source_id: str = "input") -> QuantCompreh
     expr_specs.extend(
         (m.entity, Mul(Symbol(m.ref), Literal(m.factor))) for m in muls
     )
+    expr_specs.extend(
+        (d.entity, Div(Symbol(d.ref), Literal(d.divisor))) for d in divs
+    )
     if sum_eq is not None:
         lhs, parts = sum_eq
         expr_specs.append((lhs, SumOf(tuple(Symbol(p) for p in parts))))

generate/quantitative_expr.py

@@ -65,6 +65,27 @@ class Mul:
     right: "Expr"
 
 
+@dataclass(frozen=True, slots=True)
+class Div:
+    """Exact integer division of a symbol by a dimensionless literal divisor — the
+    fractional comparative ("half/a third as many"). ``left`` is the referenced symbol,
+    ``right`` a dimensionless literal divisor; the quotient keeps the symbol's unit
+    (``count / scalar = count``).
+
+    "half as many" is modelled as ``Div(Symbol, Literal(2))``, NOT ``Mul`` by a rational:
+    the system is integer-exact end to end (``oracle_answer -> int``) and :class:`Literal`
+    is a dimensionless *integer* (the contract PR-6a proved load-bearing), so a fractional
+    factor is not representable. Division by an integer divisor keeps everything integral.
+
+    Divisor-only contract (the wrong=0 boundary). The only admitted shape is
+    ``Div(Symbol, Literal)`` — see :func:`to_relation`, which refuses every other shape.
+    Exactness is enforced downstream: the answer oracle admits the quotient ONLY when
+    ``base % divisor == 0`` (an odd base over 2 refuses, never floors to a wrong integer)."""
+
+    left: "Expr"
+    right: "Expr"
+
+
 @dataclass(frozen=True, slots=True)
 class SumOf:
     """An aggregate over ≥2 symbols (the part-whole total)."""
@@ -72,7 +93,7 @@ class SumOf:
     parts: tuple[Symbol, ...]
 
 
-Expr = Union[Literal, Symbol, Add, Sub, Mul, SumOf]
+Expr = Union[Literal, Symbol, Add, Sub, Mul, Div, SumOf]
 
 
 def to_canonical_string(expr: Expr) -> str:
@@ -88,6 +109,8 @@ def to_canonical_string(expr: Expr) -> str:
             return f"{to_canonical_string(left)} - {to_canonical_string(right)}"
         case Mul(left, right):
             return f"{to_canonical_string(left)} * {to_canonical_string(right)}"
+        case Div(left, right):
+            return f"{to_canonical_string(left)} / {to_canonical_string(right)}"
         case SumOf(parts):
             return " + ".join(to_canonical_string(p) for p in parts)
     raise TypeError(f"not an Expr: {expr!r}")  # pragma: no cover - exhaustive above
@@ -100,7 +123,7 @@ def dependencies(expr: Expr) -> frozenset[str]:
             return frozenset()
         case Symbol(symbol_id):
             return frozenset({symbol_id})
-        case Add(left, right) | Sub(left, right) | Mul(left, right):
+        case Add(left, right) | Sub(left, right) | Mul(left, right) | Div(left, right):
             return dependencies(left) | dependencies(right)
         case SumOf(parts):
             out: frozenset[str] = frozenset()
@@ -119,6 +142,8 @@ def operation_kind(expr: Expr) -> str:
             return "subtract"
         case Mul(_, _):
             return "multiply"
+        case Div(_, _):
+            return "divide"
         case _:
             raise TypeError(f"expression has no operation_kind: {expr!r}")
 
@@ -129,9 +154,11 @@ def to_relation(lhs: str, expr: Expr) -> dict[str, Any] | None:
     ``None`` for a shape the projection does not handle — the caller refuses rather than
     emit a guessed relation (wrong=0 boundary). Each ``case`` is intentionally a *narrow*
     structural pattern, not a kind tag: ``Mul(Symbol, Literal)`` is the only multiplicative
-    shape projected (the scalar-only contract — a ``count × count`` ``Mul(Symbol, Symbol)``
+    shape projected and ``Div(Symbol, Literal)`` the only divisive one (the scalar/divisor
-    or a compound factor falls through to ``None``). The dimensional checker would not catch
+    contracts — a ``count × count`` ``Mul(Symbol, Symbol)``, a compound factor, or a
-    such a masquerade (it products units happily), so this boundary is load-bearing.
+    symbol-over-symbol ``Div`` falls through to ``None``). The dimensional checker would not
+    catch such a masquerade (it products/quotients units happily), so this boundary is
+    load-bearing.
     """
     match expr:
         case Add(Symbol(ref), Literal(delta)):
@@ -140,6 +167,8 @@ def to_relation(lhs: str, expr: Expr) -> dict[str, Any] | None:
             return {"kind": "fewer_than", "entity": lhs, "ref": ref, "delta": delta}
         case Mul(Symbol(ref), Literal(factor)):
             return {"kind": "times_as_many", "entity": lhs, "ref": ref, "factor": factor}
+        case Div(Symbol(ref), Literal(divisor)):
+            return {"kind": "divide_by", "entity": lhs, "ref": ref, "divisor": divisor}
         case SumOf(parts):
             return {"kind": "sum_of", "entity": lhs, "parts": [p.symbol_id for p in parts]}
         case _:
@@ -148,6 +177,7 @@ def to_relation(lhs: str, expr: Expr) -> dict[str, Any] | None:
 
 __all__ = [
     "Add",
+    "Div",
     "Expr",
     "Literal",
     "Mul",

tests/test_binding_graph_admissibility.py

@@ -247,6 +247,63 @@ def test_divide_refuses_three_deps() -> None:
     assert ei.value.reason == "operand_arity"
 
 
+# --------------------------------------------------------------------------- #
+# ADR-0134 amendment 2026-06-07 — single-dep divide (divide by a dimensionless literal)
+# --------------------------------------------------------------------------- #
+
+
+def test_divide_single_dep_dimensionless_keeps_unit() -> None:
+    """A single-dep divide (the reader's "half as many") divides by an implicit
+    dimensionless literal and keeps the dividend's unit — symmetric with single-dep
+    multiply.
+
+    Meaningful-fail: if the ``len == 1`` branch were removed (reverting to ``!= 2``
+    refuse), this admission turns into an ``operand_arity`` refusal and the assert fails.
+    """
+    symbols = {"carl": _sym("carl", unit="item")}
+    proof = check_admissibility(
+        _eq(kind="divide", deps=frozenset({"carl"})), symbols=symbols
+    )
+    assert proof.operation_kind == "divide"
+    assert proof.lhs_unit == parse_unit("item")  # item / dimensionless = item
+    assert proof.operand_units == (parse_unit("item"),)
+
+
+def test_divide_refuses_zero_or_three_deps() -> None:
+    """The single-dep extension is narrow: zero deps and three deps still refuse with
+    ``operand_arity`` — only one (dimensionless divide) or two (rate divide) are admitted.
+    """
+    with pytest.raises(AdmissibilityError) as ei0:
+        check_admissibility(_eq(kind="divide", deps=frozenset()), symbols={})
+    assert ei0.value.reason == "operand_arity"
+
+    symbols = {
+        "a": _sym("a", unit="foot"),
+        "b": _sym("b", unit="hour"),
+        "op_000__divisor": _sym("op_000__divisor", unit="hour"),
+    }
+    with pytest.raises(AdmissibilityError) as ei3:
+        check_admissibility(
+            _eq(kind="divide", deps=frozenset({"a", "b", "op_000__divisor"})),
+            symbols=symbols,
+        )
+    assert ei3.value.reason == "operand_arity"
+
+
+def test_divide_two_dep_rate_path_unchanged_by_amendment() -> None:
+    """The original two-dep rate divide (dividend + ``*__divisor``) is untouched — the
+    amendment only ADDED the single-dep form."""
+    symbols = {
+        "q_actor_foot_t0": _sym("q_actor_foot_t0", unit="foot"),
+        "op_000__divisor": _sym("op_000__divisor", unit="hour"),
+    }
+    proof = check_admissibility(
+        _eq(kind="divide", deps=frozenset({"q_actor_foot_t0", "op_000__divisor"})),
+        symbols=symbols,
+    )
+    assert proof.lhs_unit.exponents == (1, -1, 0, 0, 0, 0)  # foot / hour = speed
+
+
 # ---------------------------------------------------------------------------
 # apply_rate
 # ---------------------------------------------------------------------------

tests/test_quantitative_comprehension.py

@@ -196,3 +196,25 @@ def test_multiplicative_missing_base_refuses() -> None:
     # never fabricate a base quantity.
     comp = comprehend_quantitative("Quinn has twice as many toys as Rosa. How many toys does Quinn have?")
     assert isinstance(comp, Refusal)
+
+
+def test_half_as_many_builds_divide_equation() -> None:
+    # PR-6c: "half as many" is the divisive twin of "twice as many" — operation_kind
+    # "divide", a single symbol dep (the divisor literal is in the IR, not a graph symbol),
+    # and the REAL single-dep admissibility check (item / dimensionless = item) admits it.
+    comp = _comp("Carl has 8 coins. Dora has half as many coins as Carl. How many coins does Dora have?")
+    eq = next(e for e in comp.binding_graph.equations if e.lhs_symbol_id == "dora")
+    assert eq.operation_kind == "divide"
+    assert eq.rhs_canonical == "carl / 2"
+    assert eq.dependencies == frozenset({"carl"})  # uniform with Mul: literal not a dep
+    assert eq.admissibility_status == "admitted"
+    assert single_unknown(comp.binding_graph).symbol_id == "dora"
+    # The graph carries ONLY the two entities — no synthesized __divisor symbol pollutes
+    # it (that is why the symmetric single-dep divide was chosen over divisor synthesis).
+    assert {s.symbol_id for s in comp.binding_graph.symbols} == {"carl", "dora"}
+
+
+def test_half_as_many_missing_base_refuses() -> None:
+    # "half as many ... as Rod" with no value for Rod -> ungrounded base -> REFUSE.
+    comp = comprehend_quantitative("Sue has half as many pears as Rod. How many pears does Sue have?")
+    assert isinstance(comp, Refusal)

tests/test_quantitative_expr.py

@@ -169,3 +169,61 @@ def test_scalar_only_guard_is_load_bearing() -> None:
     assert proof.operation_kind == "multiply"
     # But the projection REFUSES the same shape — the boundary that keeps wrong=0.
     assert to_relation("c", Mul(Symbol("a"), Symbol("b"))) is None
+
+
+# --------------------------------------------------------------------------- #
+# PR-6c — the divisive comparative (Div), the divisor twin of Mul
+# --------------------------------------------------------------------------- #
+
+
+def test_div_serialization_and_derivations() -> None:
+    from generate.quantitative_expr import Div
+
+    d = Div(Symbol("carl"), Literal(2))
+    assert to_canonical_string(d) == "carl / 2"
+    assert dependencies(d) == frozenset({"carl"})  # the literal divisor is NOT a dep
+    assert operation_kind(d) == "divide"
+    assert to_relation("dora", d) == {
+        "kind": "divide_by", "entity": "dora", "ref": "carl", "divisor": 2,
+    }
+
+
+def test_div_projection_admits_only_symbol_over_literal() -> None:
+    """``Div(Symbol, Literal)`` is the ONLY shape that projects to ``divide_by``; every
+    other ``Div`` shape REFUSES (``to_relation`` → None) — the divisor-only twin of the
+    scalar-only Mul contract.
+
+    Meaningful-fail: a ``Div(Symbol, Symbol)`` is a quantity-over-quantity ratio (the
+    rate-divide family), NOT a divide-by-dimensionless-literal; projecting it as
+    ``divide_by`` would fabricate a divisor. These asserts fail the moment that guard is
+    loosened.
+    """
+    from generate.quantitative_expr import Div
+
+    # The one admitted shape.
+    assert to_relation("dora", Div(Symbol("carl"), Literal(2))) == {
+        "kind": "divide_by", "entity": "dora", "ref": "carl", "divisor": 2,
+    }
+    # Quantity over quantity (a ratio), not a dimensionless divide → refuse.
+    assert to_relation("dora", Div(Symbol("a"), Symbol("b"))) is None
+    # Commuted (literal dividend) → refuse.
+    assert to_relation("dora", Div(Literal(8), Symbol("a"))) is None
+    # Compound divisor → refuse.
+    assert to_relation("dora", Div(Symbol("a"), Add(Symbol("b"), Literal(1)))) is None
+    # A bare literal quotient carries no symbol to reference → refuse.
+    assert to_relation("dora", Div(Literal(8), Literal(2))) is None
+
+
+def test_div_is_symmetric_with_mul_in_the_ir() -> None:
+    """``Div`` and ``Mul`` are structural twins: single-symbol dep, dimensionless literal
+    operand, the operand is never a dependency. This symmetry is what lets the reader
+    build BOTH uniformly (``deps = dependencies(expr)``) without a per-op special case.
+    """
+    from generate.quantitative_expr import Div, Mul
+
+    mul = Mul(Symbol("anna"), Literal(2))
+    div = Div(Symbol("carl"), Literal(2))
+    assert dependencies(mul) == frozenset({"anna"})
+    assert dependencies(div) == frozenset({"carl"})  # identical shape: literal not a dep
+    assert operation_kind(mul) == "multiply"
+    assert operation_kind(div) == "divide"

tests/test_setup_oracle.py

@@ -152,19 +152,21 @@ def test_reader_units_read_from_the_binding_graph() -> None:
 # --------------------------------------------------------------------------- #
 
 
-def test_r1_multiplicative_supported_rest_refused_wrong_zero() -> None:
+def test_r1_comparative_supported_rest_refused_wrong_zero() -> None:
     r = run_r1()
     assert r["total"] == 10
-    # THE invariant through the first capability slice: NO R1 case is misread. Adding the
+    # THE invariant through every capability slice: NO R1 case is misread. Each frame
-    # multiplicative frame turned refusals into correct readings without any setup_wrong.
+    # turns refusals into correct readings without ever producing a setup_wrong.
     assert r["setup_wrong"] == 0
-    # The multiplicative frame (PR-5c) reads "twice as many" (r1-01) and the multi-step
-    # chain whose middle step is "N times as many" (r1-05); the rest stay safe refusals.
     by_id = {d["id"]: d["outcome"] for d in r["details"]}
+    # Multiplicative frame (PR-5c): "twice as many" (r1-01) + the multi-step chain whose
+    # middle step is "N times as many" (r1-05).
     assert by_id["r1-01-twice"] == "correct"
     assert by_id["r1-05-chain"] == "correct"
-    assert r["setup_correct"] == 2
+    # Divisive frame (PR-6c): "half as many" (r1-02).
-    assert r["setup_refused"] == 8
+    assert by_id["r1-02-half"] == "correct"
+    assert r["setup_correct"] == 3
+    assert r["setup_refused"] == 7
     # No detail is ever WRONG, and every non-correct one is a typed refusal.
     for d in r["details"]:
         assert d["outcome"] in ("correct", "refused")
@@ -209,12 +211,82 @@ def test_r1_answer_lane_scores_only_setup_correct_fixtures() -> None:
     assert r["setup_wrong"] == 0
     assert r["wrong"] == 0
     assert r["gold_error"] == 0
-    assert r["correct"] == 2
+    assert r["correct"] == 3
-    assert r["refused"] == 8
+    assert r["refused"] == 7
     by_id = {d["id"]: d for d in r["details"]}
     assert by_id["r1-01-twice"] == {"id": "r1-01-twice", "outcome": "correct", "answer": 12}
+    assert by_id["r1-02-half"] == {"id": "r1-02-half", "outcome": "correct", "answer": 4}
     assert by_id["r1-05-chain"] == {"id": "r1-05-chain", "outcome": "correct", "answer": 14}
     for fixture_id, detail in by_id.items():
-        if fixture_id not in {"r1-01-twice", "r1-05-chain"}:
+        if fixture_id not in {"r1-01-twice", "r1-02-half", "r1-05-chain"}:
             assert detail["outcome"] == "refused"
             assert detail.get("reason")
+
+
+# --------------------------------------------------------------------------- #
+# PR-6c — off-serving answer oracle support for divide_by ("half as many")
+# --------------------------------------------------------------------------- #
+
+
+def test_oracle_computes_divide_by_exact() -> None:
+    assert oracle_answer(
+        [
+            {"kind": "fact", "entity": "carl", "value": 8},
+            {"kind": "divide_by", "entity": "dora", "ref": "carl", "divisor": 2},
+        ],
+        {"entity": "dora"},
+    ) == 4
+
+
+def test_oracle_refuses_non_exact_division() -> None:
+    """The wrong=0 boundary of the divisive frame: a non-exact division REFUSES rather
+    than flooring to a wrong integer. ``7 // 2 == 3`` would be WRONG; the oracle raises.
+
+    Meaningful-fail: if the ``base % divisor != 0`` guard were dropped, this would return
+    3 (a fabricated answer) instead of raising — the assert flips from pass to fail.
+    """
+    with pytest.raises(OracleError):
+        oracle_answer(
+            [
+                {"kind": "fact", "entity": "xio", "value": 7},
+                {"kind": "divide_by", "entity": "yon", "ref": "xio", "divisor": 2},
+            ],
+            {"entity": "yon"},
+        )
+
+
+def test_oracle_rejects_bad_divisor_and_forward_ref() -> None:
+    """The full ``divide_by`` refusal contract — every bad-divisor / unresolved-base class
+    raises ``OracleError`` (never a ZeroDivisionError, never a silent float/floor)."""
+    base = {"kind": "fact", "entity": "carl", "value": 8}
+
+    def _bad_divisor(divisor: object) -> None:
+        with pytest.raises(OracleError):
+            oracle_answer(
+                [base, {"kind": "divide_by", "entity": "dora", "ref": "carl", "divisor": divisor}],
+                {"entity": "dora"},
+            )
+
+    _bad_divisor(0.5)   # non-integer (fractional < 1)
+    _bad_divisor(1.5)   # non-integer (fractional > 1)
+    _bad_divisor(0)     # zero divisor — never ZeroDivisionError
+    _bad_divisor(True)  # bool is not an admissible int divisor (isinstance(True, int) is True)
+    # Forward reference to an unresolved base → refuse.
+    with pytest.raises(OracleError):
+        oracle_answer(
+            [{"kind": "divide_by", "entity": "dora", "ref": "carl", "divisor": 2}],
+            {"entity": "dora"},
+        )
+
+
+def test_oracle_divide_by_one_is_identity() -> None:
+    """``divisor=1`` is intentionally ALLOWED: base / 1 = base, exact. The reader never
+    constructs it (``_DIVISOR_WORDS`` only maps 'half'→2), but the oracle's grammar admits
+    it mathematically. Pinned so the choice stays deliberate, not accidental."""
+    assert oracle_answer(
+        [
+            {"kind": "fact", "entity": "carl", "value": 8},
+            {"kind": "divide_by", "entity": "dora", "ref": "carl", "divisor": 1},
+        ],
+        {"entity": "dora"},
+    ) == 8