@@ -228,7 +228,7 @@ fields to issue templates. Changes to issue templates require user approval.
 ### Paper (docs/paper/reductions.typ)
 - `problem-def(name)[def][body]` — defines a problem with auto-generated schema, reductions list, and label `<def:ProblemName>`. Title comes from `display-name` dict.
 - `reduction-rule(source, target, example: bool, ...)[rule][proof]` — generates a theorem with label `<thm:Source-to-Target>` and registers in `covered-rules` state. Overhead auto-derived from JSON edge data.
-- Every directed reduction needs its own `reduction-rule` entry (except trivial Decision↔Optimization pairs which are auto-filtered)
+- Every directed reduction needs its own `reduction-rule` entry (except trivial Decision↔Optimization pairs and pure `One → i64 → f64` numeric casts, which are auto-filtered)
 - Completeness warnings auto-check that all JSON graph nodes/edges are covered in the paper; `Decision<P> ↔ P` edges are excluded since they are trivial solve-and-compare reductions
 - `display-name` dict maps `ProblemName` to display text
 
@@ -302,7 +302,7 @@ Also add to the `display-name` dictionary:
 ]
 ```
 
-Every directed reduction in the graph needs its own `reduction-rule` entry. The paper auto-checks completeness against the generated `reduction_graph.json` export.
+Every nontrivial directed reduction in the graph needs its own `reduction-rule` entry. Do not add paper explanations for pure `One → i64 → f64` numeric casts. Other same-model variant reductions, such as graph transformations and bounded-integer encodings, still require entries. The paper auto-checks completeness against the generated `reduction_graph.json` export.
 
 ## Complexity Verification Requirements
 
 
@@ -95,7 +95,7 @@ Traits and helpers: `src/rules/traits.rs`, `src/rules/test_helpers.rs`, `src/rul
    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).
+5. Paper `reduction-rule` entry — how-to-write-manual (adapt the how-to-verify proof, don't rewrite). Pure `One -> i64 -> f64` numeric casts are exempt; other same-model variant reductions still need entries.
 
 ## Traps
 
 
@@ -24,8 +24,8 @@ The paper `docs/paper/reductions.typ` is the mathematical manual: one `problem-d
 - `reduction-rule(source, target, example:, example-source-variant:, example-target-variant:,
   example-caption:, extra:)[statement][proof]` auto-derives overhead from the graph export and
   registers the edge for the completeness check; label `<thm:Source-to-Target>`.
-- Every directed reduction needs its own entry, including reverses. Only `Decision<P> <-> P` pairs are
-  exempt. The completeness warning block at the end of the paper lists missing edges; your change
+- Every directed reduction needs its own entry, including reverses. `Decision<P> <-> P` pairs and pure `One -> i64 -> f64` numeric casts are
+  exempt; do not explain numeric casts in the paper. Nontrivial same-model variant reductions still require entries. The completeness warning block at the end of the paper lists missing edges; your change
   must never increase it.
 
 ## Example data — never invent
 
@@ -3287,7 +3287,7 @@ In all graph problems below, $G = (V, E)$ denotes an undirected graph with $|V|
   ]
 }
 #{
-  let x = load-model-example("SteinerTree")
+  let x = load-model-example("SteinerTree", variant: (graph: "SimpleGraph", weight: "i64"))
   let nv = graph-num-vertices(x.instance)
   let ne = graph-num-edges(x.instance)
   let edges = x.instance.graph.edges
@@ -4451,7 +4451,7 @@ In all graph problems below, $G = (V, E)$ denotes an undirected graph with $|V|
 }
 
 #{
-  let x = load-model-example("ComparativeContainment")
+  let x = load-model-example("ComparativeContainment", variant: (weight: "i64"))
   let n = x.instance.universe_size
   let R = x.instance.r_sets
   let S = x.instance.s_sets
@@ -4994,7 +4994,7 @@ In all graph problems below, $G = (V, E)$ denotes an undirected graph with $|V|
     #problem-def("QUBO")[
       Given $n$ binary variables $x_i in {0, 1}$ and an upper-triangular matrix $Q$, minimize $f(bold(x)) = sum_(i=1)^n Q_(i i) x_i + sum_(i < j) Q_(i j) x_i x_j$ (using $x_i^2 = x_i$ for binary variables). The registered variants use either exact integer coefficients $Q in ZZ^(n times n)$ (the default) or finite floating-point coefficients $Q in RR^(n times n)$.
     ][
-    Equivalent to the Ising model via the linear substitution $s_i = 2x_i - 1$. The native formulation for quantum annealing hardware (e.g., D-Wave) and a standard target for penalty-method reductions @glover2019. QUBO unifies many combinatorial problems into a single unconstrained binary framework, making it a universal intermediate representation for quantum and classical optimization. The integer variant stores exact coefficients, the floating-point variant stores finite real coefficients, and their explicit reduction converts exactly representable integers through `i64_to_exact_f64`. The best known general algorithm runs in $O^*(2^n)$ by brute-force enumeration#footnote[QUBO inherits the Ising model's complexity; no algorithm improving on brute-force is known for the general case.].
+    Equivalent to the Ising model via the linear substitution $s_i = 2x_i - 1$. The native formulation for quantum annealing hardware (e.g., D-Wave) and a standard target for penalty-method reductions @glover2019. QUBO unifies many combinatorial problems into a single unconstrained binary framework, making it a universal intermediate representation for quantum and classical optimization. The integer variant stores exact coefficients, the floating-point variant stores finite real coefficients. The best known general algorithm runs in $O^*(2^n)$ by brute-force enumeration#footnote[QUBO inherits the Ising model's complexity; no algorithm improving on brute-force is known for the general case.].
 
     *Example.* Consider $n = #n$ with $Q = mat(#mat-rows)$. The objective is $f(bold(x)) = -x_1 - x_2 - x_3 + 2x_1 x_2 + 2x_2 x_3$. Evaluating all $2^#n$ assignments: $f(0,0,0) = 0$, $f(1,0,0) = -1$, $f(0,1,0) = -1$, $f(0,0,1) = -1$, $f(1,1,0) = 0$, $f(0,1,1) = 0$, $f(1,0,1) = -2$, $f(1,1,1) = 1$. The minimum is $f^* = #fstar$ at $bold(x)^* = (#fmt-values(xstar))$: selecting #selected.join(" and ") avoids the penalty terms #unselected-pairs.join(" and ").
 
@@ -16827,15 +16827,14 @@ See #link("https://github.com/CodingThrust/problem-reductions/blob/main/examples
 Problems parameterized by graph type, weight type, target type, or clause width ($k$) use explicit reductions between registered variants. Each rule constructs the target representation, registers an exact size map, and preserves the witness representation.
 
 #reduction-rule("MaximumIndependentSet", "MaximumIndependentSet")[
-  Explicit MIS variant reductions convert King's and triangular lattice graphs to unit-disk graphs, unit-disk graphs to simple adjacency graphs, and unit weights to integer weights. Every rule preserves the vertex indices and has an exact identity size map.
+  Explicit MIS variant reductions convert King's and triangular lattice graphs to unit-disk graphs, and unit-disk graphs to simple adjacency graphs. Every rule preserves the vertex indices and has an exact identity size map.
 ][
   _Construction._ The registered rules use these concrete maps:
   - _KingsSubgraph $arrow.r$ UnitDiskGraph:_ integer grid positions $(i, j)$ map to float coordinates with radius $r = 1.5$.
   - _TriangularSubgraph $arrow.r$ UnitDiskGraph:_ triangular lattice positions map to float coordinates with radius $r = 1.1$.
   - _UnitDiskGraph $arrow.r$ SimpleGraph:_ discard coordinates, retain only the adjacency edge list.
-  - _One $arrow.r$ i64:_ each unit weight maps to $1_ZZ$.
 
-  _Correctness._ Each graph conversion preserves the adjacency relation, and the weight conversion preserves every unit objective contribution as the integer one. Since the MIS objective $max sum_(v in S) w(v)$ depends only on adjacency and weights, feasible sets and their objective values are preserved.
+  _Correctness._ Each graph conversion preserves the adjacency relation. Since the MIS objective $max sum_(v in S) w(v)$ depends only on adjacency and weights, feasible sets and their objective values are preserved.
 
   _Solution extraction._ Return the target configuration unchanged (identity map on vertices).
 ]
@@ -16860,44 +16859,27 @@ Problems parameterized by graph type, weight type, target type, or clause width
   _Solution extraction._ Return the target configuration unchanged.
 ]
 
-#reduction-rule("SpinGlass", "SpinGlass")[
-  An Ising spin-glass instance with integer couplings and fields ($J_(i j), h_i in ZZ$) converts to the floating-point variant ($J_(i j), h_i in RR$) through exact `i64_to_exact_f64` embeddings. The graph topology is preserved.
-][
-  _Construction._ Given $"SpinGlass"(G, bold(J), bold(h))$ with $J_(i j) in ZZ$ and $h_i in ZZ$, construct $"SpinGlass"(G, bold(J)', bold(h)')$ with $J'_(i j) = J_(i j) in RR$ and $h'_i = h_i in RR$.
-
-  _Correctness._ The spin-glass Hamiltonian $H(bold(s)) = sum_((i,j) in E) J_(i j) s_i s_j + sum_i h_i s_i$ is preserved exactly under the integer-to-float embedding (no rounding). Spin configurations and the objective value are unchanged.
-
-  _Solution extraction._ Return the target configuration unchanged.
-]
-
-#reduction-rule("MaximumSetPacking", "MaximumSetPacking")[
-  A Maximum Set Packing instance converts unit weights to integer weights ($"One" arrow.r ZZ$) and integer weights to exactly represented floating weights ($ZZ arrow.r RR$). The set family and universe are preserved.
-][
-  _Construction._ Given $"MSP"(cal(S), bold(w))$, construct $"MSP"(cal(S), bold(w)')$ using:
-  - _One $arrow.r$ i64:_ each unit weight maps to $1_ZZ$.
-  - _i64 $arrow.r$ f64:_ each integer weight maps through `i64_to_exact_f64`.
-
-  _Correctness._ The packing constraint (no two selected sets share a universe element) depends only on set membership, not on weights. The objective $max sum_(i in P) w_i$ is preserved under the type embedding. Optimality is unchanged.
-
-  _Solution extraction._ Return the target configuration unchanged.
-]
-
-
-#reduction-rule("QUBO", "QUBO")[
-  An integer QUBO converts to the floating-coefficient variant by embedding every matrix coefficient with `i64_to_exact_f64`.
-][
-  _Construction._ Given $Q in ZZ^(n times n)$, construct $Q' in RR^(n times n)$ with $Q'_(i j) = "f64"(Q_(i j))$ for every exactly representable coefficient $|Q_(i j)| lt.eq 2^53 - 1$.
-
-  _Correctness._ For every binary vector $bold(x)$, exact coefficient conversion gives $bold(x)^top Q' bold(x) = bold(x)^top Q bold(x)$. The objective ordering and minimizers are preserved.
-
-  _Solution extraction._ Return the binary vector unchanged.
-]
 
 // Completeness check: warn about reduction rules in JSON but missing from paper
 #context {
   let covered = covered-rules.final()
   let json-edges = {
-    let edges = graph-data.edges.map(e => (graph-data.nodes.at(e.source).name, graph-data.nodes.at(e.target).name))
+    let is-numeric-cast(src, tgt) = {
+      src.name == tgt.name and ("weight", "coefficient").any(field => {
+        let from = src.variant.at(field, default: none)
+        let to = tgt.variant.at(field, default: none)
+        let promotion = (from == "One" and to == "i64") or (from == "i64" and to == "f64")
+        let promoted = src.variant
+        promoted.insert(field, to)
+        promotion and promoted == tgt.variant
+      })
+    }
+    let source = (name: "MaximumIndependentSet", variant: (graph: "SimpleGraph", weight: "One"))
+    assert(is-numeric-cast(source, (name: source.name, variant: (graph: "SimpleGraph", weight: "i64"))))
+    assert(not is-numeric-cast(source, (name: source.name, variant: (graph: "TriangularSubgraph", weight: "i64"))))
+    let edges = graph-data.edges.filter(e => {
+      not is-numeric-cast(graph-data.nodes.at(e.source), graph-data.nodes.at(e.target))
+    }).map(e => (graph-data.nodes.at(e.source).name, graph-data.nodes.at(e.target).name))
     let unique = ()
     for e in edges {
       if unique.find(u => u.at(0) == e.at(0) and u.at(1) == e.at(1)) == none {
@@ -17149,13 +17131,13 @@ The following table shows concrete target-variable counts for example instances,
 // === Non-ILP reduction rules ===
 
 #reduction-rule("ILP", "ILP")[
-  ILP variants convert between binary and bounded integer variable domains and between exact-integer and floating-point coefficients. The independent bounds dimension defaults to general; the bounded integer variant requires finite lower and upper endpoints for every variable. Binary variables embed into bounded integer ILP, which embeds into general integer ILP while retaining all stored bounds. A bounded integer variable is encoded by binary variables with truncated positional weights. Integer coefficients are embedded only when every stored coefficient and right-hand side has an exact `f64` representation.
+  ILP variants convert between binary and bounded integer variable domains. The independent bounds dimension defaults to general; the bounded integer variant requires finite lower and upper endpoints for every variable. Binary variables embed into bounded integer ILP, which embeds into general integer ILP while retaining all stored bounds. A bounded integer variable is encoded by binary variables with truncated positional weights.
 ][
-  _Construction._ For the binary-to-bounded-integer and bounded-to-general edges, copy the variables, constraints, objective, and optimization direction unchanged. For an integer variable $x_i in [L_i, U_i]$, let $D_i = U_i - L_i$ and choose positive truncated binary weights $w_(i j)$ whose subset sums represent every integer from $0$ through $D_i$; substitute $x_i = L_i + sum_j w_(i j)y_(i j)$ into every constraint and objective term. This edge is registered only for the bounded integer variant; its constructor requires two finite bounds for every variable. For the coefficient edge, copy the variable bounds and optimization direction and convert each entry of the constraint matrix, right-hand side, and objective independently; reject the instance if any integer lies outside the exactly representable `f64` integer range.
+  _Construction._ For the binary-to-bounded-integer and bounded-to-general edges, copy the variables, constraints, objective, and optimization direction unchanged. For an integer variable $x_i in [L_i, U_i]$, let $D_i = U_i - L_i$ and choose positive truncated binary weights $w_(i j)$ whose subset sums represent every integer from $0$ through $D_i$; substitute $x_i = L_i + sum_j w_(i j)y_(i j)$ into every constraint and objective term. This edge is registered only for the bounded integer variant; its constructor requires two finite bounds for every variable.
 
-  _Correctness._ The binary-to-bounded-integer and bounded-to-general embeddings change no mathematical expression. For bounded integer variables, every $x_i in [L_i,U_i]$ has a truncated binary representation, and every binary assignment decodes inside that interval; substitution preserves all constraints and changes the stored objective only by the constant lower-bound contribution, so optimal assignments are preserved. Exact conversion preserves every stored coefficient, so it constructs the same formal linear objective and constraints over the same integer variables.
+  _Correctness._ The binary-to-bounded-integer and bounded-to-general embeddings change no mathematical expression. For bounded integer variables, every $x_i in [L_i,U_i]$ has a truncated binary representation, and every binary assignment decodes inside that interval; substitution preserves all constraints and changes the stored objective only by the constant lower-bound contribution, so optimal assignments are preserved.
 
-  _Solution extraction._ Binary-to-bounded-integer, bounded-to-general, and coefficient conversions preserve the assignment; coefficient conversion additionally checks the assignment against the source integer ILP. Binary encoding returns $x_i = L_i + sum_j w_(i j)y_(i j)$.
+  _Solution extraction._ Binary-to-bounded-integer and bounded-to-general conversions preserve the assignment. Binary encoding returns $x_i = L_i + sum_j w_(i j)y_(i j)$.
 ]
 
 #let hc_hp = load-example("HamiltonianCircuit", "HamiltonianPath")
 
@@ -364,19 +364,30 @@ crate::register_brute_force! {
 
 #[cfg(feature = "example-db")]
 pub(crate) fn canonical_model_example_specs() -> Vec<crate::example_db::specs::ModelExampleSpec> {
-    vec![crate::example_db::specs::ModelExampleSpec {
-        id: "steiner_tree_simplegraph",
-        instance: Box::new(SteinerTree::new(
-            SimpleGraph::new(
-                5,
-                vec![(0, 1), (0, 3), (1, 2), (1, 3), (2, 3), (2, 4), (3, 4)],
-            ),
-            vec![2, 5, 2, 1, 5, 6, 1],
-            vec![0, 2, 4],
-        )),
-        optimal_config: serde_json::json!(vec![true, false, true, true, false, false, true]),
-        optimal_value: serde_json::json!(6),
-    }]
+    vec![
+        crate::example_db::specs::ModelExampleSpec {
+            id: "steiner_tree_simplegraph",
+            instance: Box::new(SteinerTree::new(
+                SimpleGraph::new(
+                    5,
+                    vec![(0, 1), (0, 3), (1, 2), (1, 3), (2, 3), (2, 4), (3, 4)],
+                ),
+                vec![2, 5, 2, 1, 5, 6, 1],
+                vec![0, 2, 4],
+            )),
+            optimal_config: serde_json::json!(vec![true, false, true, true, false, false, true]),
+            optimal_value: serde_json::json!(6),
+        },
+        crate::example_db::specs::ModelExampleSpec {
+            id: "steiner_tree_one",
+            instance: Box::new(SteinerTree::<SimpleGraph, One>::unit_weights(
+                SimpleGraph::path(3),
+                vec![0, 2],
+            )),
+            optimal_config: serde_json::json!([true, true]),
+            optimal_value: serde_json::json!(2),
+        },
+    ]
 }
 
 #[cfg(test)]
 
@@ -366,21 +366,31 @@ fn contains_selected_subset_unchecked(config: &[bool], set: &[usize]) -> bool {
 
 #[cfg(feature = "example-db")]
 pub(crate) fn canonical_model_example_specs() -> Vec<crate::example_db::specs::ModelExampleSpec> {
-    vec![crate::example_db::specs::ModelExampleSpec {
-        id: "comparative_containment",
-        instance: Box::new(
-            ComparativeContainment::with_weights(
-                4,
-                vec![vec![0, 1, 2, 3], vec![0, 1]],
-                vec![vec![0, 1, 2, 3], vec![2, 3]],
-                vec![2, 5],
-                vec![3, 6],
-            )
-            .expect("canonical comparative-containment instance must be valid"),
-        ),
-        optimal_config: serde_json::json!(vec![false, true, false, false]),
-        optimal_value: serde_json::json!(true),
-    }]
+    vec![
+        crate::example_db::specs::ModelExampleSpec {
+            id: "comparative_containment",
+            instance: Box::new(
+                ComparativeContainment::with_weights(
+                    4,
+                    vec![vec![0, 1, 2, 3], vec![0, 1]],
+                    vec![vec![0, 1, 2, 3], vec![2, 3]],
+                    vec![2, 5],
+                    vec![3, 6],
+                )
+                .expect("canonical comparative-containment instance must be valid"),
+            ),
+            optimal_config: serde_json::json!(vec![false, true, false, false]),
+            optimal_value: serde_json::json!(true),
+        },
+        crate::example_db::specs::ModelExampleSpec {
+            id: "comparative_containment_one",
+            instance: Box::new(
+                ComparativeContainment::<One>::new(2, vec![vec![0]], vec![vec![1]]).unwrap(),
+            ),
+            optimal_config: serde_json::json!([true, false]),
+            optimal_value: serde_json::json!(true),
+        },
+    ]
 }
 
 #[cfg(test)]