core/docs/analysis/solver-operation-coverage.md

Solver Operation Coverage Audit

Status: Proposed analysis draft. No serving behavior is changed. This is a read-only structural audit to de-risk ADR-0174 Phase 5b / Phase-4-style composition work. Verdicts below are code-reading conclusions only; they must be verified in the Claude lane with executable solver/binding-graph cases before any promotion claim.

Scope

Read surfaces:

• generate/math_problem_graph.py
• generate/math_solver.py
• generate/binding_graph/{model,adapter,admissibility,allocation,question_target,units}.py
• ADR-0116, ADR-0117, ADR-0132, ADR-0133, ADR-0134, ADR-0135
• Skimmed ADR-0174 Phase 5b and ADR-0203/0204/0205 to confirm current composition/proof-DAG framing.

Important correction to the relay: the current solver/graph vocabulary is not only {add, subtract, transfer, multiply, divide}. MathProblemGraph and math_solver both include the eight operation kinds:

add, subtract, transfer, multiply, divide,
apply_rate, compare_additive, compare_multiplicative

ADR-0174 Phase 5b states the same: the solver is already waiting for these operations; the gap is reader -> injector -> Operation front-end wiring plus composition.

Existing Operation Substrate

Surface	Evidence	Consequence
Closed operation vocabulary	generate/math_problem_graph.py defines VALID_OPERATION_KINDS with eight kinds.	New arithmetic verbs are not needed for ordinary multiply/divide/rate/comparison chains.
Pack-bound solver dispatch	generate/math_solver.py maps all eight kinds to en_arithmetic_v1 lemmas before solving.	Missing pack lemmas fail loudly; no hidden operation fallback.
Stateful solver semantics	_apply mutates (actor, unit) terminal state for add, subtract, transfer, multiply, divide; _apply_rate produces numerator-unit state from denominator-unit state; comparisons derive an actor state from a reference actor.	The solver is good at forward state trajectories, but weak at keeping multiple same-unit derived intermediates alive under one actor.
Unknown shape	Unknown(entity, unit) resolves either terminal state for one entity or total-across all entities with that unit.	Target questions that ask for a missing operand, number of iterations, or intermediate state are not represented by Unknown alone.
Binding-graph equation/data model	BoundEquation(operation_kind=...), BoundUnknown(question_form=...), semantic roles include rate, duration, difference, ratio.	The graph can name richer forms than the solver's final Unknown, but current adapter still comes from existing MathProblemGraph operation chains.
Unit admissibility	check_admissibility covers additive, multiplicative, divide, apply_rate, and comparison kinds.	Dimensional proofs exist for the current eight operation kinds; new node types would need explicit admissibility rules.
Question-target binding	infer_question_form recognizes ratio, difference, rate, total, and count from operation kinds touching the unknown.	It can label answer form, but it does not solve inverse targets or select intermediate operation indices yet.
Acyclicity	ADR-0203 adds circular_dependency refusal to the shared binding-graph constructor.	Any new equation/intermediate-node extension must remain a DAG, not a cyclic algebra system hidden inside the graph.

Phase-4 Target Chains

Target chain	Verdict	Existing operations that can carry it	What is missing / risk
Multi-step rate-sum	Expressible via composition for straight-line rate applications and sums. Piecewise tariffs/conditionals need scoped selection before admission.	apply_rate computes X/Y * Y -> X; add/subtract can aggregate generated same-unit totals. Binding admissibility has an apply_rate rule requiring one rate dep plus one duration/count dep.	The reader must emit the base duration/count quantities, rate hypotheses, and sum operations without clobbering unrelated same-unit state. Piecewise tariffs such as "$50/day or $500/14 days" need a tariff/choice scope or explicit branch-disagreement gate; that is a binding/composition problem, not a missing arithmetic verb.
Ratio chain	Expressible via composition for forward ratio chains. Inverse ratio equations need a target/equation extension.	compare_multiplicative supports "actor = factor * reference"; multiply/divide support scalar transformations; infer_question_form maps touching compare_multiplicative to ratio.	Forward chains like A, B = 2A, C = 1/2(A+B) can be represented if the reader emits the right reference actors and order. Inverse forms such as "ducks are 10 more than 4x chickens; ducks = 150; find total birds" require solving for an unknown reference, not just applying a forward operation. That needs equation/target solving or a new binding node shape, not a new ratio operation kind.
Accumulate-against-target	Needs new binding-graph target/equation capability; not expressible as a fixed existing operation chain in the current solver.	add, subtract, multiply, divide, and apply_rate can express the arithmetic once the iteration count or missing operand is known.	The current solver consumes a fully specified graph in source order, then resolves terminal Unknown(entity, unit). It cannot represent "after how many weeks", "how many cups to sell to reach profit", or "how long to make back cost" as an unknown operand/iteration count. This needs a first-class target-slot/equation node or bounded inverse solver with refusal/disagreement, plus proof that no cyclic dependency is introduced.
Percent/fraction mutation	Mostly expressible via composition for forward mutations; needs intermediate-symbol/scope support for same-unit derived amounts and event subsets.	Percent/fraction values can be scalar multiply/divide factors, with add/subtract for mutation and compare_multiplicative for relative quantities. Binding admissibility already covers multiply/divide dimensions.	Some cases are safe forward mutations ("eat 75% of a pan", "lose half"). Others require original and derived same-unit quantities to coexist, e.g. principal plus interest, insured vs uninsured portions, operating cost as percent of startup cost. The current solver overwrites (actor, unit) for multiply/divide and apply_rate, so these need derived intermediate symbols/event scopes or separate binding nodes. A new percent operation kind is not structurally necessary; a new scoped intermediate/equation representation may be.

Structural Verdict

Phase 4/5b is mostly not blocked by missing arithmetic operation kinds. The current operation vocabulary already covers the primitive arithmetic field: addition/subtraction/transfer, scalar multiply/divide, rate application, and additive/multiplicative comparison.

The real scope risk is representation:

• Can the reader emit a chain of typed operations from scattered clauses while preserving all grounded quantities?
• Can the graph retain intermediate derived quantities when they share the same actor/unit as their source?
• Can a question bind to a missing operand, iteration count, or intermediate state instead of only terminal Unknown(entity, unit)?
• Can inverse/equation targets be solved under a disagreement rule and the ADR-0203 acyclicity invariant?

That makes the likely build a binding-target / intermediate-symbol / derivation-composer extension, not a broad new solver primitive pack.

Chain-Specific Notes

Multi-step rate-sum

apply_rate is first-class: the solver's _apply_rate reads the actor's denominator-unit state and writes numerator-unit state. The binding-graph adapter synthesizes a rate symbol with composite unit <num>_per_<denom>, and admissibility checks that the denominator cancels. Therefore simple rate-sum is expressible as:

duration/count fact -> apply_rate -> produced total
produced totals -> add/subtract -> final total

The unsafe part is not the operation. It is branch selection and scope: overtime, tariffs, and "including today" require deciding which rate applies to which event subset.

Ratio chain

compare_multiplicative already gives a forward ratio operation. It refuses when the reference actor has no quantity or multiple ambiguous units, which is the right wrong=0 boundary. Binding target can label ratio-form questions.

The gap is inverse ratio. Current Operation is directional: it mutates the actor from a known reference. If the reference is the unknown and the actor is given, the solver has no inverse-equation mode.

Accumulate-against-target

This is the clearest "needs new graph shape" target. A terminal state solver can answer "what is the total after N weeks"; it cannot answer "what N reaches total T" unless N is already present as a quantity and a divide operation has been materialized by the reader. A safe implementation needs a target slot that names the missing operand/iteration count and an admissibility/disagreement rule for the inverse derivation.

Percent/fraction mutation

Percent/fraction does not need a new arithmetic verb. It needs:

• scalar extraction (75% -> 0.75, 1/4 -> 0.25);
• complement derivation when the text says "covers 80%" but the cost asks for the uncovered part;
• event/subset scoping ("after the first appointment", "subsequent visits");
• intermediate symbols when original principal/cost and derived interest/cost must both remain available.

The binding graph is the natural home for these intermediates because it already has BoundEquation, dependency sets, unit proofs, question forms, and acyclicity checks.

Open Questions for the Claude Lane

• Does apply_rate overwriting (actor, numerator_unit) create a concrete hazard in rate-sum cases where the actor already holds money? If yes, the build needs derived result symbols before promotion.
• Should inverse target solving be introduced as a new BoundUnknown form, a new BoundEquation operation kind, or a separate proof/derivation rule over existing equations?
• Can forward ratio chains be admitted through compare_multiplicative without widening the parser's reference-actor ambiguity beyond the existing refusal discipline?
• What is the smallest executable probe set that distinguishes "new operation kind required" from "same operation, new intermediate symbol required" for percent/fraction mutations?
• When proof-DAG consumers and math binding graphs share SemanticSymbolicBindingGraph, should proposition-specific operation kinds remain isolated from math admissibility, or should the admissibility dispatcher split into math/proof entrypoints before more equation kinds are added?