Derive reduction parameter contracts and bound ILP encodings

.claude/CLAUDE.md

@@ -149,7 +149,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",
@@ -159,11 +159,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 must target the most specific applicable registered variant: `ILP<bool>` for binary variables, `ILP<i64, i64, Bounded>` for explicit finite integer domains, and general `ILP<i64>` otherwise. Supply finite 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. The independent `bounds` dimension defaults to `general`; register additional concrete variants only when a reduction needs them.
 - `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)"`)
@@ -182,7 +183,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 registers witness/config reductions; aggregate value mappings register through `#[aggregate_reduction]` / `register_aggregate_reduction!` (see Key Patterns); Turing edges (generated by `register_decision_variant!`) and metadata-only edges without an executor use a manual `ReductionEntry`
+- `#[reduction]` requires one uniform or mixed `transform` declaration and registers witness/config reductions; aggregate value mappings register through `#[aggregate_reduction]` / `register_aggregate_reduction!` (see Key Patterns); Turing edges (generated by `register_decision_variant!`) and metadata-only edges without an executor use a manual `ReductionEntry`
 - `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
@@ -316,8 +317,9 @@ The complexity string represents the **worst-case time complexity of the best kn
 
 ### Reduction Parameter Relation (`#[reduction(transform = exact|upper_bound {...})]`)
 Parameter expressions describe how target problem parameters relate to source problem parameters. To verify correctness:
-1. Read the `reduce_to()` implementation and count the actual output sizes
+1. Derive parameter bounds from every construction block in `reduce_to()`, including early returns, skipped rows, duplicate terms, and target normalization. Use a simple proved upper bound by default; declare equality only when it holds for every accepted input.
 2. Check that each field (e.g., `num_vertices`, `num_edges`, `num_sets`) matches the constructed target problem
 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`). Reuse canonical examples and existing behavior tests to check the derived expressions; passing examples supplement the derivation, never establish its correctness. Metadata-only rules have no executable size check and must be identified separately.

.claude/skills/how-to-code/SKILL.md

@@ -79,7 +79,7 @@ Traits and helpers: `src/rules/traits.rs`, `src/rules/test_helpers.rs`, `src/rul
      (composed extractors delegate to the first direct decoder).
    - `#[reduction(transform = exact { .. })]`, `upper_bound { .. }`, or `unavailable { .. }`, with an
      auxiliary `unavailable = { param = "reason" }` block for unrepresentable target parameters.
-     Every target parameter appears exactly once. There is no `overhead =` form.
+     Every target parameter appears exactly once. Mixed accuracy uses `transform = { exact { .. }, upper_bound { .. }, unavailable { .. } }`. Derive bounds by counting each construction block, including normalization and early returns; use equality only when guaranteed across the accepted domain. There is no `overhead =` form.
    - `reduce_to(&self) -> Result<Self::Result, ReductionError>`; wrap target construction failures
      with `Self::target_construction(e)`, never stringify.
    - Aggregate value mapping: `#[crate::aggregate_reduction] impl AggregateReductionResult` on the
@@ -92,7 +92,7 @@ Traits and helpers: `src/rules/traits.rs`, `src/rules/test_helpers.rs`, `src/rul
    don't duplicate endpoints.
 4. Tests in `src/unit_tests/rules/<source>_<target>.rs`: `test_<source>_to_<target>_closed_loop`
    (use `assert_*_round_trip_*` from `test_helpers.rs`), an infeasible instance, target structure
-   and parameter counts vs the transform, and one test per malformed representation the decoder
+   and parameter counts vs the transform (reuse existing inputs; the shared executable-rule check lives in `src/unit_tests/parameter_formula_validation.rs`), and one test per malformed representation the decoder
    rejects (zero/multiple one-hot bits, duplicate permutation entries, ...). Aggregate edges: test
    `extract_value` against `BruteForce::solve` on both sides.
 5. Paper `reduction-rule` entry — how-to-write-manual (adapt the how-to-verify proof, don't rewrite).

.claude/skills/how-to-verify/SKILL.md

@@ -56,7 +56,7 @@ per (n, m) where full enumeration is infeasible). Seven sections, none empty:
 1. symbolic (sympy) check of every overhead formula — "trivial" is no excuse;
 2. exhaustive forward + backward: source feasible ⇔ target feasible (optimum preserved);
 3. extraction from every feasible target witness (the most skipped section);
-4. measured target size vs formula;
+4. measured target size vs formula; first derive each bound from the construction, covering branches, omitted rows, and coefficient normalization; equality requires a full-domain argument, not agreement on examples;
 5. structural well-formedness of the target (gadget invariants, no degenerate cases);
 6. YES example reproduced number-for-number;
 7. NO example reproduced, both sides infeasible.