diff --git a/docs/paper/reductions.typ b/docs/paper/reductions.typ
index 8f413459c..c06aca6f3 100644
--- a/docs/paper/reductions.typ
+++ b/docs/paper/reductions.typ
@@ -12050,7 +12050,9 @@ the displayed rule, extracted from the corresponding `pred path` entry.
 
       Encode $x_i+M_i in [0,2M_i]$ with powers of two and one capped final weight. If $W$ maps the resulting bits to coefficient offsets, $G=B^top B$, $h=B^top bold(t)$, and $bold(ell)=-bold(M)$, then
       $ norm(B bold(x)-bold(t))_2^2 = bold(z)^top(W^top G W)bold(z) + 2 bold(z)^top W^top(G bold(ell)-h) + "const". $
-      The constant is dropped. The exact bit count depends on concrete entries, so its symbolic transform is unavailable.
+      The constant is dropped.
+
+      _Size bound._ Let $h >= 1$ be the maximum bit length of the absolute entries of $B$ and $bold(t)$. Each cofactor has magnitude at most $(n-1)! 2^(h(n-1))$, and $C_j < (m+1)2^h$. Thus $M_i < n! (m+1)2^(h n)$. Using $log_2(n!) <= n^2$ and $log_2(m+1) <= m$ for $m >= 1$, each coefficient needs at most $n^2+m+n h+3$ bits. The registered bounds are therefore $V=n(n^2+m+n h+3)$ QUBO variables and $V^2$ quadratic terms. A rank-zero basis gives zero variables. The magnitude parameter describes only the source entries, independently of this encoding.
 
       _Correctness._ ($arrow.r.double$) Every bit vector decodes inside the derived box and has QUBO value equal to its CVP squared distance minus one common constant, so a QUBO minimizer is best within the box. ($arrow.l.double$) The derived box contains a global CVP minimizer, and every point in the box has an exact-range encoding. Therefore the best encoded point is globally optimal for CVP.
 
@@ -12299,7 +12301,7 @@ where $P$ is a penalty weight large enough that any constraint violation costs m
 
       _Solution extraction._ Validate the target configuration once and require squared distance exactly $n$ through the formal aggregate certificate. Return the first $n$ coefficients as Boolean selections, accepting one as true; the remaining coefficients are the specified carries. A larger optimal squared distance proves NO and provides no source witness.
 
-      _Representation._ The target has $2n+b$ coordinates and $n+b-1$ basis columns. Since bit length is not a registered Subset Sum parameter, the symbolic relations are marked unavailable with that reason. Dimensions and the total dense basis byte count are checked before allocation. The threshold and squared-distance evaluation use checked `i64` arithmetic; overflow is an error, not a NO certificate. The solver uses exact rational sphere-enumeration bounds; runtime limitations are separate from the mathematical equivalence.
+      _Representation._ The target has $2n+b$ coordinates and $n+b-1$ basis columns. The existing source parameter `max_numeric_magnitude_bits` is exactly $b$, so both dimensions are predicted exactly. Target basis entries have magnitude at most two and target coordinates are Boolean, giving target `max_numeric_magnitude_bits` at most two; this supplies the numerical parameter needed by the subsequent CVP-to-QUBO rule. Dimensions and the total dense basis byte count are checked before allocation. The threshold and squared-distance evaluation use checked `i64` arithmetic; overflow is an error, not a NO certificate. The solver uses exact rational sphere-enumeration bounds; runtime limitations are separate from the mathematical equivalence.
     ]
   ]
 }
@@ -12313,7 +12315,7 @@ where $P$ is a penalty weight large enough that any constraint violation costs m
 
   Write the extended rows as $A' z=b$, where the first $n$ bits of $z$ are $x$ and the remaining bits are row-specific slack. Set $P=1+sum_i |d_i|+sum_k |b_k|$, $C=P sum_k b_k^2$, $L=sum_i min(d_i,0)$, and $U=sum_i max(d_i,0)$. The upper-triangular QUBO matrix has diagonal $Q_(i i)=d_i+P sum_k ((a'_(k i))^2-2 b_k a'_(k i))$ and off-diagonal $Q_(i j)=2P sum_k a'_(k i)a'_(k j)$ for $i<j$; extend $d$ by zeros on slack coordinates. Its energy satisfies
   $ E(z)+C=d^top x+P sum_k (a'_k z-b_k)^2. $
-  Store the energy interval $[L-C,U-C]$, the constant $C$, and the source sense in the reduction result. Dimensions, matrix arithmetic, constant and interval endpoints are checked before use. The target has $n+sum_k S_k$ variables; its registered overhead remains unavailable because the source parameter vector omits coefficient magnitudes and right-hand sides.
+  Store the energy interval $[L-C,U-C]$, the constant $C$, and the source sense in the reduction result. Dimensions, matrix arithmetic, constant and interval endpoints are checked before use. The target has $n+sum_k S_k$ variables. With $m$ source constraints and source parameter $h$ = `max_constraint_magnitude_bits`, the registered upper bounds are $V=n+m(n+h)$ variables and $V^2$ quadratic terms.
 
   _Forward direction._ Every feasible source assignment has a slack extension satisfying every row, with $E+C=d^top x$ in $[L,U]$. Hence its target energy lies in the stored interval. For positive slack range the powers-of-two encoding represents the exact required slack; for zero range no slack is needed.
 
@@ -12377,6 +12379,8 @@ where $P$ is a penalty weight large enough that any constraint violation costs m
   $ C = floor(S / 2). $
   Every feasible knapsack solution is therefore a subset of the original elements, and because $w_i = v_i$, its objective value equals the same subset sum.
 
+  _Parameter propagation._ If each source size has at most $h$ bits, their sum has at most $h+n$ bits; halving cannot increase this. The target `capacity_bits` is therefore at most $h+n$, including zero capacity. Composing with the Knapsack-to-QUBO rule yields at most $2n+h$ variables and $(2n+h)^2$ quadratic terms. The raw capacity field remains unavailable because these predictions need only its bit length.
+
   _Correctness._ ($arrow.r.double$) If the Partition instance is satisfiable, some subset $A'$ has sum $S / 2$. In particular $S$ is even, so $C = S / 2$, and selecting exactly the corresponding knapsack items is feasible with value $S / 2$. No feasible knapsack solution can have value larger than $C$, because value equals weight for every item and total weight is bounded by $C$. Thus the knapsack optimum is exactly $S / 2$. ($arrow.l.double$) If the knapsack optimum is $S / 2$, then the optimum is an integer and hence $S$ must be even. The selected items have total value $S / 2$, so they also have total weight $S / 2$ because $w_i = v_i$ itemwise. Those items therefore form a subset of the original multiset whose complement has the same sum, giving a valid balanced partition.
 
   _Solution extraction._ Return the same binary selection vector on the original elements: item $i$ is selected in the knapsack witness if and only if element $i$ belongs to the extracted partition subset.
@@ -12510,6 +12514,8 @@ where $P$ is a penalty weight large enough that any constraint violation costs m
   where $bold(z) = (x_0, dots, x_(n-1), s_0, dots, s_(B-1))$ and $P = 1 + sum_i v_i$. Expanding the quadratic penalty using $z_k^2 = z_k$ (binary):
   $ Q_(k k) = P a_k^2 - 2 P C a_k - [k < n] v_k, quad Q_(i j) = 2 P a_i a_j quad (i < j) $
 
+  _Size bound._ Let $b$ be the source parameter `capacity_bits`, the binary digit count of $C$ with a minimum of one for zero. The encoding uses exactly $b$ slack bits, so the QUBO has exactly $n+b$ variables and at most $(n+b)^2$ quadratic terms.
+
   _Correctness._ ($arrow.r.double$) If $bold(x)^*$ is a feasible knapsack solution with value $V^*$, then there exist slack values $bold(s)^*$ satisfying the equality constraint (encoding $C - sum w_i x_i^*$ in binary), so $f(bold(z)^*) = -V^*$. ($arrow.l.double$) If the equality constraint is violated, the penalty $(sum a_k z_k - C)^2 gt.eq 1$ contributes at least $P > sum_i v_i$ to the objective. Since all values are nonnegative, every feasible assignment has objective in the range $[-sum_i v_i, 0]$, so that penalty exceeds the entire feasible value range. Among feasible assignments (penalty zero), $f$ reduces to $-sum v_i x_i$, minimized at the knapsack optimum.
 
   _Solution extraction._ Discard slack variables: return $bold(z)[0..n]$.
@@ -13004,6 +13010,8 @@ where $P$ is a penalty weight large enough that any constraint violation costs m
 ][
   _Construction._ Given a SAT instance $phi$ with $n$ variables and $m$ clauses, introduce a sentinel variable $s$ (variable index $n + 1$). For each clause $C_j = (ell_1 or dots or ell_k)$, construct the NAE clause $C'_j = (ell_1, dots, ell_k, s)$. The target NAE-SAT instance has $n + 1$ variables and $m$ clauses.
 
+  _Size bound._ An empty source clause is represented by the contradictory NAE clause $(s,s)$. If the source has $L$ literal occurrences and $m$ clauses, the target has at most $L+2m$ literals. The sum of within-clause literal-pair counts is bounded by $(L+2m)^2$.
+
   _Correctness._ ($arrow.r.double$) Given a satisfying assignment $bold(x)$ for $phi$, set $s = 0$. Each clause $C_j$ has at least one true literal $ell_i$ and the false sentinel $s = 0$, so $C'_j$ has both a true and a false literal, satisfying the NAE constraint. ($arrow.l.double$) Given a satisfying NAE assignment $(bold(x), s)$: if $s = 0$, each clause has at least one true literal (or else all literals in $C'_j$ would be false, including $s$, violating NAE); if $s = 1$, complement the entire assignment --- the complemented sentinel is $0$, and each complemented clause still has at least one true literal because the original NAE clause had at least one false non-sentinel literal.
 
   _Solution extraction._ If the sentinel $s = 0$, return the first $n$ variables. If $s = 1$, return the complement of the first $n$ variables.
@@ -13044,6 +13052,8 @@ where $P$ is a penalty weight large enough that any constraint violation costs m
   $
   using the 2-clause NOT gadget, the 3-clause AND/OR gadgets, and the 4-clause XOR gadget. If the simplified right-hand side becomes a variable or auxiliary variable $z_e$, add $(overline(o_i) or z_e)$ and $(o_i or overline(z_e))$ for every output $o_i$. If it simplifies to a constant, add the unit clause $o_i$ or $overline(o_i)$ accordingly. Repeat this independently for every assignment in the circuit.
 
+  _Size bound._ Let $N$ count all source expression nodes and $O$ all assignment outputs. Replacing multi-input gates by binary gates introduces at most $2N$ gates, each with at most four clauses of three literals. Output equalities add at most $2O$ clauses of two literals. Thus the target has at most $n+2N$ variables, $8N+2O$ clauses, and $24N+4O$ literals, including constant expressions and assignments without outputs.
+
   _Correctness._ ($arrow.r.double$) Let $sigma$ be a satisfying CircuitSAT assignment. Set every auxiliary variable $v_alpha$ to the truth value of the corresponding subexpression $alpha$ under $sigma$. Each Tseitin gadget is then satisfied because its output variable matches the gate semantics, and every output-equivalence or unit clause holds because $sigma$ already makes each circuit assignment $o_1, dots, o_t = e$ true. Hence the CNF is satisfiable. ($arrow.l.double$) Let $tau$ satisfy the constructed CNF. Every Tseitin gadget forces its auxiliary variable to equal the truth value of its subexpression, so the root variable $z_e$ equals the value of $e$. The output-equivalence clauses therefore force every output $o_i$ to equal $e$, and unit clauses force the required constants. Restricting $tau$ to the named circuit variables yields an assignment satisfying every original circuit equation.
 
   _Solution extraction._ Return the values of the named circuit variables and discard the auxiliary Tseitin variables.
@@ -13136,7 +13146,7 @@ where $P$ is a penalty weight large enough that any constraint violation costs m
 
   _Solution extraction._ Evaluate the target certificate once and reject it unless all equations hold. Read off factor bits $p = sum_i p_i 2^(i-1)$ and $q = sum_j q_j 2^(j-1)$, then return $(min(p,q), max(p,q))$. The source requires $m <= n$. Sorting preserves the asymmetric bounds: if inputs are exchanged, the new smaller factor is below the old first factor, while both inputs fit the larger width.
 
-  _Size and arithmetic._ Product width and assignment capacity are checked before allocation. At most $6 m n + 2(m+n) + 2$ assignments and $6 m n + 2(m+n) + 1$ variables are generated. Factors and products use exact arbitrary-precision integers; the circuit enforces bit arithmetic without floating-point conversions. The cell and output assignments use only the existing Boolean expression API.
+  _Size and arithmetic._ Product width and assignment capacity are checked before allocation. At most $6 m n + 2(m+n) + 2$ assignments and $6 m n + 2(m+n) + 1$ variables are generated. Factors and products use exact arbitrary-precision integers; the circuit enforces bit arithmetic without floating-point conversions. Each assignment has one output and at most five expression nodes, so the assignment bound also bounds output count, and five times that bound covers expression nodes. The cell and output assignments use only the existing Boolean expression API.
 
 ]
 
@@ -13647,7 +13657,7 @@ The following reductions to Integer Linear Programming are straightforward formu
     *Uniqueness:* The fixture stores one canonical optimal witness. For this instance the optimum is unique: items $\{#fmt-values(ks_ilp_selected)\}$ are the only feasible choice achieving value #ks_ilp_sel_value.
   ],
 )[
-  A 0-1 Knapsack instance is already a binary Integer Linear Program @papadimitriou-steiglitz1982: each item-selection bit becomes a binary variable, the capacity condition is a single linear inequality, and the value objective is linear. The reduction preserves the number of decision variables exactly, producing an ILP with $n$ variables and one constraint.
+  A 0-1 Knapsack instance is already a binary Integer Linear Program @papadimitriou-steiglitz1982: each item-selection bit becomes a binary variable, the capacity condition is a single linear inequality, and the value objective is linear. The reduction preserves the number of decision variables exactly, producing an ILP with $n$ variables and at most $n+1$ constraints after fixing oversized items to zero.
 ][
   _Construction._ Given nonnegative weights $w_0, dots, w_(n-1)$, nonnegative values $v_0, dots, v_(n-1)$, and capacity $C$, introduce binary variables $x_0, dots, x_(n-1) in {0,1}$ where $x_i = 1$ iff item $i$ is selected. The ILP is:
   $
@@ -13655,7 +13665,7 @@ The following reductions to Integer Linear Programming are straightforward formu
     "subject to" quad & sum_(i=0)^(n-1) w_i x_i <= C \
     & x_i in {0, 1} quad forall i in {0, dots, n - 1}.
   $
-  The target therefore has exactly $n$ variables and one linear constraint.
+  The implementation omits every weight greater than $C$ from the capacity row and adds $x_i=0$ for that item. This preserves feasibility and gives exactly $n$ variables and at most $n+1$ constraints. Every constraint coefficient and right-hand side has magnitude at most $max(C,1)$, so `capacity_bits` bounds the target `max_constraint_magnitude_bits`.
 
   _Correctness._ ($arrow.r.double$) Any feasible knapsack solution $bold(x)$ satisfies $sum_i w_i x_i <= C$, so the same binary vector is feasible for the ILP and attains identical objective value $sum_i v_i x_i$. ($arrow.l.double$) Any feasible binary ILP solution selects exactly the items with $x_i = 1$; the single inequality guarantees the chosen set fits in the knapsack, and the ILP objective equals the knapsack value. Therefore optimal solutions correspond one-to-one and preserve the optimum value.
 
@@ -13716,6 +13726,8 @@ The following reductions to Integer Linear Programming are straightforward formu
 
   _Correctness._ ($arrow.r.double$) Any feasible Integer Knapsack multiplicity vector $bold(c)$ already satisfies $sum_i s_i c_i <= B$, and every source multiplicity also satisfies $c_i <= floor.l B / s_i floor.r$, so the same vector is feasible for the ILP and attains exactly the same objective value $sum_i v_i c_i$. ($arrow.l.double$) Any feasible ILP solution satisfies the same capacity inequality and the same per-item multiplicity bounds, so it is a valid Integer Knapsack witness with identical total value. Therefore optimal solutions correspond one-to-one and preserve the optimum value.
 
+  _Numeric magnitude._ Items with $s_i>B$ have multiplicity fixed to zero and are omitted from the capacity row. All constraint magnitudes and variable bounds are therefore at most $max(B,1)$. The source `capacity_bits`, defined as the binary digit count of $B$ with a minimum of one, bounds the target `max_constraint_magnitude_bits`.
+
   _Solution extraction._ Identity: return the ILP variable vector $bold(c)$ as the Integer Knapsack multiplicities.
 ]
 
@@ -14443,6 +14455,8 @@ The following reductions to Integer Linear Programming are straightforward formu
 
   Create one Betweenness element $a_u$ for each $u in U'$ and one distinguished pole $p$. For every size-2 subset ${u, v} in cal(C)'$, add triple $(a_u, p, a_v)$. For every size-3 subset ${u, v, w} in cal(C)'$, introduce a fresh auxiliary element $d_(u,v,w)$ and add triples $(a_u, d_(u,v,w), a_v)$ and $(d_(u,v,w), p, a_w)$.
 
+  _Size bound._ Write $u$ for the source universe size and $s$ for its number of subsets. After deduplication, each subset has at most $u$ elements and undergoes at most $u$ decomposition steps, each adding two elements and two subsets. Hence the normalized universe has at most $u+2s u$ elements and at most $s(2u+1)$ subsets. Adding one pole and at most one auxiliary per normalized subset gives at most $u+1+s(4u+1)$ elements; at most two triples per subset gives $2s(2u+1)$ triples.
+
   _Correctness._ The normalization identity preserves splittability: a coloring splits ${s_1, dots, s_k}$ if and only if it can be extended to fresh elements $y^+, y^-$ so that ${s_1, s_2, y^+}$, ${y^+, y^-}$, and ${y^-, s_3, dots, s_k}$ are all non-monochromatic. Thus it suffices to reason about normalized subsets.
 
   ($arrow.r.double$) Let $chi: U' -> {0, 1}$ split every subset of $cal(C)'$. Place all $a_u$ with $chi(u) = 0$ to the left of $p$ and all $a_u$ with $chi(u) = 1$ to the right. For a size-2 subset ${u, v}$, non-monochromaticity gives $chi(u) != chi(v)$, so $p$ lies between $a_u$ and $a_v$, satisfying $(a_u, p, a_v)$. For a size-3 subset ${u, v, w}$, not all three colors are equal. If $u$ and $v$ lie on the same side of $p$, then $w$ lies on the opposite side; place $d_(u,v,w)$ between $a_u$ and $a_v$ on their shared side. If $u$ and $v$ lie on opposite sides of $p$, place $d_(u,v,w)$ between them on the side opposite $a_w$. In both cases $(a_u, d_(u,v,w), a_v)$ and $(d_(u,v,w), p, a_w)$ hold.
@@ -15319,6 +15333,8 @@ The following reductions to Integer Linear Programming are straightforward formu
 #reduction-rule("OpenShopScheduling", "ILP")[
   Binary ordering variables and integer start times encode the disjunctive non-overlap constraints for both machines and jobs; the makespan is the minimized objective.
 ][
+  _Numeric magnitude._ The source `schedule_horizon_bits` is the binary digit count of the total processing time $M$, with a minimum of one. Start times and makespan have explicit domains $[0,M]$. All constraint magnitudes are at most $max(M,1)$, so this parameter bounds the target `max_constraint_magnitude_bits`.
+
   _Construction._ Let $M = sum_(j,i) p(j,i)$ be the big-$M$ constant (an upper bound on the makespan). For each pair $j < k$ and each machine $i$, let $x_{j k i} in {0,1}$ with $x_{j k i} = 1$ iff job $j$ precedes job $k$ on machine $i$. For each job $j$ and pair of machines $i < i'$, let $y_{j i i'} in {0,1}$ with $y_{j i i'} = 1$ iff machine $i$ is processed before machine $i'$ for job $j$. Let $s_{j,i} in ZZ_{>=0}$ be the start time of job $j$ on machine $i$, and $C$ be the integer makespan variable. The ILP is:
   $
     min quad & C \
@@ -15352,7 +15368,7 @@ The following reductions to Integer Linear Programming are straightforward formu
 )[
   Impose the decision bound on the open-shop makespan variable. The optimization formulation gains one constraint and no variables.
 ][
-  _Construction._ For bound $B$, use the OpenShopScheduling-to-ILP construction above, add $C <= B$, and replace the objective with zero.
+  _Construction._ For bound $B$, use the OpenShopScheduling-to-ILP construction above, add $C <= min(M,max(-1,B))$, and replace the objective with zero. Clipping preserves feasibility because $0 <= C <= M$, and keeps the target `max_constraint_magnitude_bits` bounded by the source `schedule_horizon_bits` independently of $B$.
 
   _Correctness._ ($arrow.r.double$) A schedule of makespan at most $B$ gives feasible ordering variables and start times, with $C$ equal to its makespan. The existing horizon bounds can be met by removing unnecessary idle time. ($arrow.l.double$) Every feasible target assignment decodes to a schedule whose makespan is at most $C <= B$. Thus target feasibility is equivalent to the source YES answer; no optimum needs to be computed.
 
@@ -18327,6 +18343,8 @@ The following table shows concrete target-variable counts for example instances,
   $
   Set the knapsack capacity to $B$. The target therefore has the same number of items as the source has elements.
 
+  _Numeric magnitude._ The source `max_numeric_magnitude_bits` includes the target sum $B$ and therefore bounds the Integer Knapsack `capacity_bits`. Raw `capacity` remains unavailable in the symbolic contract; its bit-length bound suffices for the downstream ILP size predictions.
+
   _Correctness._ ($arrow.r.double$) If $I subset.eq {1, dots, n}$ satisfies $sum_(i in I) a_i = B$, define multiplicities $c_i = 1$ for $i in I$ and $c_i = 0$ otherwise. Then
   $
     sum_i c_i s_i = sum_(i in I) a_i = B <= B
@@ -18904,9 +18922,11 @@ The following table shows concrete target-variable counts for example instances,
     *Multiplicity:* The fixture stores one canonical witness.
   ],
 )[
-  This $O(n^2 + m)$ reduction @stockmeyer1973 assigns each variable $x_i$ a distinct prime $p_i >= 5$, encoding TRUE as residue 1 and FALSE as residue 2 modulo $p_i$. All other residues are forbidden. Each clause is encoded via CRT as a single forbidden residue class modulo the product of its variables' primes. A satisfying assignment exists iff some integer avoids all forbidden classes.
+  This polynomial-time reduction @stockmeyer1973 assigns each variable $x_i$ a distinct prime $p_i >= 3$, encoding TRUE as residue 1 and FALSE as residue 2 modulo $p_i$. All other residues are forbidden. Each clause is encoded via CRT as a single forbidden residue class modulo the product of its variables' primes. A satisfying assignment exists iff some integer avoids all forbidden classes.
 ][
-  _Construction._ Given 3-SAT with $n$ variables and $m$ clauses, assign primes $p_1, dots, p_n >= 5$. For each variable $x_i$, forbid residues ${0, 3, 4, dots, p_i - 1}$ modulo $p_i$, leaving only ${1, 2}$. For each clause $C_j$ over variables $x_(i_1), x_(i_2), x_(i_3)$, compute the falsifying residue $r_k in {1, 2}$ for each literal and use CRT to find $R_j$ with $R_j equiv r_k mod p_(i_k)$ for $k = 1,2,3$. Forbid $R_j$ modulo $M_j = p_(i_1) p_(i_2) p_(i_3)$.
+  _Construction._ Given 3-SAT with $n$ variables and $m$ clauses, assign primes $p_1, dots, p_n >= 3$. For each variable $x_i$, forbid residues ${0, 3, 4, dots, p_i - 1}$ modulo $p_i$, leaving only ${1, 2}$. For each clause $C_j$ over variables $x_(i_1), x_(i_2), x_(i_3)$, compute the falsifying residue $r_k in {1, 2}$ for each literal and use CRT to find $R_j$ with $R_j equiv r_k mod p_(i_k)$ for $k = 1,2,3$. Forbid $R_j$ modulo $M_j = p_(i_1) p_(i_2) p_(i_3)$.
+
+  _Size bound._ There are $sum_(i=1)^n (p_i-2)+m$ forbidden pairs, where $p_i$ is the $i$th odd prime. For the ordinary $k$th prime $q_k$, the standard estimate $q_k < k(ln k+ln ln k)$ for $k >= 6$ @axler2019, together with the first five primes, implies $q_k <= 2k^2$ for every $k >= 1$. Consequently $p_i=q_(i+1) <= 2(n+1)^2$ and $2n(n+1)^2+m$ bounds the pair count.
 
   _Correctness._ ($arrow.r.double$) A satisfying assignment $tau$ defines residues $r_i in {1,2}$ per variable. By CRT, some integer $x$ has these residues. It avoids all variable-forbidden classes and all clause-forbidden classes (since at least one literal is true, the residue triple differs from the falsifying triple). ($arrow.l.double$) Any feasible $x$ has $x mod p_i in {1,2}$ for all $i$. Define $tau(x_i) = "TRUE"$ if residue 1, FALSE if 2. If a clause were false, $x$ would match its forbidden CRT class -- contradiction.
 
@@ -19042,6 +19062,8 @@ The following table shows concrete target-variable counts for example instances,
 ][
   _Construction._ The source is a nonempty list of positive integers $a_1,...,a_k$, with $S=sum_j a_j$. Set $Q=floor(S/2)$. Use three machines, one job $(a_j,a_j,a_j)$ per element, and one special job $(Q,Q,Q)$. Let $D=3Q$.
 
+  _Numeric magnitude._ Let $h$ be the source `max_numeric_magnitude_bits`. The sum $S$ needs at most $h+k$ bits, and the target schedule horizon is $3S+3Q <= 6S$. Thus `schedule_horizon_bits` is at most $h+k+3$. Raw `schedule_horizon` remains unavailable; its bit-length bound is sufficient to compose polynomial size bounds through bounded ILP and QUBO.
+
   _Forward correctness._ Given a balanced partition into groups $A,B$, each group has total size $Q$ and $S=2Q$. Divide time into three phases $[r Q,(r+1)Q)$, $r=0,1,2$. In phase $r$, run the special job on machine $r$, all jobs of $A$ consecutively on machine $(r+1) mod 3$, and all jobs of $B$ consecutively on machine $(r+2) mod 3$. Each group exactly fills its phase, each element job has one operation per phase, and the machine rotation processes it once on every machine. This is a feasible nonpreemptive schedule of makespan $D$.
 
   _Backward correctness._ Every schedule has makespan at least $3Q$ by the special job's total processing time, and at least $S+Q$ by each machine's load. If a feasible schedule attains $D$, these bounds give $S+Q<=3Q$; together with $S>=2Q$ this forces $S=2Q$. Since the source sizes are positive, $Q>0$. The special job must run without gaps and start its three operations at $0,Q,2Q$, in some machine order. Select the unique machine on which it starts at $Q$. Element operations on that machine fit before $Q$ or after $2Q$, each interval having capacity $Q$. Their total load is $2Q$, so the jobs completing by $Q$ have total size exactly $Q$ and define a balanced partition. It is the middle machine that supplies these two separate intervals, not an arbitrary fixed machine.
diff --git a/docs/paper/references.bib b/docs/paper/references.bib
index 369d309f0..a65104787 100644
--- a/docs/paper/references.bib
+++ b/docs/paper/references.bib
@@ -2321,3 +2321,14 @@ @techreport{mandersAdleman1976
   month = {November},
   url = {https://digicoll.lib.berkeley.edu/record/134974/files/ERL-m-615.pdf}
 }
+
+@article{axler2019,
+  author = {Axler, Christian},
+  title = {New Estimates for the nth Prime Number},
+  journal = {Journal of Integer Sequences},
+  volume = {22},
+  number = {4},
+  pages = {Article 19.4.2},
+  year = {2019},
+  url = {https://www.maths.tcd.ie/EMIS/journals/JIS/VOL22/Axler/axler17.pdf}
+}
diff --git a/docs/src/design.md b/docs/src/design.md
index f6e0717bb..5b58f73ff 100644
--- a/docs/src/design.md
+++ b/docs/src/design.md
@@ -495,6 +495,12 @@ magnitudes. New parameters must describe intrinsic source data independently of
 any reduction, and their propagation must be audited on incoming rules. Keep
 model-specific definitions and rule-specific formulas beside their implementations.
 
+Avoid registering synonymous aliases. Arithmetic dependence alone does not make a
+parameter redundant: keep a meaningful derived quantity when its name makes
+formulas clearer or enables useful, sound predictions. Substitute existing
+parameters when doing so preserves clarity. Lack of a current formula consumer
+alone is not a reason to remove a parameter.
+
 `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
diff --git a/problemreductions-cli/tests/cli_tests.rs b/problemreductions-cli/tests/cli_tests.rs
index 5d3b7f9c4..899189d80 100644
--- a/problemreductions-cli/tests/cli_tests.rs
+++ b/problemreductions-cli/tests/cli_tests.rs
@@ -5536,12 +5536,31 @@ fn test_path_set_has_explicit_parameter_information() {
 #[test]
 fn test_path_overall_unavailable_is_reported_per_field_without_internal_modes() {
     let output = pred()
-        .args(["path", "Factoring", "SpinGlass", "--json"])
+        .args([
+            "path",
+            "ThreePartition",
+            "QUBO/i64",
+            "--limit",
+            "2",
+            "--json",
+        ])
         .output()
         .unwrap();
     assert!(output.status.success());
     let envelope: serde_json::Value = serde_json::from_slice(&output.stdout).unwrap();
-    let overall = &envelope["paths"][0]["overall_parameters"];
+    let path = envelope["paths"]
+        .as_array()
+        .unwrap()
+        .iter()
+        .find(|path| {
+            path["path"]
+                .as_array()
+                .unwrap()
+                .iter()
+                .any(|step| step["from"]["name"] == "SequencingWithReleaseTimesAndDeadlines")
+        })
+        .expect("time-indexed scheduling path exists");
+    let overall = &path["overall_parameters"];
     let fields = overall["fields"].as_array().unwrap();
     assert!(!fields.is_empty());
     assert!(fields.iter().all(|field| {
@@ -5601,7 +5620,7 @@ fn test_path_preserves_exact_variables_and_bounded_quadratic_terms() {
 #[test]
 fn test_path_overall_preserves_unavailable_fields_alongside_exact_fields() {
     let output = pred()
-        .args(["path", "BMF", "BicliqueCover", "--limit", "1", "--json"])
+        .args(["path", "Partition", "Knapsack", "--limit", "1", "--json"])
         .output()
         .unwrap();
     assert!(output.status.success());
@@ -5618,10 +5637,8 @@ fn test_path_overall_preserves_unavailable_fields_alongside_exact_fields() {
             )
         })
         .collect::<std::collections::BTreeMap<_, _>>();
-    for field in ["num_vertices", "left_size", "right_size", "rank"] {
-        assert_eq!(relations[field], "exact");
-    }
-    assert_eq!(relations["num_edges"], "unavailable");
+    assert_eq!(relations["num_items"], "exact");
+    assert_eq!(relations["capacity"], "unavailable");
     let unavailable = fields
         .iter()
         .find(|field| field["relation"] == "unavailable")
diff --git a/src/models/algebraic/closest_vector_problem.rs b/src/models/algebraic/closest_vector_problem.rs
index bce15f48f..2153e3a3f 100644
--- a/src/models/algebraic/closest_vector_problem.rs
+++ b/src/models/algebraic/closest_vector_problem.rs
@@ -86,6 +86,13 @@ impl ClosestVectorProblem {
         self.target.len()
     }
 
+    /// Maximum bit length of an absolute basis or target entry, at least one.
+    pub fn max_numeric_magnitude_bits(&self) -> u64 {
+        crate::types::max_numeric_magnitude_bits(
+            self.basis.iter().flatten().chain(&self.target).copied(),
+        )
+    }
+
     /// Integer basis columns.
     pub fn basis(&self) -> &[Vec<i64>] {
         &self.basis
@@ -167,6 +174,7 @@ impl Problem for ClosestVectorProblem {
     crate::problem_parameters![
         ("ambient_dimension", ambient_dimension),
         ("num_basis_vectors", num_basis_vectors),
+        ("max_numeric_magnitude_bits", max_numeric_magnitude_bits),
     ];
 
     fn evaluate(&self, solution: &Self::Solution) -> Result<Min<i64>, EvaluationError> {
diff --git a/src/models/misc/knapsack.rs b/src/models/misc/knapsack.rs
index 91eca16a6..8b7d37150 100644
--- a/src/models/misc/knapsack.rs
+++ b/src/models/misc/knapsack.rs
@@ -132,6 +132,11 @@ impl Knapsack {
         self.capacity
     }
 
+    /// Binary digit count of the capacity, with a minimum of one for zero.
+    pub fn capacity_bits(&self) -> u64 {
+        crate::types::max_numeric_magnitude_bits([self.capacity])
+    }
+
     /// Returns the number of items.
     pub fn num_items(&self) -> usize {
         self.weights.len()
@@ -142,11 +147,7 @@ impl Knapsack {
     /// For positive capacity this is `floor(log2(C)) + 1`; for zero capacity we
     /// keep one slack bit so the encoding shape remains uniform.
     pub fn num_slack_bits(&self) -> usize {
-        if self.capacity == 0 {
-            1
-        } else {
-            self.capacity.ilog2() as usize + 1
-        }
+        usize::try_from(self.capacity_bits()).expect("capacity bit length fits usize")
     }
 }
 
@@ -155,7 +156,11 @@ impl Problem for Knapsack {
     type Solution = Vec<bool>;
     type Value = Max<i64>;
 
-    crate::problem_parameters![("capacity", capacity), ("num_items", num_items),];
+    crate::problem_parameters![
+        ("capacity", capacity),
+        ("capacity_bits", capacity_bits),
+        ("num_items", num_items),
+    ];
 
     fn variant() -> Vec<(&'static str, &'static str)> {
         crate::variant_params![]
diff --git a/src/models/misc/open_shop_scheduling.rs b/src/models/misc/open_shop_scheduling.rs
index a08efa1a7..d3b5062c0 100644
--- a/src/models/misc/open_shop_scheduling.rs
+++ b/src/models/misc/open_shop_scheduling.rs
@@ -189,6 +189,11 @@ impl OpenShopScheduling {
             .expect("processing times must fit the brute-force schedule horizon")
     }
 
+    /// Binary digit count of the schedule horizon, with a minimum of one for zero.
+    pub fn schedule_horizon_bits(&self) -> u64 {
+        crate::types::max_numeric_magnitude_bits([self.schedule_horizon()])
+    }
+
     fn finish_time(
         &self,
         config: &[usize],
@@ -238,6 +243,7 @@ impl Problem for OpenShopScheduling {
         ("num_jobs", num_jobs),
         ("num_machines", num_machines),
         ("schedule_horizon", schedule_horizon),
+        ("schedule_horizon_bits", schedule_horizon_bits),
     ];
 
     fn variant() -> Vec<(&'static str, &'static str)> {
diff --git a/src/models/set/exact_cover_by_3_sets.rs b/src/models/set/exact_cover_by_3_sets.rs
index 43cce38b0..1fc915b31 100644
--- a/src/models/set/exact_cover_by_3_sets.rs
+++ b/src/models/set/exact_cover_by_3_sets.rs
@@ -202,7 +202,6 @@ impl Problem for ExactCoverBy3Sets {
     type Value = crate::types::Or;
 
     crate::problem_parameters![
-        ("num_sets", num_sets),
         ("num_subsets", num_subsets),
         ("universe_size", universe_size),
     ];
diff --git a/src/models/set/integer_knapsack.rs b/src/models/set/integer_knapsack.rs
index 6080cbdff..04be21fc8 100644
--- a/src/models/set/integer_knapsack.rs
+++ b/src/models/set/integer_knapsack.rs
@@ -88,6 +88,11 @@ impl IntegerKnapsack {
         self.capacity
     }
 
+    /// Binary digit count of the capacity, with a minimum of one for zero.
+    pub fn capacity_bits(&self) -> u64 {
+        crate::types::max_numeric_magnitude_bits([self.capacity])
+    }
+
     /// Returns the number of items.
     pub fn num_items(&self) -> usize {
         self.sizes.len()
@@ -99,7 +104,11 @@ impl Problem for IntegerKnapsack {
     type Solution = Vec<usize>;
     type Value = Max<i64>;
 
-    crate::problem_parameters![("capacity", capacity), ("num_items", num_items),];
+    crate::problem_parameters![
+        ("capacity", capacity),
+        ("capacity_bits", capacity_bits),
+        ("num_items", num_items),
+    ];
 
     fn variant() -> Vec<(&'static str, &'static str)> {
         crate::variant_params![]
diff --git a/src/rules/bmf_bicliquecover.rs b/src/rules/bmf_bicliquecover.rs
index 867926684..57908da05 100644
--- a/src/rules/bmf_bicliquecover.rs
+++ b/src/rules/bmf_bicliquecover.rs
@@ -92,17 +92,17 @@ impl ReductionResult for ReductionBMFToBicliqueCover {
     }
 }
 
-#[reduction(
-    transform = exact {
+#[reduction(transform = {
+    exact {
         num_vertices = "rows + cols",
         left_size = "rows",
         right_size = "cols",
         rank = "rank",
     },
-    unavailable = {
-        num_edges = "the number of true matrix entries is not a registered BMF parameter",
-    }
-)]
+    upper_bound {
+        num_edges = "rows * cols",
+    },
+})]
 impl ReduceTo<BicliqueCover> for BMF {
     type Result = ReductionBMFToBicliqueCover;
 
diff --git a/src/rules/circuit_sat.rs b/src/rules/circuit_sat.rs
index 4030b23ca..0bc5657ac 100644
--- a/src/rules/circuit_sat.rs
+++ b/src/rules/circuit_sat.rs
@@ -307,13 +307,11 @@ impl ReductionResult for ReductionCircuitSATToSAT {
 #[crate::aggregate_reduction(identity)]
 impl crate::rules::AggregateReductionResult for ReductionCircuitSATToSAT {}
 
-#[reduction(
-    transform = unavailable {
-        num_vars = "the exact Tseitin variable count is specific to this reduction and is not a CircuitSAT parameter",
-        num_clauses = "the exact Tseitin clause count is specific to this reduction and is not a CircuitSAT parameter",
-            num_literals = "the exact target parameter is not represented by this reduction's symbolic transform",
-}
-)]
+#[reduction(transform = upper_bound {
+    num_vars = "num_variables + 2 * num_expression_nodes",
+    num_clauses = "8 * num_expression_nodes + 2 * num_assignment_outputs",
+    num_literals = "24 * num_expression_nodes + 4 * num_assignment_outputs",
+})]
 impl ReduceTo<Satisfiability> for CircuitSAT {
     type Result = ReductionCircuitSATToSAT;
 
diff --git a/src/rules/closestvectorproblem_qubo.rs b/src/rules/closestvectorproblem_qubo.rs
index 6d8986da3..f29dde9fa 100644
--- a/src/rules/closestvectorproblem_qubo.rs
+++ b/src/rules/closestvectorproblem_qubo.rs
@@ -231,9 +231,11 @@ fn dot(left: &[i64], right: &[i64], operation: &str) -> Result<i64, crate::rules
         })
 }
 
-#[reduction(transform = unavailable {
-    num_vars = "the exact encoding size depends on the concrete basis and target values",
-    num_quadratic_terms = "the number of nonzero products depends on the concrete basis coefficients",
+// Cofactor bounds give at most r^2 + d + r*h + 3 bits per coefficient,
+// where r is the rank, d the ambient dimension, and h the input magnitude bits.
+#[reduction(transform = upper_bound {
+    num_vars = "num_basis_vectors * (num_basis_vectors^2 + ambient_dimension + num_basis_vectors * max_numeric_magnitude_bits + 3)",
+    num_quadratic_terms = "(num_basis_vectors * (num_basis_vectors^2 + ambient_dimension + num_basis_vectors * max_numeric_magnitude_bits + 3))^2",
 })]
 impl ReduceTo<QUBO<i64>> for ClosestVectorProblem {
     type Result = ReductionCVPToQUBO;
diff --git a/src/rules/decisionminimumvertexcover_hamiltoniancircuit.rs b/src/rules/decisionminimumvertexcover_hamiltoniancircuit.rs
index e2cea1103..2c98d97d4 100644
--- a/src/rules/decisionminimumvertexcover_hamiltoniancircuit.rs
+++ b/src/rules/decisionminimumvertexcover_hamiltoniancircuit.rs
@@ -300,12 +300,10 @@ impl crate::rules::AggregateReductionResult
 {
 }
 
-#[reduction(
-    transform = unavailable {
-        num_vertices = "the construction size depends on the decision threshold, which is not a problem parameter",
-        num_edges = "the construction size depends on the decision threshold, which is not a problem parameter",
-    }
-)]
+#[reduction(transform = upper_bound {
+    num_vertices = "num_vertices + 12 * num_edges + 3",
+    num_edges = "(num_vertices + 12 * num_edges + 3)^2",
+})]
 impl ReduceTo<HamiltonianCircuit<SimpleGraph>> for Decision<MinimumVertexCover<SimpleGraph, One>> {
     type Result = ReductionDecisionMinimumVertexCoverToHamiltonianCircuit;
 
diff --git a/src/rules/exactcoverby3sets_algebraicequationsovergf2.rs b/src/rules/exactcoverby3sets_algebraicequationsovergf2.rs
index b177223cf..a397b158f 100644
--- a/src/rules/exactcoverby3sets_algebraicequationsovergf2.rs
+++ b/src/rules/exactcoverby3sets_algebraicequationsovergf2.rs
@@ -38,8 +38,8 @@ impl crate::rules::AggregateReductionResult for ReductionX3CToAlgebraicEquations
 
 #[reduction(
     transform = upper_bound {
-    num_variables = "num_sets",
-    num_equations = "universe_size + 9 * num_sets^2",
+    num_variables = "num_subsets",
+    num_equations = "universe_size + 9 * num_subsets^2",
 })]
 impl ReduceTo<AlgebraicEquationsOverGF2> for ExactCoverBy3Sets {
     type Result = ReductionX3CToAlgebraicEquationsOverGF2;
diff --git a/src/rules/exactcoverby3sets_maximumsetpacking.rs b/src/rules/exactcoverby3sets_maximumsetpacking.rs
index 8aa93e9c5..d1ac3445f 100644
--- a/src/rules/exactcoverby3sets_maximumsetpacking.rs
+++ b/src/rules/exactcoverby3sets_maximumsetpacking.rs
@@ -63,14 +63,14 @@ impl crate::rules::AggregateReductionResult for ReductionXC3SToMaximumSetPacking
     }
 }
 
-#[reduction(
-    transform = exact {
+#[reduction(transform = {
+    exact {
         num_sets = "num_subsets",
     },
-    unavailable = {
-        universe_size = "the exact target parameter is not represented by this reduction's symbolic transform",
-    }
-)]
+    upper_bound {
+        universe_size = "universe_size",
+    },
+})]
 impl ReduceTo<MaximumSetPacking<One>> for ExactCoverBy3Sets {
     type Result = ReductionXC3SToMaximumSetPacking;
 
diff --git a/src/rules/exactcoverby3sets_subsetproduct.rs b/src/rules/exactcoverby3sets_subsetproduct.rs
index 1e902948b..b184b5942 100644
--- a/src/rules/exactcoverby3sets_subsetproduct.rs
+++ b/src/rules/exactcoverby3sets_subsetproduct.rs
@@ -68,7 +68,7 @@ impl crate::rules::AggregateReductionResult for ReductionX3CToSubsetProduct {}
 
 #[reduction(
     transform = exact {
-        num_elements = "num_sets",
+        num_elements = "num_subsets",
     })]
 impl ReduceTo<SubsetProduct> for ExactCoverBy3Sets {
     type Result = ReductionX3CToSubsetProduct;
diff --git a/src/rules/factoring_circuit.rs b/src/rules/factoring_circuit.rs
index ddbe91027..c130d1fe3 100644
--- a/src/rules/factoring_circuit.rs
+++ b/src/rules/factoring_circuit.rs
@@ -214,16 +214,12 @@ fn build_multiplier_cell(
 #[crate::aggregate_reduction(identity)]
 impl crate::rules::AggregateReductionResult for ReductionFactoringToCircuit {}
 
-#[reduction(
-    transform = upper_bound {
-        num_variables = "6 * num_bits_first * num_bits_second + 2 * (num_bits_first + num_bits_second) + 1",
-        num_assignments = "6 * num_bits_first * num_bits_second + 2 * (num_bits_first + num_bits_second) + 2",
-    },
-    unavailable = {
-        num_assignment_outputs = "the exact target parameter is not represented by this reduction's symbolic transform",
-        num_expression_nodes = "the exact target parameter is not represented by this reduction's symbolic transform",
-    }
-)]
+#[reduction(transform = upper_bound {
+    num_variables = "6 * num_bits_first * num_bits_second + 2 * (num_bits_first + num_bits_second) + 1",
+    num_assignments = "6 * num_bits_first * num_bits_second + 2 * (num_bits_first + num_bits_second) + 2",
+    num_assignment_outputs = "6 * num_bits_first * num_bits_second + 2 * (num_bits_first + num_bits_second) + 2",
+    num_expression_nodes = "5 * (6 * num_bits_first * num_bits_second + 2 * (num_bits_first + num_bits_second) + 2)",
+})]
 impl ReduceTo<CircuitSAT> for Factoring {
     type Result = ReductionFactoringToCircuit;
 
diff --git a/src/rules/integerknapsack_ilp.rs b/src/rules/integerknapsack_ilp.rs
index 5ee902be1..5c6918b9a 100644
--- a/src/rules/integerknapsack_ilp.rs
+++ b/src/rules/integerknapsack_ilp.rs
@@ -38,7 +38,7 @@ impl ReductionResult for ReductionIntegerKnapsackToILP {
         num_constraints = "num_items + 1",
     },
     upper_bound {
-        max_constraint_magnitude_bits = "capacity + 1",
+        max_constraint_magnitude_bits = "capacity_bits",
         num_nonzeros = "2 * num_items",
     },
 })]
diff --git a/src/rules/kclique_balancedcompletebipartitesubgraph.rs b/src/rules/kclique_balancedcompletebipartitesubgraph.rs
index af52a2233..b3cb09b81 100644
--- a/src/rules/kclique_balancedcompletebipartitesubgraph.rs
+++ b/src/rules/kclique_balancedcompletebipartitesubgraph.rs
@@ -56,16 +56,12 @@ impl ReductionResult for ReductionKCliqueToBCBS {
 #[crate::aggregate_reduction(identity)]
 impl crate::rules::AggregateReductionResult for ReductionKCliqueToBCBS {}
 
-#[reduction(
-    transform = upper_bound {
-        left_size = "num_vertices + k * (k - 1) / 2",
-        right_size = "num_edges + num_vertices - k",
-        k = "num_vertices + k * (k - 1) / 2 - k",
-    },
-    unavailable = {
-        num_vertices = "the exact target parameter is not represented by this reduction's symbolic transform",
-    }
-)]
+#[reduction(transform = upper_bound {
+    left_size = "num_vertices + k * (k - 1) / 2",
+    right_size = "num_edges + num_vertices - k",
+    k = "num_vertices + k * (k - 1) / 2 - k",
+    num_vertices = "2 * num_vertices + num_edges + k * (k - 1) / 2 - k",
+})]
 impl ReduceTo<BalancedCompleteBipartiteSubgraph> for KClique<SimpleGraph> {
     type Result = ReductionKCliqueToBCBS;
 
diff --git a/src/rules/knapsack_ilp.rs b/src/rules/knapsack_ilp.rs
index 2b2c400ff..e26e2f8be 100644
--- a/src/rules/knapsack_ilp.rs
+++ b/src/rules/knapsack_ilp.rs
@@ -41,7 +41,7 @@ impl ReductionResult for ReductionKnapsackToILP {
         num_vars = "num_items",
     },
     upper_bound {
-        max_constraint_magnitude_bits = "capacity + 1",
+        max_constraint_magnitude_bits = "capacity_bits",
         num_constraints = "num_items + 1",
         num_nonzeros = "num_items",
     },
diff --git a/src/rules/knapsack_qubo.rs b/src/rules/knapsack_qubo.rs
index 39d844644..8ecc8cdda 100644
--- a/src/rules/knapsack_qubo.rs
+++ b/src/rules/knapsack_qubo.rs
@@ -44,9 +44,13 @@ impl ReductionResult for ReductionKnapsackToQUBO {
     }
 }
 
-#[reduction(transform = unavailable {
-    num_vars = "the exact piecewise slack-bit count is not representable in the parameter-expression language",
-    num_quadratic_terms = "the nonzero products depend on item sizes and values",
+#[reduction(transform = {
+    exact {
+        num_vars = "num_items + capacity_bits",
+    },
+    upper_bound {
+        num_quadratic_terms = "(num_items + capacity_bits)^2",
+    },
 })]
 impl ReduceTo<QUBO<i64>> for Knapsack {
     type Result = ReductionKnapsackToQUBO;
diff --git a/src/rules/ksatisfiability_directedtwocommodityintegralflow.rs b/src/rules/ksatisfiability_directedtwocommodityintegralflow.rs
index 655396bd3..cbc842d3f 100644
--- a/src/rules/ksatisfiability_directedtwocommodityintegralflow.rs
+++ b/src/rules/ksatisfiability_directedtwocommodityintegralflow.rs
@@ -189,15 +189,11 @@ impl ReductionResult for Reduction3SATToDirectedTwoCommodityIntegralFlow {
 #[crate::aggregate_reduction(identity)]
 impl crate::rules::AggregateReductionResult for Reduction3SATToDirectedTwoCommodityIntegralFlow {}
 
-#[reduction(
-    transform = exact {
-        num_vertices = "6 * num_vars + 2 * num_literals + num_clauses + 4",
-        num_arcs = "7 * num_vars + 4 * num_literals + num_clauses + 1",
-    },
-    unavailable = {
-        max_capacity = "the exact target parameter is not represented by this reduction's symbolic transform",
-    }
-)]
+#[reduction(transform = exact {
+    num_vertices = "6 * num_vars + 2 * num_literals + num_clauses + 4",
+    num_arcs = "7 * num_vars + 4 * num_literals + num_clauses + 1",
+    max_capacity = "1",
+})]
 impl ReduceTo<DirectedTwoCommodityIntegralFlow> for KSatisfiability<K3> {
     type Result = Reduction3SATToDirectedTwoCommodityIntegralFlow;
 
diff --git a/src/rules/ksatisfiability_preemptivescheduling.rs b/src/rules/ksatisfiability_preemptivescheduling.rs
index 2d651e5f1..1a61efea7 100644
--- a/src/rules/ksatisfiability_preemptivescheduling.rs
+++ b/src/rules/ksatisfiability_preemptivescheduling.rs
@@ -368,16 +368,12 @@ impl crate::rules::AggregateReductionResult for Reduction3SATToPreemptiveSchedul
     }
 }
 
-#[reduction(
-    transform = upper_bound {
-        num_tasks = "(2 * num_vars + 3 + 6 * num_clauses) * (num_vars + 3)",
-        num_processors = "2 * num_vars + 3 + 6 * num_clauses",
-        d_max = "(2 * num_vars + 3 + 6 * num_clauses) * (num_vars + 3)",
-    },
-    unavailable = {
-        num_precedences = "the exact target parameter is not represented by this reduction's symbolic transform",
-    }
-)]
+#[reduction(transform = upper_bound {
+    num_tasks = "(2 * num_vars + 3 + 6 * num_clauses) * (num_vars + 3)",
+    num_processors = "2 * num_vars + 3 + 6 * num_clauses",
+    d_max = "(2 * num_vars + 3 + 6 * num_clauses) * (num_vars + 3)",
+    num_precedences = "((2 * num_vars + 3 + 6 * num_clauses) * (num_vars + 3))^2",
+})]
 impl ReduceTo<PreemptiveScheduling> for KSatisfiability<K3> {
     type Result = Reduction3SATToPreemptiveScheduling;
 
diff --git a/src/rules/ksatisfiability_simultaneousincongruences.rs b/src/rules/ksatisfiability_simultaneousincongruences.rs
index 7fa0c5dc5..693b5805f 100644
--- a/src/rules/ksatisfiability_simultaneousincongruences.rs
+++ b/src/rules/ksatisfiability_simultaneousincongruences.rs
@@ -181,8 +181,8 @@ fn ensure_prime_product_fits_target(
 impl crate::rules::AggregateReductionResult for Reduction3SATToSimultaneousIncongruences {}
 
 #[reduction(
-    transform = unavailable {
-        num_pairs = "the number of residue pairs depends on the first num_vars odd primes and is not expressible in the size-expression language",
+    transform = upper_bound {
+        num_pairs = "2 * num_vars * (num_vars + 1)^2 + num_clauses",
     }
 )]
 impl ReduceTo<SimultaneousIncongruences> for KSatisfiability<K3> {
diff --git a/src/rules/minimumvertexcover_longestcommonsubsequence.rs b/src/rules/minimumvertexcover_longestcommonsubsequence.rs
index 2cdc94188..12b8bc604 100644
--- a/src/rules/minimumvertexcover_longestcommonsubsequence.rs
+++ b/src/rules/minimumvertexcover_longestcommonsubsequence.rs
@@ -39,16 +39,20 @@ impl ReductionResult for ReductionVCToLCS {
 }
 
 #[reduction(
-    transform = exact {
-        alphabet_size = "num_vertices",
-        num_strings = "num_edges + 1",
-        max_length = "num_vertices",
-        total_length = "num_vertices + 2 * num_edges * num_vertices - 2 * num_edges",
-        sum_triangular_lengths = "num_vertices * (num_vertices + 1) / 2 + num_edges * (2 * num_vertices - 2) * (2 * num_vertices - 1) / 2",
+    transform = {
+        exact {
+            alphabet_size = "num_vertices",
+            num_strings = "num_edges + 1",
+            max_length = "num_vertices",
+            total_length = "num_vertices + 2 * num_edges * num_vertices - 2 * num_edges",
+            sum_triangular_lengths = "num_vertices * (num_vertices + 1) / 2 + num_edges * (2 * num_vertices - 2) * (2 * num_vertices - 1) / 2",
+        },
+        upper_bound {
+            num_transitions = "num_vertices",
+        },
     },
     unavailable = {
         cross_frequency_product = "the exact target parameter is not represented by this reduction's symbolic transform",
-        num_transitions = "the exact target parameter is not represented by this reduction's symbolic transform",
     }
 )]
 impl ReduceTo<LongestCommonSubsequence> for MinimumVertexCover<SimpleGraph, One> {
diff --git a/src/rules/openshopscheduling_ilp.rs b/src/rules/openshopscheduling_ilp.rs
index ca6ad3955..41a20ffe0 100644
--- a/src/rules/openshopscheduling_ilp.rs
+++ b/src/rules/openshopscheduling_ilp.rs
@@ -109,7 +109,7 @@ impl ReductionResult for ReductionOSSToILP {
         num_constraints = "num_jobs * (num_jobs - 1) / 2 * num_machines + num_jobs * num_machines + 1 + 2 * num_jobs * (num_jobs - 1) / 2 * num_machines + num_jobs * num_machines * (num_machines - 1) / 2 + 2 * num_jobs * num_machines * (num_machines - 1) / 2 + num_jobs * num_machines",
     },
     upper_bound {
-        max_constraint_magnitude_bits = "schedule_horizon + 1",
+        max_constraint_magnitude_bits = "schedule_horizon_bits",
         num_nonzeros = "(num_jobs * (num_jobs - 1) / 2 * num_machines + num_jobs * num_machines + num_jobs * num_machines * (num_machines - 1) / 2 + 1) * (num_jobs * (num_jobs - 1) / 2 * num_machines + num_jobs * num_machines + 1 + 2 * num_jobs * (num_jobs - 1) / 2 * num_machines + num_jobs * num_machines * (num_machines - 1) / 2 + 2 * num_jobs * num_machines * (num_machines - 1) / 2 + num_jobs * num_machines)",
     },
 })]
@@ -324,7 +324,7 @@ impl crate::rules::AggregateReductionResult for ReductionDecisionOpenShopSchedul
         num_constraints = "3 * num_jobs * (num_jobs - 1) / 2 * num_machines + 2 * num_jobs * num_machines + 3 * num_jobs * num_machines * (num_machines - 1) / 2 + 2",
     },
     upper_bound {
-        max_constraint_magnitude_bits = "schedule_horizon + 1",
+        max_constraint_magnitude_bits = "schedule_horizon_bits",
         num_nonzeros = "(num_jobs * (num_jobs - 1) / 2 * num_machines + num_jobs * num_machines + num_jobs * num_machines * (num_machines - 1) / 2 + 1) * (3 * num_jobs * (num_jobs - 1) / 2 * num_machines + 2 * num_jobs * num_machines + 3 * num_jobs * num_machines * (num_machines - 1) / 2 + 2)",
     },
 })]
diff --git a/src/rules/partition_knapsack.rs b/src/rules/partition_knapsack.rs
index bb0584ff8..3d088f0d1 100644
--- a/src/rules/partition_knapsack.rs
+++ b/src/rules/partition_knapsack.rs
@@ -49,9 +49,12 @@ impl crate::rules::AggregateReductionResult for ReductionPartitionToKnapsack {
 }
 
 #[reduction(
-    transform = exact { num_items = "num_elements" },
+    transform = {
+        exact { num_items = "num_elements" },
+        upper_bound { capacity_bits = "max_numeric_magnitude_bits + num_elements" },
+    },
     unavailable = {
-        capacity = "the exact target parameter is not represented by this reduction's symbolic transform",
+        capacity = "raw capacity requires numeric magnitude values; downstream predictions use capacity_bits",
     }
 )]
 impl ReduceTo<Knapsack> for Partition {
diff --git a/src/rules/partition_openshopscheduling.rs b/src/rules/partition_openshopscheduling.rs
index 7fb5d0ac2..fe467b900 100644
--- a/src/rules/partition_openshopscheduling.rs
+++ b/src/rules/partition_openshopscheduling.rs
@@ -81,12 +81,17 @@ impl ReductionResult for ReductionPartitionToOpenShopScheduling {
 impl crate::rules::AggregateReductionResult for ReductionPartitionToOpenShopScheduling {}
 
 #[reduction(
-    transform = exact {
-        num_jobs = "num_elements + 1",
-        num_machines = "3",
+    transform = {
+        exact {
+            num_jobs = "num_elements + 1",
+            num_machines = "3",
+        },
+        upper_bound {
+            schedule_horizon_bits = "max_numeric_magnitude_bits + num_elements + 3",
+        },
     },
     unavailable = {
-        schedule_horizon = "depends on the numeric partition sizes, which are not represented by source size parameters",
+        schedule_horizon = "raw horizon requires numeric magnitude values; downstream predictions use schedule_horizon_bits",
     }
 )]
 impl ReduceTo<Decision<OpenShopScheduling>> for Partition {
diff --git a/src/rules/sat_circuitsat.rs b/src/rules/sat_circuitsat.rs
index 3f79a7a1e..9675dd5a0 100644
--- a/src/rules/sat_circuitsat.rs
+++ b/src/rules/sat_circuitsat.rs
@@ -49,16 +49,12 @@ impl ReductionResult for ReductionSATToCircuit {
 #[crate::aggregate_reduction(identity)]
 impl crate::rules::AggregateReductionResult for ReductionSATToCircuit {}
 
-#[reduction(
-    transform = upper_bound {
-        num_variables = "2 * num_vars + num_clauses + 1",
-        num_assignments = "num_vars + num_clauses + 2",
-    },
-    unavailable = {
-        num_assignment_outputs = "the exact target parameter is not represented by this reduction's symbolic transform",
-        num_expression_nodes = "the exact target parameter is not represented by this reduction's symbolic transform",
-    }
-)]
+#[reduction(transform = upper_bound {
+    num_variables = "2 * num_vars + num_clauses + 1",
+    num_assignments = "num_vars + num_clauses + 2",
+    num_assignment_outputs = "num_vars + num_clauses + 2",
+    num_expression_nodes = "num_vars + 2 * num_literals + 2 * num_clauses + 2",
+})]
 impl ReduceTo<CircuitSAT> for Satisfiability {
     type Result = ReductionSATToCircuit;
 
diff --git a/src/rules/sat_ksat.rs b/src/rules/sat_ksat.rs
index b7aef7264..fd5607f92 100644
--- a/src/rules/sat_ksat.rs
+++ b/src/rules/sat_ksat.rs
@@ -129,15 +129,11 @@ fn add_clause_to_ksat(
 macro_rules! impl_sat_to_ksat {
     ($ktype:ty, $k:expr) => {
         #[rustfmt::skip]
-        #[reduction(
-    transform = upper_bound {
-        num_clauses = "8 * num_clauses + num_literals",
-        num_vars = "num_vars + 7 * num_clauses + num_literals",
-    },
-    unavailable = {
-        num_literals = "the exact target parameter is not represented by this reduction's symbolic transform",
-    }
-)]
+        #[reduction(transform = upper_bound {
+            num_clauses = "8 * num_clauses + num_literals",
+            num_vars = "num_vars + 7 * num_clauses + num_literals",
+            num_literals = "3 * (8 * num_clauses + num_literals)",
+        })]
         impl ReduceTo<KSatisfiability<$ktype>> for Satisfiability {
             type Result = ReductionSATToKSAT<$ktype>;
 
diff --git a/src/rules/satisfiability_integralflowhomologousarcs.rs b/src/rules/satisfiability_integralflowhomologousarcs.rs
index 17b963efc..042b3bed1 100644
--- a/src/rules/satisfiability_integralflowhomologousarcs.rs
+++ b/src/rules/satisfiability_integralflowhomologousarcs.rs
@@ -125,15 +125,11 @@ impl ReductionResult for ReductionSATToIntegralFlowHomologousArcs {
 #[crate::aggregate_reduction(identity)]
 impl crate::rules::AggregateReductionResult for ReductionSATToIntegralFlowHomologousArcs {}
 
-#[reduction(
-    transform = upper_bound {
-        num_vertices = "2 * num_vars * num_clauses + 3 * num_vars + 2 * num_clauses + 2",
-        num_arcs = "2 * num_vars * num_clauses + 5 * num_vars + num_clauses + num_literals",
-    },
-    unavailable = {
-        max_capacity = "the exact target parameter is not represented by this reduction's symbolic transform",
-    }
-)]
+#[reduction(transform = upper_bound {
+    num_vertices = "2 * num_vars * num_clauses + 3 * num_vars + 2 * num_clauses + 2",
+    num_arcs = "2 * num_vars * num_clauses + 5 * num_vars + num_clauses + num_literals",
+    max_capacity = "num_literals + 1",
+})]
 impl ReduceTo<IntegralFlowHomologousArcs> for Satisfiability {
     type Result = ReductionSATToIntegralFlowHomologousArcs;
 
diff --git a/src/rules/satisfiability_naesatisfiability.rs b/src/rules/satisfiability_naesatisfiability.rs
index e0efdf532..a02a28321 100644
--- a/src/rules/satisfiability_naesatisfiability.rs
+++ b/src/rules/satisfiability_naesatisfiability.rs
@@ -52,16 +52,16 @@ impl ReductionResult for ReductionSATToNAESAT {
 #[crate::aggregate_reduction(identity)]
 impl crate::rules::AggregateReductionResult for ReductionSATToNAESAT {}
 
-#[reduction(
-    transform = exact {
+#[reduction(transform = {
+    exact {
         num_vars = "num_vars + 1",
         num_clauses = "num_clauses",
-        num_literals = "num_literals + num_clauses",
     },
-    unavailable = {
-        num_literal_pairs = "the exact target parameter is not represented by this reduction's symbolic transform",
-    }
-)]
+    upper_bound {
+        num_literals = "num_literals + 2 * num_clauses",
+        num_literal_pairs = "(num_literals + 2 * num_clauses)^2",
+    },
+})]
 impl ReduceTo<NAESatisfiability> for Satisfiability {
     type Result = ReductionSATToNAESAT;
 
diff --git a/src/rules/setsplitting_betweenness.rs b/src/rules/setsplitting_betweenness.rs
index 547982fa4..afb1eeb63 100644
--- a/src/rules/setsplitting_betweenness.rs
+++ b/src/rules/setsplitting_betweenness.rs
@@ -51,12 +51,10 @@ impl ReductionResult for ReductionSetSplittingToBetweenness {
 #[crate::aggregate_reduction(identity)]
 impl crate::rules::AggregateReductionResult for ReductionSetSplittingToBetweenness {}
 
-#[reduction(
-    transform = unavailable {
-        num_elements = "the exact target parameters depend on normalization statistics specific to this reduction",
-        num_triples = "the exact target parameters depend on normalization statistics specific to this reduction",
-    }
-)]
+#[reduction(transform = upper_bound {
+    num_elements = "universe_size + 1 + num_subsets * (4 * universe_size + 1)",
+    num_triples = "2 * num_subsets * (2 * universe_size + 1)",
+})]
 impl ReduceTo<Betweenness> for SetSplitting {
     type Result = ReductionSetSplittingToBetweenness;
 
diff --git a/src/rules/subsetsum_closestvectorproblem.rs b/src/rules/subsetsum_closestvectorproblem.rs
index 8dbf54908..6a0142f0d 100644
--- a/src/rules/subsetsum_closestvectorproblem.rs
+++ b/src/rules/subsetsum_closestvectorproblem.rs
@@ -67,23 +67,21 @@ impl ReductionSubsetSumToClosestVectorProblem {
     }
 }
 
-#[reduction(
-    transform = unavailable {
-        ambient_dimension = "2n+b depends on input bit length b, which is not a registered SubsetSum parameter",
-        num_basis_vectors = "n+b-1 depends on input bit length b, which is not a registered SubsetSum parameter",
+#[reduction(transform = {
+    exact {
+        ambient_dimension = "2 * num_elements + max_numeric_magnitude_bits",
+        num_basis_vectors = "num_elements + max_numeric_magnitude_bits - 1",
     },
-)]
+    upper_bound {
+        max_numeric_magnitude_bits = "2",
+    }
+})]
 impl ReduceTo<Decision<ClosestVectorProblem>> for SubsetSum {
     type Result = ReductionSubsetSumToClosestVectorProblem;
 
     fn reduce_to(&self) -> Result<Self::Result, crate::rules::ReductionError> {
         let n = self.num_elements();
-        let bit_width = self
-            .sizes()
-            .iter()
-            .fold(self.target().bits().max(1), |bits, size| {
-                bits.max(size.bits())
-            });
+        let bit_width = self.max_numeric_magnitude_bits();
         let (bits, rows, columns) =
             ReductionSubsetSumToClosestVectorProblem::dimensions(n, bit_width)?;
         let mut basis = Vec::with_capacity(columns);
diff --git a/src/rules/subsetsum_integerknapsack.rs b/src/rules/subsetsum_integerknapsack.rs
index 26c93814b..ca262844e 100644
--- a/src/rules/subsetsum_integerknapsack.rs
+++ b/src/rules/subsetsum_integerknapsack.rs
@@ -32,10 +32,13 @@ inventory::submit! {
         source_variant_fn: <SubsetSum as Problem>::variant,
         target_variant_fn: <IntegerKnapsack as Problem>::variant,
         parameter_declarations_fn: || ReductionParameterDeclarations {
-            fields: vec![("num_items", crate::parameters::ParameterRelation::Exact, Expr::variable("num_elements"))],
+            fields: vec![
+                ("num_items", crate::parameters::ParameterRelation::Exact, Expr::variable("num_elements")),
+                ("capacity_bits", crate::parameters::ParameterRelation::UpperBound, Expr::variable("max_numeric_magnitude_bits")),
+            ],
             unavailable: vec![crate::rules::registry::UnavailableParameterField {
                 field: "capacity",
-                reason: "the target capacity equals the SubsetSum target, which is not a registered source parameter",
+                reason: "raw capacity requires numeric magnitude values; downstream predictions use capacity_bits",
             }],
         },
         module_path: module_path!(),
diff --git a/src/unit_tests/ilp_overhead.rs b/src/unit_tests/ilp_overhead.rs
index 205bc9a70..320afb524 100644
--- a/src/unit_tests/ilp_overhead.rs
+++ b/src/unit_tests/ilp_overhead.rs
@@ -13,6 +13,124 @@ use crate::{
 
 type BoundedILP = ILP<i64, i64, Bounded>;
 
+#[test]
+fn integer_knapsack_and_open_shop_bit_predictions_reach_qubo() {
+    use crate::models::{set::IntegerKnapsack, Decision};
+    for capacity in [0, 2, 5] {
+        check_qubo::<_, BoundedILP>(
+            IntegerKnapsack::new(vec![2, 3], vec![3, 5], capacity).unwrap(),
+        );
+    }
+    let source = OpenShopScheduling::new(1, vec![vec![2]]);
+    check_qubo::<_, BoundedILP>(source.clone());
+    for bound in [1, 2] {
+        check_qubo::<_, BoundedILP>(Decision::new(source.clone(), bound));
+    }
+}
+
+#[test]
+fn partition_open_shop_predictions_preserve_ilp_solution_recovery() {
+    use crate::models::Decision;
+    let graph = ReductionGraph::new();
+    let path = ReductionPath {
+        steps: vec![
+            step::<Partition>(),
+            step::<Decision<OpenShopScheduling>>(),
+            step::<BoundedILP>(),
+        ],
+    };
+    for (sizes, feasible) in [(vec![1], false), (vec![1, 1], true), (vec![1, 3], false)] {
+        let source = Partition::new(sizes).unwrap();
+        let predicted = graph
+            .compose_path_parameter_transform(&path)
+            .unwrap()
+            .unwrap()
+            .evaluate(&source.parameters())
+            .unwrap();
+        let chain = graph.reduce_along_path(&path, &source).unwrap().unwrap();
+        let target = chain.target_problem::<BoundedILP>();
+        for (field, actual) in target.parameters().iter() {
+            assert!(predicted.get(field).expect(field) >= actual);
+        }
+        match ILPSolver::new().solve(target) {
+            Ok(solution) => {
+                assert!(feasible);
+                let recovered = chain.extract_solution::<Vec<bool>, _>(&solution).unwrap();
+                assert!(source.evaluate(&recovered).unwrap().0);
+            }
+            Err(crate::solvers::ILPSolveError::Infeasible) => assert!(!feasible),
+            Err(error) => panic!("{error}"),
+        }
+    }
+}
+
+#[test]
+fn partition_knapsack_qubo_predictions_and_solution_recovery() {
+    for sizes in [vec![1], vec![1, 1], vec![1, 2], vec![1, 3]] {
+        for through_ilp in [false, true] {
+            let mut steps = vec![step::<Partition>(), step::<Knapsack>()];
+            if through_ilp {
+                steps.push(step::<ILP<bool>>());
+            }
+            steps.push(step::<QUBO<i64>>());
+            check_path(
+                Partition::new(sizes.clone()).unwrap(),
+                ReductionPath { steps },
+            );
+        }
+    }
+    let path = ReductionPath {
+        steps: vec![step::<Partition>(), step::<Knapsack>(), step::<QUBO<i64>>()],
+    };
+    let source = Partition::new(vec![1 << 19; 10]).unwrap();
+    let predicted = ReductionGraph::new()
+        .compose_path_parameter_transform(&path)
+        .unwrap()
+        .unwrap()
+        .evaluate(&source.parameters())
+        .unwrap();
+    assert!(predicted.get("num_vars").unwrap() <= 40);
+    assert!(predicted.get("num_quadratic_terms").unwrap() <= 1600);
+}
+
+#[test]
+fn subset_sum_lattice_qubo_predictions_and_solution_recovery() {
+    use crate::models::{algebraic::ClosestVectorProblem, Decision};
+    for (sizes, target) in [(vec![1], 1), (vec![2], 1)] {
+        check_path(
+            SubsetSum::new(sizes, target),
+            ReductionPath {
+                steps: vec![
+                    step::<SubsetSum>(),
+                    step::<Decision<ClosestVectorProblem>>(),
+                    step::<ClosestVectorProblem>(),
+                    step::<QUBO<i64>>(),
+                ],
+            },
+        );
+    }
+}
+
+#[test]
+fn factoring_circuit_sat_qubo_predictions_and_solution_recovery() {
+    use crate::models::formula::{CircuitSAT, NAESatisfiability, Satisfiability};
+    for target in [1u32, 3] {
+        check_path(
+            Factoring::with_factor_bits(target, 1, 1),
+            ReductionPath {
+                steps: vec![
+                    step::<Factoring>(),
+                    step::<CircuitSAT>(),
+                    step::<Satisfiability>(),
+                    step::<NAESatisfiability>(),
+                    step::<ILP<bool>>(),
+                    step::<QUBO<i64>>(),
+                ],
+            },
+        );
+    }
+}
+
 fn check_contract<S: Problem + ReduceTo<T>, T: Problem>(source: &S) {
     let target = source.reduce_to().unwrap();
     let entry = crate::rules::registry::reduction_entries()
diff --git a/src/unit_tests/problem_parameters.rs b/src/unit_tests/problem_parameters.rs
index 200f0a081..778b89fae 100644
--- a/src/unit_tests/problem_parameters.rs
+++ b/src/unit_tests/problem_parameters.rs
@@ -200,6 +200,7 @@ fn test_problem_parameters_biclique_cover() {
     let size = bc.parameters();
     assert_eq!(size.get("left_size"), Some(2));
     assert_eq!(size.get("right_size"), Some(3));
+    assert_eq!(size.get("num_vertices"), Some(5));
     assert_eq!(size.get("num_edges"), Some(3));
     assert_eq!(size.get("rank"), Some(2));
 }
diff --git a/src/unit_tests/rules/subsetsum_integerknapsack.rs b/src/unit_tests/rules/subsetsum_integerknapsack.rs
index 15a2978f8..36f190079 100644
--- a/src/unit_tests/rules/subsetsum_integerknapsack.rs
+++ b/src/unit_tests/rules/subsetsum_integerknapsack.rs
@@ -34,6 +34,52 @@ fn subset_sum_embedding(source: &SubsetSum) -> IntegerKnapsack {
     .unwrap()
 }
 
+#[test]
+fn test_subsetsum_integerknapsack_capacity_bits_propagate() {
+    use crate::models::algebraic::{Bounded, ILP};
+    use crate::rules::{ReduceTo, ReductionResult};
+    let entries = crate::rules::registry::reduction_entries();
+    let embedding = entries
+        .iter()
+        .find(|entry| {
+            entry.source_name == SubsetSum::NAME && entry.target_name == IntegerKnapsack::NAME
+        })
+        .unwrap()
+        .parameter_contract()
+        .unwrap();
+    let ilp = entries
+        .iter()
+        .find(|entry| entry.source_name == IntegerKnapsack::NAME && entry.target_name == "ILP")
+        .unwrap()
+        .parameter_contract()
+        .unwrap();
+    let composed = embedding
+        .transform()
+        .unwrap()
+        .compose(ilp.transform().unwrap(), "SubsetSum -> ILP")
+        .unwrap();
+    for (sizes, target, bits) in [(vec![1], 0, 1), (vec![1], 8, 4), (vec![8], 1, 4)] {
+        let source = SubsetSum::new(sizes, target);
+        let intermediate = subset_sum_embedding(&source);
+        let prediction = embedding
+            .transform()
+            .unwrap()
+            .evaluate(&source.parameters())
+            .unwrap();
+        assert_eq!(prediction.get("capacity_bits"), Some(bits));
+        assert!(prediction.get("capacity").is_none());
+        assert!(
+            prediction.get("capacity_bits").unwrap()
+                >= intermediate.parameters().get("capacity_bits").unwrap()
+        );
+        let reduced = ReduceTo::<ILP<i64, i64, Bounded>>::reduce_to(&intermediate).unwrap();
+        let predicted = composed.evaluate(&source.parameters()).unwrap();
+        for (field, actual) in reduced.target_problem().parameters().iter() {
+            assert!(predicted.get(field).expect(field) >= actual);
+        }
+    }
+}
+
 #[test]
 fn test_subsetsum_to_integerknapsack_forward_example() {
     let source = SubsetSum::new(vec![3u32, 7, 1, 8, 5], 16u32);
diff --git a/src/unit_tests/symbolic_parameter_contracts.rs b/src/unit_tests/symbolic_parameter_contracts.rs
index 8cd2aed03..c095f9eab 100644
--- a/src/unit_tests/symbolic_parameter_contracts.rs
+++ b/src/unit_tests/symbolic_parameter_contracts.rs
@@ -8,6 +8,39 @@ use crate::topology::SimpleGraph;
 use crate::types::ProblemParameters;
 use crate::Problem;
 
+#[test]
+fn parameter_schemas_keep_distinct_counts_without_synonymous_aliases() {
+    let graph = ReductionGraph::new();
+    for (model, retained) in [
+        ("ExactCoverBy3Sets", &["num_subsets"][..]),
+        ("ClosestString", &["string_length", "total_length"]),
+        ("ClosestSubstring", &["total_length", "total_num_windows"]),
+        ("ThreePartition", &["num_elements", "num_groups"]),
+        ("PaintShop", &["num_cars", "num_sequence"]),
+        (
+            "MinimumCodeGenerationOneRegister",
+            &["num_vertices", "num_leaves", "num_internal"],
+        ),
+        (
+            "HamiltonianPath",
+            &["num_vertices", "num_consecutive_positions"],
+        ),
+        (
+            "LongestCommonSubsequence",
+            &["max_length", "num_transitions"],
+        ),
+    ] {
+        let fields = graph.parameter_names(model);
+        for field in retained {
+            assert!(fields.iter().any(|name| name == field), "{model}: {field}");
+        }
+    }
+    assert!(!graph
+        .parameter_names("ExactCoverBy3Sets")
+        .iter()
+        .any(|field| field == "num_sets"));
+}
+
 #[test]
 fn exact_rule_formula_matches_the_constructed_target() {
     let source = MaximumIndependentSet::<SimpleGraph, i64>::new(
@@ -193,13 +226,6 @@ where
             S::NAME,
             T::NAME
         );
-        assert_eq!(
-            predicted.get(field),
-            actual.get(field),
-            "{} -> {}: {field}",
-            S::NAME,
-            T::NAME
-        );
         assert!(
             !contract
                 .unavailable()
@@ -352,10 +378,8 @@ fn parameter_relations_match_reduced_instances() {
 
 #[test]
 fn exact_parameter_formulas_cover_sparse_and_boundary_instances() {
-    use crate::models::algebraic::{QuadraticAssignment, BMF, ILP};
-    use crate::models::graph::{
-        BicliqueCover, HamiltonianCircuit, HamiltonianPath, MinimumVertexCover,
-    };
+    use crate::models::algebraic::{QuadraticAssignment, ILP};
+    use crate::models::graph::{HamiltonianCircuit, HamiltonianPath, MinimumVertexCover};
     use crate::models::misc::{
         ConsistencyOfDatabaseFrequencyTables, FrequencyTable, KnownValue, LongestCommonSubsequence,
         MaximumLikelihoodRanking, RegisterSufficiency,
@@ -422,23 +446,6 @@ fn exact_parameter_formulas_cover_sparse_and_boundary_instances() {
         &["sum_triangular_lengths"],
         exact,
     );
-
-    let source = BMF::new(vec![vec![true, false], vec![false, true]], 1);
-    let reduction = ReduceTo::<BicliqueCover>::reduce_to(&source).unwrap();
-    assert_eq!(
-        reduction.target_problem().parameters().get("num_edges"),
-        Some(2)
-    );
-    let entry = crate::rules::registry::reduction_entries()
-        .into_iter()
-        .find(|entry| entry.source_name == "BMF" && entry.target_name == "BicliqueCover")
-        .unwrap();
-    let contract = entry.parameter_contract().unwrap();
-    assert!(contract.transform().unwrap().get("num_edges").is_none());
-    assert!(contract
-        .unavailable()
-        .iter()
-        .any(|field| field.field == "num_edges"));
 }
 
 #[test]
@@ -532,3 +539,378 @@ fn augmentation_magnitude_predictions_cover_weights_and_budgets() {
         );
     }
 }
+#[test]
+fn missing_structural_bounds_cover_sparse_and_normalized_instances() {
+    use crate::models::{
+        algebraic::BMF,
+        graph::{BalancedCompleteBipartiteSubgraph, BicliqueCover, KClique},
+        set::MaximumSetPacking,
+    };
+    use crate::types::One;
+    let upper = ParameterRelation::UpperBound;
+    for matrix in [
+        vec![],
+        vec![vec![]],
+        vec![vec![false; 3]; 2],
+        vec![vec![true, false], vec![false, true]],
+        vec![vec![true; 3]; 2],
+    ] {
+        check_reduced_parameters::<_, BicliqueCover>(BMF::new(matrix, 1), &["num_edges"], upper);
+    }
+    for subsets in [vec![], vec![[0, 1, 2]], vec![[0, 1, 2], [0, 1, 2]]] {
+        check_reduced_parameters::<_, MaximumSetPacking<One>>(
+            ExactCoverBy3Sets::new(6, subsets),
+            &["universe_size"],
+            upper,
+        );
+    }
+    for graph in [
+        SimpleGraph::empty(3),
+        SimpleGraph::new(3, vec![(0, 0), (0, 1), (0, 1)]),
+        SimpleGraph::complete(3),
+    ] {
+        check_reduced_parameters::<_, BalancedCompleteBipartiteSubgraph>(
+            KClique::new(graph, 2),
+            &["num_vertices"],
+            upper,
+        );
+    }
+}
+
+#[test]
+fn sat_bounds_cover_empty_short_and_repeated_clauses() {
+    use crate::models::{
+        formula::{CNFClause, CircuitSAT, KSatisfiability, NAESatisfiability, Satisfiability},
+        graph::IntegralFlowHomologousArcs,
+    };
+    use crate::variant::K3;
+    for clauses in [
+        vec![],
+        vec![CNFClause::new(vec![])],
+        vec![CNFClause::new(vec![1])],
+        vec![CNFClause::new(vec![1, -1, 2, 2, 3])],
+    ] {
+        let source = Satisfiability::new(4, clauses);
+        check_reduced_parameters::<_, KSatisfiability<K3>>(
+            source.clone(),
+            &["num_literals"],
+            ParameterRelation::UpperBound,
+        );
+        check_reduced_parameters::<_, NAESatisfiability>(
+            source.clone(),
+            &["num_literal_pairs"],
+            ParameterRelation::UpperBound,
+        );
+        check_reduced_parameters::<_, CircuitSAT>(
+            source.clone(),
+            &["num_expression_nodes", "num_assignment_outputs"],
+            ParameterRelation::UpperBound,
+        );
+        check_reduced_parameters::<_, IntegralFlowHomologousArcs>(
+            source,
+            &["max_capacity"],
+            ParameterRelation::UpperBound,
+        );
+    }
+}
+
+#[test]
+fn circuit_bounds_cover_fanin_constants_and_multiple_outputs() {
+    use crate::models::formula::{Assignment, BooleanExpr, Circuit, CircuitSAT, Satisfiability};
+    for expr in [
+        BooleanExpr::constant(true),
+        BooleanExpr::not(BooleanExpr::var("x")),
+        BooleanExpr::xor(vec![BooleanExpr::var("x"); 8]),
+        BooleanExpr::and(vec![
+            BooleanExpr::or(vec![
+                BooleanExpr::var("x"),
+                BooleanExpr::var("y")
+            ]);
+            4
+        ]),
+    ] {
+        for outputs in [vec![], vec!["a".into(), "b".into()]] {
+            let source =
+                CircuitSAT::new(Circuit::new(vec![Assignment::new(outputs, expr.clone())]));
+            check_reduced_parameters::<_, Satisfiability>(
+                source,
+                &["num_vars", "num_clauses", "num_literals"],
+                ParameterRelation::UpperBound,
+            );
+        }
+    }
+}
+
+#[test]
+fn factoring_circuit_bounds_cover_zero_width_and_overflow_sentinels() {
+    use crate::models::{formula::CircuitSAT, misc::Factoring};
+    for m in 0..=3 {
+        for n in m..=3 {
+            for target in [0u64, 1, 255] {
+                check_reduced_parameters::<_, CircuitSAT>(
+                    Factoring::with_factor_bits(target, m, n),
+                    &["num_assignment_outputs", "num_expression_nodes"],
+                    ParameterRelation::UpperBound,
+                );
+            }
+        }
+    }
+}
+
+#[test]
+fn sat_flow_and_scheduling_bounds_cover_fixed_outputs() {
+    use crate::models::{
+        formula::{CNFClause, KSatisfiability},
+        graph::DirectedTwoCommodityIntegralFlow,
+        misc::PreemptiveScheduling,
+    };
+    use crate::variant::K3;
+    for clauses in [
+        vec![],
+        vec![CNFClause::new(vec![])],
+        vec![CNFClause::new(vec![1, 1, -2])],
+    ] {
+        let source = KSatisfiability::<K3>::new_allow_less(2, clauses);
+        check_reduced_parameters::<_, DirectedTwoCommodityIntegralFlow>(
+            source.clone(),
+            &["max_capacity"],
+            ParameterRelation::Exact,
+        );
+        check_reduced_parameters::<_, PreemptiveScheduling>(
+            source,
+            &["num_precedences"],
+            ParameterRelation::UpperBound,
+        );
+    }
+}
+
+#[test]
+fn set_splitting_bounds_cover_deduplication_and_large_subsets() {
+    use crate::models::{misc::Betweenness, set::SetSplitting};
+    for subsets in [
+        vec![],
+        vec![vec![0, 0]],
+        vec![vec![0, 1]],
+        vec![(0..8).collect()],
+        vec![vec![0; 20], (0..8).collect()],
+    ] {
+        check_reduced_parameters::<_, Betweenness>(
+            SetSplitting::new(8, subsets),
+            &["num_elements", "num_triples"],
+            ParameterRelation::UpperBound,
+        );
+    }
+}
+
+#[test]
+fn decision_cover_bounds_do_not_depend_on_threshold_magnitude() {
+    use crate::models::{
+        graph::{HamiltonianCircuit, MinimumVertexCover},
+        Decision,
+    };
+    use crate::types::One;
+    for graph in [
+        SimpleGraph::empty(0),
+        SimpleGraph::path(3),
+        SimpleGraph::new(3, vec![(0, 0), (0, 1), (1, 2)]),
+    ] {
+        for threshold in [i64::MIN, 0, 1, 2, i64::MAX] {
+            check_reduced_parameters::<_, HamiltonianCircuit<SimpleGraph>>(
+                Decision::new(
+                    MinimumVertexCover::<_, One>::new(
+                        graph.clone(),
+                        vec![One; crate::topology::Graph::num_vertices(&graph)],
+                    ),
+                    threshold,
+                ),
+                &["num_vertices", "num_edges"],
+                ParameterRelation::UpperBound,
+            );
+        }
+    }
+}
+
+#[test]
+fn subset_lattice_dimensions_use_existing_numeric_magnitude() {
+    use crate::models::{algebraic::ClosestVectorProblem, misc::SubsetSum, Decision};
+    for (sizes, target) in [
+        (vec![], 0u64),
+        (vec![1], 0),
+        (vec![7], 8),
+        (vec![8], 7),
+        (vec![1, 3], 4),
+    ] {
+        check_reduced_parameters::<_, Decision<ClosestVectorProblem>>(
+            SubsetSum::new(sizes, target),
+            &["ambient_dimension", "num_basis_vectors"],
+            ParameterRelation::Exact,
+        );
+    }
+}
+
+#[test]
+fn knapsack_qubo_bounds_cover_capacity_boundaries() {
+    use crate::models::{algebraic::QUBO, misc::Knapsack};
+    for (capacity, bits) in [(0, 1), (1, 1), (2, 2), (3, 2), (4, 3), (7, 3), (8, 4)] {
+        let source = Knapsack::new(vec![0, 1, 2], vec![0, 2, 1], capacity);
+        assert_eq!(source.parameters().get("capacity_bits"), Some(bits));
+        check_reduced_parameters::<_, QUBO<i64>>(source, &["num_vars"], ParameterRelation::Exact);
+    }
+}
+
+#[test]
+fn knapsack_ilp_magnitude_uses_capacity_bits() {
+    use crate::models::{algebraic::ILP, misc::Knapsack};
+    for (capacity, bits) in [(0, 1), (7, 3), (8, 4), (i64::MAX, 63)] {
+        let source = Knapsack::new(vec![0, 1, i64::MAX], vec![1, 2, 3], capacity);
+        assert_eq!(source.parameters().get("capacity_bits"), Some(bits));
+        check_reduced_parameters::<_, ILP<bool>>(
+            source,
+            &["max_constraint_magnitude_bits"],
+            ParameterRelation::UpperBound,
+        );
+    }
+}
+
+#[test]
+fn partition_propagates_capacity_bits_without_raw_capacity() {
+    use crate::models::misc::{Knapsack, Partition};
+    for sizes in [vec![1], vec![1, 2], vec![7, 8], vec![i64::MAX]] {
+        check_reduced_parameters::<_, Knapsack>(
+            Partition::new(sizes).unwrap(),
+            &["capacity_bits"],
+            ParameterRelation::UpperBound,
+        );
+    }
+}
+
+#[test]
+fn integer_knapsack_capacity_bits_bound_ilp_magnitudes() {
+    use crate::models::{algebraic::ILP, set::IntegerKnapsack};
+    for (capacity, bits) in [(0, 1), (7, 3), (8, 4), (i64::MAX, 63)] {
+        let source = IntegerKnapsack::new(vec![1, i64::MAX], vec![1, 2], capacity).unwrap();
+        assert_eq!(source.parameters().get("capacity_bits"), Some(bits));
+        check_reduced_parameters::<_, ILP<i64, i64, Bounded>>(
+            source,
+            &["max_constraint_magnitude_bits"],
+            ParameterRelation::UpperBound,
+        );
+    }
+}
+
+#[test]
+fn open_shop_horizon_bits_cover_totals_and_decision_bounds() {
+    use crate::models::{algebraic::ILP, misc::OpenShopScheduling, Decision};
+    for (machines, times, bits) in [
+        (0, vec![vec![]], 1),
+        (2, vec![], 1),
+        (2, vec![vec![0, 0]], 1),
+        (2, vec![vec![3, 4]], 3),
+        (2, vec![vec![4, 4]], 4),
+        (1, vec![vec![i64::MAX]], 63),
+    ] {
+        let source = OpenShopScheduling::new(machines, times);
+        assert_eq!(source.parameters().get("schedule_horizon_bits"), Some(bits));
+        check_reduced_parameters::<_, ILP<i64, i64, Bounded>>(
+            source.clone(),
+            &["max_constraint_magnitude_bits"],
+            ParameterRelation::UpperBound,
+        );
+        for bound in [i64::MIN, 0, i64::MAX] {
+            check_reduced_parameters::<_, ILP<i64, i64, Bounded>>(
+                Decision::new(source.clone(), bound),
+                &["max_constraint_magnitude_bits"],
+                ParameterRelation::UpperBound,
+            );
+        }
+    }
+}
+
+#[test]
+fn partition_propagates_open_shop_horizon_bits() {
+    use crate::models::{
+        misc::{OpenShopScheduling, Partition},
+        Decision,
+    };
+    for sizes in [vec![1], vec![1, 1], vec![1, 2], vec![1 << 20; 2]] {
+        check_reduced_parameters::<_, Decision<OpenShopScheduling>>(
+            Partition::new(sizes).unwrap(),
+            &["schedule_horizon_bits"],
+            ParameterRelation::UpperBound,
+        );
+    }
+}
+
+#[test]
+fn closest_vector_size_bounds_cover_numeric_and_rank_variation() {
+    use crate::models::algebraic::{ClosestVectorProblem, QUBO};
+    for (basis, target, bits) in [
+        (vec![], vec![], 1),
+        (vec![], vec![-8], 4),
+        (vec![vec![1]], vec![0], 1),
+        (vec![vec![-8]], vec![1], 4),
+        (vec![vec![1]], vec![8], 4),
+        (vec![vec![2, 0], vec![1, 2]], vec![3, 2], 2),
+        (vec![vec![1, 8], vec![0, 1]], vec![-1, 1], 4),
+    ] {
+        let source = ClosestVectorProblem::new(basis, target).unwrap();
+        assert_eq!(
+            source.parameters().get("max_numeric_magnitude_bits"),
+            Some(bits)
+        );
+        check_reduced_parameters::<_, QUBO<i64>>(
+            source,
+            &["num_vars", "num_quadratic_terms"],
+            ParameterRelation::UpperBound,
+        );
+    }
+    for value in [i64::MIN, i64::MAX] {
+        let source = ClosestVectorProblem::new(vec![vec![value]], vec![value]).unwrap();
+        assert_eq!(
+            source.parameters().get("max_numeric_magnitude_bits"),
+            Some(if value == i64::MIN { 64 } else { 63 })
+        );
+    }
+}
+
+#[test]
+fn incongruence_pair_bounds_cover_prime_growth_and_repeated_literals() {
+    use crate::models::{
+        algebraic::SimultaneousIncongruences,
+        formula::{CNFClause, KSatisfiability},
+    };
+    use crate::variant::K3;
+    for variables in 0..=12 {
+        let clauses = if variables == 0 {
+            vec![]
+        } else {
+            vec![CNFClause::new(vec![1, 1, -1])]
+        };
+        check_reduced_parameters::<_, SimultaneousIncongruences>(
+            KSatisfiability::<K3>::new(variables, clauses),
+            &["num_pairs"],
+            ParameterRelation::UpperBound,
+        );
+    }
+}
+
+#[test]
+fn vertex_cover_lcs_transition_bounds_cover_empty_strings() {
+    use crate::models::{graph::MinimumVertexCover, misc::LongestCommonSubsequence};
+    use crate::{
+        topology::{Graph, SimpleGraph},
+        types::One,
+    };
+    for graph in [
+        SimpleGraph::empty(0),
+        SimpleGraph::empty(1),
+        SimpleGraph::path(3),
+    ] {
+        let weights = vec![One; graph.num_vertices()];
+        check_reduced_parameters::<_, LongestCommonSubsequence>(
+            MinimumVertexCover::new(graph, weights),
+            &["num_transitions"],
+            ParameterRelation::UpperBound,
+        );
+    }
+}