Make derivable reduction parameters exact

.claude/CLAUDE.md

@@ -179,7 +179,7 @@ Max<V>, Min<V>, Sum<W>, Or, And, Extremum<V>, ExtremumSense
 - `NumericSize` supertrait bundles common numeric bounds (`Clone + Default + PartialOrd + Num + Zero + Bounded + AddAssign + 'static`)
 
 ### Parameter Relations
-Each reduction declares one rule-level parameter relation using the `Expr` AST in `src/expr.rs`. The `transform` declaration is required:
+Each reduction declares explicit per-field parameter relations using the `Expr` AST in `src/expr.rs`. The `transform` declaration is required:
 ```rust
 #[reduction(transform = upper_bound {
     num_vertices = "num_vertices + num_clauses",
@@ -189,11 +189,12 @@ impl ReduceTo<Target> for Source { ... }
 ```
 - Expression strings are parsed at compile time by a Pratt parser in the proc macro crate
 - Variable names are validated against the source problem's canonical parameter schema
-- Use `transform = exact { ... }` when every formula is an equality and `transform = upper_bound { ... }` when every formula is only an upper bound. One expression block cannot mix relations.
+- Use `transform = exact { ... }` when every formula is an equality and `transform = upper_bound { ... }` when every formula is only an upper bound. For mixed accuracy, use `transform = { exact { ... }, upper_bound { ... }, unavailable { ... } }`. Every formula RHS uses only registered source parameters; derive target relationships and substitute source expressions before declaring them.
 - Use `transform = unavailable { ... }` when no formula is representable, or an auxiliary `unavailable = { ... }` block for omitted target parameters.
 - Every target parameter must appear exactly once as a formula or as unavailable with a non-empty reason.
-- `ParameterTransform` evaluates and composes formulas with exact rational and arbitrary-precision integer arithmetic. Unsafe upper-bound composition becomes unavailable; it never performs budget pruning or path ranking.
+- `ParameterTransform` evaluates and composes formulas with exact rational and arbitrary-precision integer arithmetic. Composition preserves independent fields and their accuracy. An unavailable dependency or unsafe upper-bound substitution makes only the affected field unavailable; it never performs budget pruning or path ranking.
 - Concrete instance parameters come from each endpoint instance's `Problem::parameters()` implementation; `ReductionEntry` stores only the symbolic parameter relation.
+- Rules producing `ILP<i64>` must declare known finite variable domains with `ILP::with_variables`; constraint rows alone do not supply bounds to binary encoding. Bounds on auxiliary variables must preserve feasibility and the optimum. Document genuinely unbounded variables rather than inventing a cutoff.
 - `VariantEntry` has both a complexity string and compiled `complexity_eval_fn` — same pattern
 - Expressions support: constants, variables, `+`, `-`, `*`, `/`, `^`, `exp()`, `log()`, `sqrt()`, `factorial()`
 - Complexity strings must use **concrete numeric values only** (e.g., `"2^(2.372 * num_vertices / 3)"`, not `"2^(omega * num_vertices / 3)"`)
@@ -212,7 +213,7 @@ Reduction graph nodes use variant key-value pairs from `Problem::variant()`:
 - Same-name variant relations are explicit `#[reduction]` registrations
 - Each primitive reduction is determined by the exact `(source_variant, target_variant)` endpoint pair
 - Reduction edges carry `EdgeCapabilities { witness, aggregate, turing }`; graph search defaults to witness mode, aggregate mode is available through `ReductionMode::Aggregate`, and Turing (multi-query) mode via `ReductionMode::Turing`
-- `#[reduction]` requires one `transform = exact`, `transform = upper_bound`, or `transform = unavailable` declaration and currently registers witness/config reductions; aggregate-only and Turing edges require manual `ReductionEntry` registration
+- `#[reduction]` requires one uniform or mixed `transform` declaration and currently registers witness/config reductions; aggregate-only and Turing edges require manual `ReductionEntry` registration
 - `Decision<P> → P` supports both mappings: compare the exact optimum to the bound, and recover a witness only if it meets the bound. `P → Decision<P>` is a Turing edge (binary search over decision bound).
 
 ### Extension Points
@@ -351,3 +352,4 @@ Parameter expressions describe how target problem parameters relate to source pr
 3. Watch for common errors: universe elements mismatch (edge indices vs vertex indices), worst-case edge counts in intersection graphs (quadratic, not linear), constant factors in circuit constructions
 4. Test with concrete small instances: construct a source problem, run the reduction, and compare target parameters against the formula
 5. Ensure there is only one primitive reduction registration for each exact source/target variant pair; wrap shared helpers instead of registering duplicate endpoints
+6. Every new rule's `exact` and `upper_bound` fields must be covered by `src/unit_tests/parameter_formula_validation.rs`: evaluate each formula on a valid source instance and compare it with measured target parameters (equal for `exact`, predicted ≥ measured for `upper_bound`). Provide a canonical example or registered generator so the shared test can exercise the rule; add targeted boundary cases when needed.

.claude/skills/add-rule/SKILL.md

@@ -168,6 +168,8 @@ Add to `src/rules/mod.rs`:
 
 Create `src/unit_tests/rules/<source>_<target>.rs`:
 
+Follow the [reduction parameter testing requirement](../../CLAUDE.md#reduction-parameter-relation): the shared test must cover every declared `exact` or `upper_bound` field using a valid source instance.
+
 **Required: closed-loop test** (`test_<source>_to_<target>_closed_loop`):
 ```rust
 // 1. Create source problem instance

docs/src/design.md

@@ -423,10 +423,10 @@ All path-finding operates on **exact variant nodes**. Use `ReductionGraph::varia
 | `find_all_paths(src, src_var, dst, dst_var)` | All simple paths | Enumerate every route |
 | `compose_path_parameter_transform(path)` | Symbolic composition | Compose each rule's exact or upper-bound parameter relation while preserving its promise |
 
-A rule has one relation for all of its formulas: either an exact equality or an upper
-bound. Composition keeps exact formulas exact only when every step is exact; every other
-combination is an upper bound. Concrete-instance measurement remains a separate execution
-API.
+Each formula has its own relation: exact equality or upper bound. Composition preserves
+exactness when the formula and its required inputs are exact. Bounded inputs require sound
+upper-bound substitution. Unavailable fields affect only formulas that depend on them;
+independent formulas survive. Concrete-instance measurement remains a separate execution API.
 
 **Example:** Finding a path from `MIS{KingsSubgraph, i64}` to `VC{SimpleGraph, i64}`:
 
@@ -450,8 +450,10 @@ The returned `ReductionChain` stores each intermediate reduction and extracts th
 <details>
 <summary>Parameter contracts</summary>
 
-Each reduction declares one relation for all represented target-parameter fields and may mark
-other fields unavailable with a reason. The `#[reduction]` macro parses every formula into
+Each reduction classifies every target parameter exactly once as exact, upper bound, or
+unavailable with a reason. Every formula uses only registered source parameters on its RHS.
+Target structural relationships may justify a formula, but source expressions must be
+substituted before registration; there is no automatic model-level inference. The `#[reduction]` macro parses every formula into
 the canonical `Expr` DAG at compile time:
 
 ```rust,ignore
@@ -467,6 +469,28 @@ unavailable = {
 impl ReduceTo<Target> for Source { ... }
 ```
 
+Rules can mix accuracy explicitly while existing uniform declarations remain supported:
+
+```rust,ignore
+#[reduction(transform = {
+    exact { num_vars = "num_vars" },
+    upper_bound { num_quadratic_terms = "num_vars * (num_vars - 1) / 2" },
+})]
+impl ReduceTo<Decision<QUBO<i64>>> for KSatisfiability<K2> { ... }
+```
+
+Here both RHS expressions refer to the SAT source's `num_vars`.
+Likewise, an ILP's canonical constraint matrix has at most variables times constraints
+nonzeros. If a rule predicts those dimensions by source expressions `f` and `g`, it can
+explicitly declare `num_nonzeros <= f * g`. Such structural bounds remain valid when
+coefficients cancel; exact sparsity can still require additional source information.
+
+`ReductionParameterDeclarations::fields` stores `(name, relation, expression)` triples.
+Use `ParameterTransform::relation(field)` to inspect a formula's accuracy and
+`unavailable(field)` for a composition failure and its upstream cause. The uniform
+`ParameterTransform::new` constructor remains available; `from_fields` accepts mixed relations.
+CLI contract JSON stores `relation` within each formula entry in `fields`.
+
 `ParameterTransform` uses exact rational and arbitrary-precision integer arithmetic. Exact
 relations must evaluate to non-negative integers, while upper-bound results round rational
 values upward. Missing fields, negative or non-integral exact results, division by zero,
@@ -485,7 +509,7 @@ first fully expanded and like monomials are combined; terms with non-positive co
 are then removed before substitution. For example, `m <= n^2` followed by `k = 10 - m`
 produces the sound bound `k <= 10`, while
 `e' = v(v - 1)/2 - e` produces `e' <= v^2/2`. A non-polynomial downstream formula cannot
-propagate symbolic upper bounds and reports an error. Projection to `Growth` is a separate descriptive terminal operation used for
+propagate symbolic upper bounds and makes that field unavailable, preserving the other fields. Projection to `Growth` is a separate descriptive terminal operation used for
 Big-O display; it does not rank or filter paths.
 
 </details>

problemreductions-cli/src/commands/graph.rs

@@ -2,6 +2,7 @@ use crate::dispatch::{load_problem, read_input, ProblemJson};
 use crate::output::OutputConfig;
 use crate::problem_name::{aliases_for, parse_problem_spec, resolve_problem_ref};
 use anyhow::Result;
+use problemreductions::parameters::ParameterRelation;
 use problemreductions::registry::collect_schemas;
 use problemreductions::registry::ProblemCategory;
 use problemreductions::rules::{ExecutedPath, ReductionGraph, ReductionPath, TraversalFlow};
@@ -584,13 +585,9 @@ fn strongest_contract_fields(
     let mut fields = BTreeMap::new();
     if let Some(transform) = contract.transform() {
         for (field, expression) in transform.expressions() {
-            let relation = match transform.relation() {
-                problemreductions::parameters::ParameterRelation::Exact => {
-                    StrongestContractRelation::Exact(expression)
-                }
-                problemreductions::parameters::ParameterRelation::UpperBound => {
-                    StrongestContractRelation::UpperBound(expression)
-                }
+            let relation = match transform.relation(field).expect("declared formula") {
+                ParameterRelation::Exact => StrongestContractRelation::Exact(expression),
+                ParameterRelation::UpperBound => StrongestContractRelation::UpperBound(expression),
             };
             fields.insert(field, relation);
         }
@@ -670,11 +667,11 @@ pub(crate) fn parameter_contract_to_json(
 ) -> serde_json::Value {
     match contract {
         Ok(contract) => serde_json::json!({
-            "relation": contract.transform().map(|transform| transform.relation()),
             "fields": contract.transform().map(|transform| transform.expressions().map(|(field, expression)| {
                 serde_json::json!({
                     "field": field,
                     "formula": expression.to_string(),
+                    "relation": transform.relation(field),
                     "big_o": big_o_of(expression),
                 })
             }).collect::<Vec<_>>()).unwrap_or_default(),
@@ -731,88 +728,50 @@ struct PreparedParameterField {
     relation: PreparedParameterRelation,
 }
 
-fn terminal_parameter_contract(
-    graph: &ReductionGraph,
-    path: &ReductionPath,
-) -> Option<problemreductions::rules::ReductionParameterContract> {
-    path.steps
-        .windows(2)
-        .last()
-        .and_then(|pair| {
-            graph.find_entry(
-                &pair[0].name,
-                &pair[0].variant,
-                &pair[1].name,
-                &pair[1].variant,
-            )
-        })
-        .and_then(|entry| entry.parameter_contract.ok())
-}
-
 fn prepare_overall_parameters(
     graph: &ReductionGraph,
     path: &ReductionPath,
 ) -> Vec<PreparedParameterField> {
-    let Some(target) = path.target() else {
+    let Some(target) = path.steps.last() else {
         return Vec::new();
     };
     let composed = graph.compose_path_parameter_transform(path);
-    let terminal_contract = terminal_parameter_contract(graph, path);
-
-    graph
-        .parameter_names(target)
-        .into_iter()
-        .map(|field| {
-            let expression = composed
-                .as_ref()
-                .ok()
-                .and_then(|transform| transform.as_ref())
-                .and_then(|transform| {
-                    transform
-                        .get(&field)
-                        .map(|expression| (transform.relation(), expression))
-                });
-            let relation = if let Some((relation, expression)) = expression {
-                match relation {
-                    problemreductions::parameters::ParameterRelation::Exact => {
-                        PreparedParameterRelation::Exact(expression.to_string())
-                    }
-                    problemreductions::parameters::ParameterRelation::UpperBound => {
-                        PreparedParameterRelation::UpperBound(expression.to_string())
+    let fields = problemreductions::registry::find_variant_entry(&target.name, &target.variant)
+        .map(|entry| entry.parameter_names())
+        .unwrap_or_default();
+    fields
+        .iter()
+        .map(|&field| {
+            let relation = match &composed {
+                Ok(Some(transform)) => {
+                    if let Some(expression) = transform.get(field) {
+                        match transform.relation(field).expect("declared formula") {
+                            ParameterRelation::Exact => {
+                                PreparedParameterRelation::Exact(expression.to_string())
+                            }
+                            ParameterRelation::UpperBound => {
+                                PreparedParameterRelation::UpperBound(expression.to_string())
+                            }
+                        }
+                    } else {
+                        let reason = transform
+                            .unavailable(field)
+                            .map(ToString::to_string)
+                            .unwrap_or_else(|| {
+                                format!("no symbolic parameter relation is registered for target field {field}")
+                            });
+                        PreparedParameterRelation::Unavailable(reason)
                     }
                 }
-            } else if let Some(unavailable) = terminal_contract.as_ref().and_then(|contract| {
-                contract
-                    .unavailable()
-                    .iter()
-                    .find(|unavailable| unavailable.field == field)
-            }) {
-                PreparedParameterRelation::Unavailable(unavailable.reason.to_string())
-            } else if terminal_contract
-                .as_ref()
-                .and_then(|contract| contract.transform())
-                .is_some_and(|transform| transform.get(&field).is_some())
-            {
-                PreparedParameterRelation::Unavailable(match &composed {
-                    Err(error) => error.to_string(),
-                    Ok(_) => {
-                        format!(
-                            "no composed parameter relation is available for target field {field}"
-                        )
-                    }
-                })
-            } else {
-                let reason = match &composed {
-                    Err(error) => error.to_string(),
-                    Ok(_) => {
-                        format!(
-                            "no symbolic parameter relation is registered for target field {field}"
-                        )
-                    }
-                };
-                PreparedParameterRelation::Unavailable(reason)
+                Err(error) => PreparedParameterRelation::Unavailable(error.to_string()),
+                Ok(None) => PreparedParameterRelation::Unavailable(format!(
+                    "no composed parameter relation is available for target field {field}"
+                )),
             };
-            PreparedParameterField { field, relation }
+            PreparedParameterField {
+                field: field.to_string(),
+                relation,
+            }
         })
         .collect()
 }

problemreductions-cli/src/test_support.rs

@@ -399,7 +399,7 @@ problemreductions::inventory::submit! {
         source_variant_fn: AggregateValueSource::variant,
         target_variant_fn: AggregateValueTarget::variant,
         parameter_declarations_fn: || ReductionParameterDeclarations {
-            relation: None,
+
             fields: vec![],
             unavailable: vec![problemreductions::rules::registry::UnavailableParameterField {
                 field: "num_values",
@@ -430,7 +430,7 @@ problemreductions::inventory::submit! {
         source_variant_fn: AggregateValueSource::variant,
         target_variant_fn: ILP::<bool>::variant,
         parameter_declarations_fn: || ReductionParameterDeclarations {
-            relation: None,
+
             fields: vec![],
             unavailable: vec![
                 problemreductions::rules::registry::UnavailableParameterField {

problemreductions-cli/tests/cli_tests.rs

@@ -5553,6 +5553,51 @@ fn test_path_overall_unavailable_is_reported_per_field_without_internal_modes()
     assert!(overall.get("bound_composition_error").is_none());
 }
 
+#[test]
+fn test_path_preserves_exact_variables_and_bounded_quadratic_terms() {
+    for target in ["DecisionQUBO", "QUBO"] {
+        let output = pred()
+            .args([
+                "path",
+                "KSatisfiability/K2",
+                target,
+                "--limit",
+                "1",
+                "--json",
+            ])
+            .output()
+            .unwrap();
+        assert!(
+            output.status.success(),
+            "{}",
+            String::from_utf8_lossy(&output.stderr)
+        );
+        let envelope: serde_json::Value = serde_json::from_slice(&output.stdout).unwrap();
+        let fields = envelope["paths"][0]["overall_parameters"]["fields"]
+            .as_array()
+            .unwrap();
+        let relations = fields
+            .iter()
+            .map(|field| {
+                (
+                    field["field"].as_str().unwrap(),
+                    field["relation"].as_str().unwrap(),
+                )
+            })
+            .collect::<std::collections::BTreeMap<_, _>>();
+        // The reduction preserves variables; distinct off-diagonal pairs bound
+        // quadratic terms even when contributions cancel.
+        assert_eq!(
+            relations,
+            std::collections::BTreeMap::from([
+                ("num_vars", "exact"),
+                ("num_quadratic_terms", "upper_bound"),
+            ]),
+            "prediction relations for {target}"
+        );
+    }
+}
+
 #[test]
 fn test_path_overall_preserves_unavailable_fields_alongside_exact_fields() {
     let output = pred()