Commit graph

4 commits

Author SHA1 Message Date
Shay
0951d80e04 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).
2026-06-06 20:18:39 -07:00
Shay
c2b97f40bf test(comprehension): prove the scalar-multiply contract (PR-6a)
The multiplicative comparative frame (PR-5c) admits exactly one shape —
Mul(Symbol, Literal), a unit-bearing symbol times a dimensionless integer
(count × scalar = count). That contract was held by OMISSION: to_relation's
`case _: return None` refused every other Mul shape, but no test would fail
if the guard were loosened, and no doc stated where the guarantee lives.

This makes the obligation meaningfully-failing (CLAUDE.md Schema-Defined
Proof Obligations), with no runtime logic change:

- test_mul_projection_admits_only_symbol_times_literal — Mul(Symbol, Symbol)
  (a count×count product), a commuted factor, and compound factors all REFUSE
  (to_relation → None). Verified to go red when a Mul(Symbol, Symbol) projection
  arm is injected.
- test_literal_factor_is_dimensionless_by_construction — Literal has exactly
  one field (value); a unit-bearing literal multiplication is unrepresentable,
  not merely unchecked.
- test_scalar_only_guard_is_load_bearing — check_admissibility's `multiply`
  dispatch products operand units generally (count×count → count², no refusal),
  so it would NOT catch the masquerade. The projection arm is the sole boundary.

Docstrings on Mul and to_relation now state the scalar-only contract and that
it is enforced at the projection boundary, not in the dimensional checker.

Gates unchanged: setup-oracle 15-case 15/0/0 and R1 2/0/8 (setup_wrong=0);
77 expr/admissibility/reader/setup-oracle tests + 56 architectural invariants
green. No serving path touched.
2026-06-06 17:42:22 -07:00
Shay
e9cbe65d77 feat(comprehension): the multiplicative comparative frame — first R1 capability (PR-5c)
The first capability slice on the R1 arc, gated by the setup-oracle: turn the
"twice / N times as many" reading from REFUSED into a correct setup, without a single
misread. Builds on the typed IR (PR-4) and the R1 gold (PR-5b).

- IR: a Mul(symbol, literal-factor) node — to_canonical_string "ref * factor",
  operation_kind "multiply", dependencies {ref}, to_relation -> times_as_many. The
  product keeps the symbol's unit (count * scalar = count), admitted by the REAL
  check_admissibility multiply path (the literal factor is dimensionless, not a dep).
- Reader: a multiplicative template "Y has <factor> as many <unit> as X" (factor word:
  twice/double/triple/quadruple) and "Y has <N> times as many <unit> as X", checked
  BEFORE the digit gate (the factor may be a word). 'half' (a /2) is deliberately
  deferred — divide-by-literal is a separate admissibility path.
- setup-oracle: relation_signature now canonicalizes times_as_many.

Setup-oracle R1 result: 2 setup_correct (r1-01 twice; r1-05 the multi-step chain
ivy/jon=3*ivy/kim=jon+2), 0 setup_WRONG, 8 setup_refused. Every hard negative stays a
safe refusal: missing-base (Rosa ungrounded), ambiguous referent, distractor, inverse,
partition, 'altogether'/'in total' phrasings, and 'half' (divide). wrong=0 held through
the first capability addition.

Gates green: setup-oracle R1 setup_wrong=0; 15-case setup gate 15/15 setup_wrong=0;
relational_metric answer lane 15/15 wrong=0; binding-graph admissibility + realize +
architectural invariants + chat-runtime + pipeline (122+). No serving path touched (this
reader feeds the relational_metric / setup-oracle lanes, not the candidate-graph serving).
2026-06-06 17:29:23 -07:00
Shay
06450928c9 refactor(comprehension): typed expression IR as the source of meaning (PR-4)
Internal hygiene + future-proofing. No serving path, no new capability — the 15-case
reader is structurally cleaner and the projection no longer recovers meaning by
re-parsing a string.

- New generate/quantitative_expr.py: a typed Expr IR (Literal/Symbol/Add/Sub/SumOf) with
  to_canonical_string (BYTE-IDENTICAL to the legacy "ref + delta" / "ref - delta" / "a + b"
  format), dependencies, operation_kind, and to_relation (the structured projection).
- The reader builds the Expr per equation as the SOURCE OF MEANING; rhs_canonical,
  dependencies, and operation_kind are all DERIVED from it (BoundEquation stays a string —
  the binding-graph's deliberate decoupling layer is untouched). QuantComprehension carries
  the IR as equation_exprs.
- to_relational_metric reads the IR via to_relation — the rhs_canonical string-reparse is
  GONE. An unhandled equation shape refuses (None).
- The dead _rhs string builder is removed.

Gates held: relational_metric answer lane 15/15 wrong=0; setup-oracle 15/15 setup_wrong=0;
malformed-target refusals intact; realize-binding-graph + architectural invariants green
(95). rhs_canonical is byte-identical, so the binding-graph + downstream hashes are
unchanged. No model change.

This is the foundation PR-5's R1 frames build on — structured equations, not string parsing
— and only after independent R1 gold is hand-authored.
2026-06-06 16:57:53 -07:00