diff --git a/docs/paper/reductions.typ b/docs/paper/reductions.typ
index 8e0462b7a..dc1959a8d 100644
--- a/docs/paper/reductions.typ
+++ b/docs/paper/reductions.typ
@@ -17661,6 +17661,126 @@ The following table shows concrete target-variable counts for example instances,
   _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)$.
 ]
 
+// Reduction: HamiltonianPath -> HamiltonianCircuit
+#let hp_hc = load-example("HamiltonianPath", "HamiltonianCircuit")
+#let hp_hc_sol = hp_hc.solutions.at(0)
+#let hp_hc_n = graph-num-vertices(hp_hc.source.instance)
+#let hp_hc_edges = hp_hc.source.instance.graph.edges
+#let hp_hc_target_n = graph-num-vertices(hp_hc.target.instance)
+#let hp_hc_target_edges = hp_hc.target.instance.graph.edges
+#let hp_hc_has_edge(edges, u, v) = edges.any(e => e.contains(u) and e.contains(v))
+#let hp_hc_x = hp_hc_n
+#assert(hp_hc_n >= 2)
+#assert(hp_hc_target_n == hp_hc_n + 1)
+#assert(hp_hc_target_edges.len() == hp_hc_edges.len() + hp_hc_n)
+#assert(hp_hc_sol.source_config.sorted() == range(hp_hc_n))
+#assert(hp_hc_sol.target_config.sorted() == range(hp_hc_target_n))
+#assert(range(hp_hc_n - 1).all(i => hp_hc_has_edge(
+  hp_hc_edges, hp_hc_sol.source_config.at(i), hp_hc_sol.source_config.at(i + 1))))
+#assert(range(hp_hc_target_n).all(i => hp_hc_has_edge(
+  hp_hc_target_edges, hp_hc_sol.target_config.at(i),
+  hp_hc_sol.target_config.at(calc.rem(i + 1, hp_hc_target_n)))))
+#assert(range(hp_hc_n).all(v => hp_hc_has_edge(hp_hc_target_edges, v, hp_hc_x)))
+#assert(hp_hc_target_edges.filter(e => not e.contains(hp_hc_x)).len() == hp_hc_edges.len())
+#assert(hp_hc_edges.all(e => hp_hc_has_edge(hp_hc_target_edges, e.at(0), e.at(1))))
+#let hp_hc_pivot = hp_hc_sol.target_config.position(v => v == hp_hc_x)
+#let hp_hc_extracted = hp_hc_sol.target_config.slice(hp_hc_pivot + 1) + hp_hc_sol.target_config.slice(0, hp_hc_pivot)
+#assert(hp_hc_extracted == hp_hc_sol.source_config)
+// Obtain the negative companion by retaining a star from the source fixture.
+#let hp_hc_no_n = hp_hc_n - 1
+#let hp_hc_no_vertices = range(hp_hc_no_n)
+#let hp_hc_no_center = hp_hc_sol.source_config.at(1)
+#let hp_hc_no_leaves = hp_hc_no_vertices.filter(v => v != hp_hc_no_center)
+#let hp_hc_no_edges = hp_hc_edges.filter(e =>
+  e.all(v => hp_hc_no_vertices.contains(v)) and e.contains(hp_hc_no_center))
+#assert(hp_hc_no_vertices.contains(hp_hc_no_center))
+#assert(hp_hc_no_leaves.len() >= 3)
+#assert(hp_hc_no_edges.len() == hp_hc_no_leaves.len())
+#assert(hp_hc_no_leaves.all(v => hp_hc_has_edge(hp_hc_no_edges, v, hp_hc_no_center)))
+#let hp_hc_no_target_edges = hp_hc_target_edges.filter(e =>
+  e.all(v => hp_hc_no_vertices.contains(v) or v == hp_hc_x) and
+  (e.contains(hp_hc_no_center) or e.contains(hp_hc_x))
+).map(e => e.map(v => if v == hp_hc_x { hp_hc_no_n } else { v }))
+#assert(hp_hc_no_target_edges.len() == hp_hc_no_edges.len() + hp_hc_no_n)
+#assert(hp_hc_no_leaves.all(v => hp_hc_no_target_edges.filter(e => e.contains(v)).len() == 2))
+#reduction-rule("HamiltonianPath", "HamiltonianCircuit",
+  example: true,
+  example-caption: [Add a universal vertex to a path on #hp_hc_n vertices],
+  extra: [
+    #pred-commands(
+      "pred create --example " + rule-spec(hp_hc) + " -o hp.json",
+      "pred reduce hp.json --via route.json -o bundle.json",
+      "pred solve bundle.json",
+      "pred evaluate hp.json --config " + cli-config(hp_hc_sol.source_config),
+    )
+
+    *YES example -- source.* The fixture has $n = #hp_hc_n$ vertices and
+    $m = #hp_hc_edges.len()$ edges: #hp_hc_edges.map(e => $(#e.at(0), #e.at(1))$).join(", ").
+    Its satisfying path is $[#fmt-values(hp_hc_sol.source_config)]$.
+
+    *Construction and round trip.* Add vertex $x = #hp_hc_x$ and its
+    #hp_hc_n spokes. The resulting graph has #hp_hc_target_n vertices and
+    #hp_hc_target_edges.len() edges:
+    #hp_hc_target_edges.map(e => $(#e.at(0), #e.at(1))$).join(", ").
+    The global bounds evaluate to $#(hp_hc_n + 3)$ vertices and
+    $#(hp_hc_edges.len() + hp_hc_n + 3)$ edges. The target ordering
+    $[#fmt-values(hp_hc_sol.target_config)]$ has all consecutive edges,
+    including its implicit closing edge
+    $(#hp_hc_sol.target_config.last(), #hp_hc_sol.target_config.first())$.
+    Rotating around $x$ and deleting it gives $[#fmt-values(hp_hc_extracted)]$.
+
+    *NO companion.* Restrict the source fixture to vertices
+    ${#fmt-values(hp_hc_no_vertices)}$ and retain only edges incident to
+    $#hp_hc_no_center$: #hp_hc_no_edges.map(e => $(#e.at(0), #e.at(1))$).join(", ").
+    This is a star with #hp_hc_no_n vertices, #hp_hc_no_edges.len() edges,
+    and #hp_hc_no_leaves.len() leaves. Every leaf would have to be a path
+    endpoint, but a path has only two endpoints, so this source is NO.
+    Its reduction adds $x = #hp_hc_no_n$, giving $#(hp_hc_no_n + 1)$ vertices
+    and #hp_hc_no_target_edges.len() edges:
+    #hp_hc_no_target_edges.map(e => $(#e.at(0), #e.at(1))$).join(", ").
+    The global bounds are $#(hp_hc_no_n + 3)$ and
+    $#(hp_hc_no_edges.len() + hp_hc_no_n + 3)$.
+    Each old leaf has exactly the two neighbors $#hp_hc_no_center$ and
+    $#hp_hc_no_n$. A circuit would force #hp_hc_no_leaves.len() used edges
+    at the old center, exceeding circuit degree two. The target is therefore NO.
+  ],
+)[
+  Add a universal vertex to turn a Hamiltonian path into a Hamiltonian circuit.
+  This is the undirected specialization of the directed construction in
+  @Waggoner2025NPCompleteness (Example problem, Sample solution), extended
+  below to the empty and singleton source conventions. Construction takes
+  $O(n+m+1)$ time and space.
+][
+  _Construction._ Let $G=(V,E)$ be a loopless simple undirected graph, with
+  $V={0,dots,n-1}$, $n=|V|$ and $m=|E|$. For $n<2$, return the fixed triangle
+  on ${0,1,2}$. Otherwise introduce $x=n$ and construct
+  $H=(V union {x}, E union {{v,x}:v in V})$. This adds no old-to-old edge.
+  The exact target sizes are $(3,3)$ for $n<2$ and $(n+1,m+n)$ otherwise.
+  Hence the registered global upper bounds are $n+3$ vertices and $m+n+3$
+  edges. Derived machine sizes, including graph index limits, are checked before allocation and graph
+  construction uses the fallible constructor. Loops and parallel edges are
+  rejected by the source model.
+
+  _Correctness._ ($arrow.r.double$) For $n<2$, the source's empty or singleton
+  ordering is satisfying and the triangle is YES. For $n>=2$, a source path
+  $(v_0,dots,v_(n-1))$ extends to circuit ordering $(x,v_0,dots,v_(n-1))$:
+  its first and closing edges are spokes and every other edge belongs to $E$.
+  ($arrow.l.double$) For $n<2$, the source is YES by its model convention.
+  Otherwise any target circuit visits $x$ once. Rotate to $x$ and remove it;
+  the remaining ordering contains every old vertex once and all consecutive
+  edges have old endpoints, so they belong to $E$. It is a source path.
+  Both orientations and all rotations satisfy this argument. In particular,
+  two isolated source vertices remain NO, a single source edge produces a
+  triangle, and disconnected sources with $n>=2$ remain NO.
+
+  _Solution extraction._ Validate the target ordering once, rejecting malformed
+  or nonsatisfying configurations, including in the small-order branch.
+  For $n<2$, return `[]` or `[0]`. Otherwise locate $x=n$ at position $k$ and
+  return the suffix after $k$ followed by the prefix before $k$. Circuit
+  orderings have no repeated closing vertex. Completed `Or` values map
+  identically; witness counts are not asserted to be preserved.
+]
+
 #let hc_hp = load-example("HamiltonianCircuit", "HamiltonianPath")
 #let hc_hp_sol = hc_hp.solutions.at(0)
 #let hc_hp_n = graph-num-vertices(hc_hp.source.instance)
diff --git a/docs/paper/references.bib b/docs/paper/references.bib
index 0dda81fd2..edcd2f4f5 100644
--- a/docs/paper/references.bib
+++ b/docs/paper/references.bib
@@ -2342,6 +2342,15 @@ @article{axler2019
   url = {https://www.maths.tcd.ie/EMIS/journals/JIS/VOL22/Axler/axler17.pdf}
 }
 
+@misc{Waggoner2025NPCompleteness,
+  author = {Waggoner, Bowen},
+  title = {Standard 21: P and NP 2: NP-Completeness},
+  year = {2025},
+  howpublished = {University of Colorado Boulder course notes},
+  url = {https://bowaggoner.com/courses/2025/csci3104/book/standards/21-pnp-complete.html},
+  note = {Example problem, Sample solution; accessed 2026-11-03}
+}
+
 @article{een2006,
   author = {Niklas E{\'e}n and Niklas S{\"o}rensson},
   title = {Translating Pseudo-Boolean Constraints into {SAT}},
diff --git a/src/rules/hamiltonianpath_hamiltoniancircuit.rs b/src/rules/hamiltonianpath_hamiltoniancircuit.rs
new file mode 100644
index 000000000..1cf631b4b
--- /dev/null
+++ b/src/rules/hamiltonianpath_hamiltoniancircuit.rs
@@ -0,0 +1,125 @@
+//! Reduction from HamiltonianPath to HamiltonianCircuit.
+//!
+//! Add a vertex adjacent to every source vertex. Rotating a target circuit
+//! around that vertex and deleting it recovers a source path. Empty and
+//! singleton sources instead produce a triangle to respect circuit semantics.
+
+use crate::models::graph::{HamiltonianCircuit, HamiltonianPath};
+use crate::rules::{ReduceTo, ReductionError, ReductionResult};
+use crate::topology::{Graph, SimpleGraph};
+
+/// Stores the target circuit problem and the original ordering length.
+#[derive(Debug, Clone)]
+pub struct ReductionHamiltonianPathToHamiltonianCircuit {
+    target: HamiltonianCircuit<SimpleGraph>,
+    num_original_vertices: usize,
+}
+
+impl ReductionResult for ReductionHamiltonianPathToHamiltonianCircuit {
+    type Source = HamiltonianPath<SimpleGraph>;
+    type Target = HamiltonianCircuit<SimpleGraph>;
+
+    fn target_problem(&self) -> &Self::Target {
+        &self.target
+    }
+
+    fn extract_solution(
+        &self,
+        target_solution: &Vec<usize>,
+    ) -> crate::rules::ExtractionResult<Vec<usize>> {
+        crate::rules::traits::validate_target_witness(
+            self.target_problem(),
+            target_solution,
+            |value| value.0,
+            "target witness is not satisfying",
+        )?;
+
+        let n = self.num_original_vertices;
+        if n < 2 {
+            return Ok((0..n).collect());
+        }
+        let pivot = target_solution
+            .iter()
+            .position(|&vertex| vertex == n)
+            .expect("validated circuit contains the added vertex");
+        Ok(target_solution[pivot + 1..]
+            .iter()
+            .chain(&target_solution[..pivot])
+            .copied()
+            .collect())
+    }
+}
+
+#[crate::aggregate_reduction(identity)]
+impl crate::rules::AggregateReductionResult for ReductionHamiltonianPathToHamiltonianCircuit {}
+
+// The small-order branch has three vertices and edges; otherwise the exact
+// counts are n+1 and m+n, since all spokes are distinct from old edges.
+#[crate::reduction(transform = upper_bound {
+    num_vertices = "num_vertices + 3",
+    num_edges = "num_edges + num_vertices + 3",
+})]
+impl ReduceTo<HamiltonianCircuit<SimpleGraph>> for HamiltonianPath<SimpleGraph> {
+    type Result = ReductionHamiltonianPathToHamiltonianCircuit;
+
+    fn reduce_to(&self) -> Result<Self::Result, ReductionError> {
+        let n = self.num_vertices();
+        let (num_vertices, num_edges) = checked_target_sizes(n, self.num_edges())?;
+        let edges = if n < 2 {
+            vec![(0, 1), (0, 2), (1, 2)]
+        } else {
+            let mut edges = Vec::with_capacity(num_edges);
+            edges.extend(self.graph().edges());
+            edges.extend((0..n).map(|v| (v, n)));
+            edges
+        };
+        let graph = SimpleGraph::try_new(num_vertices, edges)
+            .map_err(<Self as ReduceTo<HamiltonianCircuit<SimpleGraph>>>::target_construction)?;
+        Ok(ReductionHamiltonianPathToHamiltonianCircuit {
+            target: HamiltonianCircuit::new(graph),
+            num_original_vertices: n,
+        })
+    }
+}
+
+fn checked_target_sizes(n: usize, m: usize) -> Result<(usize, usize), ReductionError> {
+    if n < 2 {
+        return Ok((3, 3));
+    }
+    let overflow = || {
+        ReductionError::integer_overflow::<
+            HamiltonianPath<SimpleGraph>,
+            HamiltonianCircuit<SimpleGraph>,
+        >("computing target graph sizes")
+    };
+    let vertices = n.checked_add(1).ok_or_else(overflow)?;
+    let edges = m.checked_add(n).ok_or_else(overflow)?;
+    // SimpleGraph uses petgraph's default index domain for both nodes and edges.
+    petgraph::graph::DefaultIx::try_from(vertices).map_err(|_| overflow())?;
+    petgraph::graph::DefaultIx::try_from(edges).map_err(|_| overflow())?;
+    Ok((vertices, edges))
+}
+
+#[cfg(feature = "example-db")]
+pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::RuleExampleSpec> {
+    vec![crate::example_db::specs::RuleExampleSpec {
+        id: "hamiltonianpath_to_hamiltoniancircuit",
+        build: || {
+            let source = HamiltonianPath::new(SimpleGraph::new(
+                5,
+                vec![(0, 1), (1, 2), (2, 3), (3, 4), (0, 2), (1, 3)],
+            ));
+            crate::example_db::specs::rule_example_with_witness::<_, HamiltonianCircuit<SimpleGraph>>(
+                source,
+                crate::export::SolutionPair {
+                    source_config: serde_json::json!([0, 1, 2, 3, 4]),
+                    target_config: serde_json::json!([5, 0, 1, 2, 3, 4]),
+                },
+            )
+        },
+    }]
+}
+
+#[cfg(test)]
+#[path = "../unit_tests/rules/hamiltonianpath_hamiltoniancircuit.rs"]
+mod tests;
diff --git a/src/rules/mod.rs b/src/rules/mod.rs
index 7606f4923..07017137c 100644
--- a/src/rules/mod.rs
+++ b/src/rules/mod.rs
@@ -59,6 +59,7 @@ pub(crate) mod hamiltoniancircuit_stackercrane;
 pub(crate) mod hamiltoniancircuit_strongconnectivityaugmentation;
 pub(crate) mod hamiltoniancircuit_travelingsalesman;
 pub(crate) mod hamiltonianpath_degreeconstrainedspanningtree;
+pub(crate) mod hamiltonianpath_hamiltoniancircuit;
 pub(crate) mod hamiltonianpath_isomorphicspanningtree;
 pub(crate) mod hamiltonianpathbetweentwovertices_longestpath;
 pub(crate) mod ilp_casts;
@@ -396,6 +397,7 @@ pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::Ru
     specs.extend(hamiltoniancircuit_strongconnectivityaugmentation::canonical_rule_example_specs());
     specs.extend(hamiltoniancircuit_travelingsalesman::canonical_rule_example_specs());
     specs.extend(hamiltonianpath_degreeconstrainedspanningtree::canonical_rule_example_specs());
+    specs.extend(hamiltonianpath_hamiltoniancircuit::canonical_rule_example_specs());
     specs.extend(graphpartitioning_maxcut::canonical_rule_example_specs());
     specs.extend(graphpartitioning_qubo::canonical_rule_example_specs());
     specs.extend(hamiltonianpathbetweentwovertices_longestpath::canonical_rule_example_specs());
diff --git a/src/unit_tests/rules/hamiltonianpath_hamiltoniancircuit.rs b/src/unit_tests/rules/hamiltonianpath_hamiltoniancircuit.rs
new file mode 100644
index 000000000..3fc28e6e0
--- /dev/null
+++ b/src/unit_tests/rules/hamiltonianpath_hamiltoniancircuit.rs
@@ -0,0 +1,285 @@
+use super::{ReductionHamiltonianPathToHamiltonianCircuit, checked_target_sizes};
+use crate::models::graph::{HamiltonianCircuit, HamiltonianPath};
+use crate::rules::test_helpers::{
+    assert_parameter_predictions, assert_satisfaction_round_trip_from_satisfaction_target,
+};
+use crate::rules::{AggregateReductionResult, ReduceTo, ReductionError, ReductionResult};
+use crate::solvers::BruteForce;
+use crate::topology::{Graph, SimpleGraph};
+use crate::traits::Problem;
+use crate::types::Or;
+use std::collections::BTreeSet;
+
+fn example_source() -> HamiltonianPath<SimpleGraph> {
+    HamiltonianPath::new(SimpleGraph::new(
+        5,
+        vec![(0, 1), (1, 2), (2, 3), (3, 4), (0, 2), (1, 3)],
+    ))
+}
+
+fn reduce(source: &HamiltonianPath<SimpleGraph>) -> ReductionHamiltonianPathToHamiltonianCircuit {
+    ReduceTo::<HamiltonianCircuit<SimpleGraph>>::reduce_to(source)
+        .expect("reduction should succeed")
+}
+
+#[test]
+fn test_hamiltonianpath_to_hamiltoniancircuit_closed_loop() {
+    let source = example_source();
+    assert_satisfaction_round_trip_from_satisfaction_target(
+        &source,
+        &reduce(&source),
+        "HamiltonianPath -> HamiltonianCircuit",
+    );
+}
+
+#[test]
+#[cfg(feature = "example-db")]
+fn test_hamiltonianpath_to_hamiltoniancircuit_paper_example() {
+    let example = (super::canonical_rule_example_specs()[0].build)();
+    let source: HamiltonianPath<SimpleGraph> =
+        serde_json::from_value(example.source.instance).unwrap();
+    let target: HamiltonianCircuit<SimpleGraph> =
+        serde_json::from_value(example.target.instance).unwrap();
+    let reduction = reduce(&source);
+    assert_eq!((target.num_vertices(), target.num_edges()), (6, 11));
+    let edges: BTreeSet<_> = target
+        .graph()
+        .edges()
+        .into_iter()
+        .map(|(u, v)| (u.min(v), u.max(v)))
+        .collect();
+    assert_eq!(
+        edges,
+        BTreeSet::from([
+            (0, 1),
+            (0, 2),
+            (0, 5),
+            (1, 2),
+            (1, 3),
+            (1, 5),
+            (2, 3),
+            (2, 5),
+            (3, 4),
+            (3, 5),
+            (4, 5),
+        ])
+    );
+    let cycle: Vec<usize> =
+        serde_json::from_value(example.solutions[0].target_config.clone()).unwrap();
+    let path: Vec<usize> =
+        serde_json::from_value(example.solutions[0].source_config.clone()).unwrap();
+    assert_eq!(cycle, vec![5, 0, 1, 2, 3, 4]);
+    assert_eq!(path, vec![0, 1, 2, 3, 4]);
+    assert_eq!(source.evaluate(&path).unwrap(), Or(true));
+    assert_eq!(target.evaluate(&cycle).unwrap(), Or(true));
+    assert_eq!(reduction.extract_solution(&cycle).unwrap(), path);
+    assert_parameter_predictions(&source, &reduction);
+}
+
+#[test]
+fn extraction_handles_both_orientations_and_every_rotation() {
+    let source = example_source();
+    let reduction = reduce(&source);
+    for (mut cycle, expected) in [
+        (vec![5, 0, 1, 2, 3, 4], vec![0, 1, 2, 3, 4]),
+        (vec![5, 4, 3, 2, 1, 0], vec![4, 3, 2, 1, 0]),
+    ] {
+        for _ in 0..cycle.len() {
+            let path = reduction.extract_solution(&cycle).unwrap();
+            assert_eq!(path, expected);
+            assert_eq!(source.evaluate(&path).unwrap(), Or(true));
+            cycle.rotate_left(1);
+        }
+    }
+}
+
+#[test]
+fn empty_and_singleton_paths_reduce_to_a_triangle() {
+    for n in 0..2 {
+        let source = HamiltonianPath::new(SimpleGraph::empty(n));
+        let reduction = reduce(&source);
+        let target = ReductionResult::target_problem(&reduction);
+        assert_eq!((target.num_vertices(), target.num_edges()), (3, 3));
+        assert_parameter_predictions(&source, &reduction);
+        let witnesses = BruteForce::new().find_all_witnesses(target).unwrap();
+        assert_eq!(witnesses.len(), 6);
+        for cycle in witnesses {
+            let path = reduction.extract_solution(&cycle).unwrap();
+            assert_eq!(path, (0..n).collect::<Vec<_>>());
+            assert_eq!(source.evaluate(&path).unwrap(), Or(true));
+        }
+        for invalid in [vec![], vec![0, 1], vec![0, 0, 0], vec![0, 1, 3]] {
+            assert!(reduction.extract_solution(&invalid).is_err());
+        }
+    }
+}
+
+#[test]
+fn exhaustive_simple_graphs_preserve_feasibility_and_every_witness() {
+    let solver = BruteForce::new();
+    let mut count = 0;
+    for n in 0..=4 {
+        let pairs: Vec<_> = (0..n)
+            .flat_map(|u| (u + 1..n).map(move |v| (u, v)))
+            .collect();
+        for mask in 0..(1usize << pairs.len()) {
+            let edges = pairs
+                .iter()
+                .enumerate()
+                .filter_map(|(i, &e)| (mask & (1 << i) != 0).then_some(e))
+                .collect();
+            let source = HamiltonianPath::new(SimpleGraph::new(n, edges));
+            let reduction = reduce(&source);
+            let target = ReductionResult::target_problem(&reduction);
+            let paths: BTreeSet<_> = solver
+                .find_all_witnesses(&source)
+                .unwrap()
+                .into_iter()
+                .collect();
+            let cycles = solver.find_all_witnesses(target).unwrap();
+            assert_eq!(paths.is_empty(), cycles.is_empty(), "n={n}, mask={mask}");
+            assert_eq!(
+                AggregateReductionResult::extract_value(&reduction, Or(!cycles.is_empty())),
+                Or(!paths.is_empty()),
+            );
+            let extracted: BTreeSet<_> = cycles
+                .iter()
+                .map(|cycle| reduction.extract_solution(cycle).unwrap())
+                .collect();
+            assert_eq!(extracted, paths, "n={n}, mask={mask}");
+            assert_parameter_predictions(&source, &reduction);
+            count += 1;
+        }
+    }
+    assert_eq!(count, 76);
+}
+
+#[test]
+fn isolated_vertices_disconnected_graphs_and_stars_remain_infeasible() {
+    for graph in [
+        SimpleGraph::empty(2),
+        SimpleGraph::new(4, vec![(0, 1), (2, 3)]),
+        SimpleGraph::new(4, vec![(0, 1), (0, 2), (0, 3)]),
+    ] {
+        let source = HamiltonianPath::new(graph);
+        let reduction = reduce(&source);
+        let target = ReductionResult::target_problem(&reduction);
+        assert!(BruteForce::new().solve(&source).unwrap().is_none());
+        assert!(BruteForce::new().solve(target).unwrap().is_none());
+        assert_eq!(
+            AggregateReductionResult::extract_value(&reduction, Or(false)),
+            Or(false)
+        );
+        assert!(
+            reduction
+                .extract_solution(&(0..target.num_vertices()).collect())
+                .is_err()
+        );
+    }
+}
+
+#[test]
+fn a_single_edge_and_reversed_edge_records_are_preserved() {
+    for graph in [
+        SimpleGraph::new(2, vec![(1, 0)]),
+        SimpleGraph::new(5, vec![(4, 3), (2, 1), (3, 2), (1, 0), (2, 0)]),
+    ] {
+        let source = HamiltonianPath::new(graph);
+        let reduction = reduce(&source);
+        let target = ReductionResult::target_problem(&reduction);
+        let n = source.num_vertices();
+        assert_eq!(
+            (target.num_vertices(), target.num_edges()),
+            (n + 1, source.num_edges() + n)
+        );
+        for u in 0..n {
+            assert!(target.graph().has_edge(u, n));
+            for v in 0..n {
+                assert_eq!(target.graph().has_edge(u, v), source.graph().has_edge(u, v));
+            }
+        }
+        assert_eq!(
+            source
+                .evaluate(&reduction.extract_solution(&(0..=n).collect()).unwrap())
+                .unwrap(),
+            Or(true)
+        );
+    }
+}
+
+#[test]
+fn extraction_rejects_wrong_lengths() {
+    let reduction = reduce(&example_source());
+    for invalid in [vec![], vec![5, 0, 1, 2, 3], vec![5, 0, 1, 2, 3, 4, 5]] {
+        assert!(reduction.extract_solution(&invalid).is_err(), "{invalid:?}");
+    }
+}
+
+#[test]
+fn extraction_rejects_out_of_range_labels() {
+    assert!(
+        reduce(&example_source())
+            .extract_solution(&vec![6, 0, 1, 2, 3, 4])
+            .is_err()
+    );
+}
+
+#[test]
+fn extraction_rejects_repeated_vertices() {
+    assert!(
+        reduce(&example_source())
+            .extract_solution(&vec![5, 0, 1, 2, 3, 3])
+            .is_err()
+    );
+}
+
+#[test]
+fn extraction_rejects_missing_edges() {
+    assert!(
+        reduce(&example_source())
+            .extract_solution(&vec![5, 0, 4, 3, 2, 1])
+            .is_err()
+    );
+}
+
+#[test]
+fn source_graph_construction_and_loading_reject_non_simple_edges() {
+    for edges in [vec![(0, 0)], vec![(0, 1), (0, 1)], vec![(0, 1), (1, 0)]] {
+        assert!(SimpleGraph::try_new(2, edges.clone()).is_err());
+        let data = serde_json::json!({"graph": {"num_vertices": 2, "edges": edges}});
+        assert!(serde_json::from_value::<HamiltonianPath<SimpleGraph>>(data).is_err());
+    }
+}
+
+#[test]
+fn target_sizes_reject_petgraph_index_overflow() {
+    let limit = usize::try_from(petgraph::graph::DefaultIx::MAX).unwrap();
+    assert!(matches!(
+        checked_target_sizes(limit, 0),
+        Err(ReductionError::IntegerOverflow { .. })
+    ));
+    assert!(matches!(
+        checked_target_sizes(2, limit - 1),
+        Err(ReductionError::IntegerOverflow { .. })
+    ));
+}
+
+#[test]
+fn target_size_arithmetic_accepts_limits_and_rejects_overflow() {
+    let limit = usize::try_from(petgraph::graph::DefaultIx::MAX).unwrap();
+    assert_eq!(checked_target_sizes(0, 0).unwrap(), (3, 3));
+    assert_eq!(checked_target_sizes(1, 0).unwrap(), (3, 3));
+    assert_eq!(
+        checked_target_sizes(limit - 1, 0).unwrap(),
+        (limit, limit - 1)
+    );
+    assert!(matches!(
+        checked_target_sizes(usize::MAX, 0),
+        Err(ReductionError::IntegerOverflow { .. })
+    ));
+    assert_eq!(checked_target_sizes(2, limit - 2).unwrap(), (3, limit));
+    assert!(matches!(
+        checked_target_sizes(2, usize::MAX - 1),
+        Err(ReductionError::IntegerOverflow { .. })
+    ));
+}