diff --git a/docs/paper/verify-reductions/adversary_subsetsum_partition.py b/docs/paper/verify-reductions/adversary_subsetsum_partition.py
new file mode 100644
index 00000000..ba1b9d0f
--- /dev/null
+++ b/docs/paper/verify-reductions/adversary_subsetsum_partition.py
@@ -0,0 +1,689 @@
+#!/usr/bin/env python3
+"""
+Adversary verification script for SubsetSum -> Partition reduction (#973).
+
+Independent implementation based solely on the Typst proof specification.
+Does NOT import or reference the constructor's verify_subsetsum_partition.py.
+"""
+
+import itertools
+import sys
+from typing import List, Optional, Tuple
+
+from hypothesis import given, settings, HealthCheck
+from hypothesis import strategies as st
+
+# ---------------------------------------------------------------------------
+# Core types
+# ---------------------------------------------------------------------------
+
+class SubsetSumInstance:
+    """Subset Sum: given multiset S of positive ints and target T, find A subset S with sum(A) = T."""
+    def __init__(self, elements: List[int], target: int):
+        self.elements = list(elements)
+        self.target = target
+        self.n = len(self.elements)
+        self.sigma = sum(self.elements)
+
+
+class PartitionInstance:
+    """Partition: given multiset S', find a partition into two parts with equal sum."""
+    def __init__(self, elements: List[int]):
+        self.elements = list(elements)
+        self.sigma_prime = sum(self.elements)
+        self.half = self.sigma_prime / 2  # may not be integer
+
+
+# ---------------------------------------------------------------------------
+# Reduction: SubsetSum -> Partition (from Typst proof)
+# ---------------------------------------------------------------------------
+
+def reduce(ss: SubsetSumInstance) -> PartitionInstance:
+    """
+    Construction from the Typst proof:
+    1. Compute d = |Sigma - 2T|
+    2. If d == 0: S' = S
+    3. If d > 0: S' = S union {d}
+    """
+    sigma = ss.sigma
+    T = ss.target
+    d = abs(sigma - 2 * T)
+    if d == 0:
+        return PartitionInstance(list(ss.elements))
+    else:
+        return PartitionInstance(list(ss.elements) + [d])
+
+
+def extract_solution(ss: SubsetSumInstance, partition_config: List[int]) -> List[int]:
+    """
+    Given a balanced partition config (list of 0/1 for each element in S'),
+    extract the SubsetSum solution (indicator over original n elements).
+
+    From the Typst proof:
+    - If d == 0: either side works; return indicator of P_1 restricted to original elements.
+    - If Sigma > 2T: S-elements on SAME side as d sum to T.
+    - If Sigma < 2T: S-elements on OPPOSITE side from d sum to T.
+    """
+    sigma = ss.sigma
+    T = ss.target
+    d = abs(sigma - 2 * T)
+    n = ss.n
+
+    if d == 0:
+        # Either side; return the side-0 indicator restricted to original elements
+        return list(partition_config[:n])
+    else:
+        # d is the last element (index n)
+        pad_side = partition_config[n]
+        if sigma > 2 * T:
+            # Same side as d
+            target_side = pad_side
+        else:
+            # Opposite side from d
+            target_side = 1 - pad_side
+        return [1 if partition_config[i] == target_side else 0 for i in range(n)]
+
+
+# ---------------------------------------------------------------------------
+# Feasibility checkers
+# ---------------------------------------------------------------------------
+
+def is_feasible_source(ss: SubsetSumInstance) -> bool:
+    """Check if any subset of S sums to T (brute force)."""
+    for mask in range(1 << ss.n):
+        s = 0
+        for i in range(ss.n):
+            if mask & (1 << i):
+                s += ss.elements[i]
+        if s == ss.target:
+            return True
+    return False
+
+
+def find_source_solution(ss: SubsetSumInstance) -> Optional[List[int]]:
+    """Find a subset summing to T, return indicator or None."""
+    for mask in range(1 << ss.n):
+        s = 0
+        for i in range(ss.n):
+            if mask & (1 << i):
+                s += ss.elements[i]
+        if s == ss.target:
+            return [1 if (mask & (1 << i)) else 0 for i in range(ss.n)]
+    return None
+
+
+def is_feasible_target(part: PartitionInstance) -> bool:
+    """Check if any subset of S' sums to Sigma'/2 (brute force)."""
+    if part.sigma_prime % 2 != 0:
+        return False
+    half = part.sigma_prime // 2
+    m = len(part.elements)
+    for mask in range(1 << m):
+        s = 0
+        for i in range(m):
+            if mask & (1 << i):
+                s += part.elements[i]
+        if s == half:
+            return True
+    return False
+
+
+def find_target_solution(part: PartitionInstance) -> Optional[List[int]]:
+    """Find a balanced partition, return config (0/1 per element) or None."""
+    if part.sigma_prime % 2 != 0:
+        return None
+    half = part.sigma_prime // 2
+    m = len(part.elements)
+    for mask in range(1 << m):
+        s = 0
+        for i in range(m):
+            if mask & (1 << i):
+                s += part.elements[i]
+        if s == half:
+            return [1 if (mask & (1 << i)) else 0 for i in range(m)]
+    return None
+
+
+# ---------------------------------------------------------------------------
+# Test tracking
+# ---------------------------------------------------------------------------
+
+passed = 0
+failed = 0
+bugs = []
+
+
+def check(condition: bool, msg: str):
+    global passed, failed, bugs
+    if condition:
+        passed += 1
+    else:
+        failed += 1
+        bugs.append(msg)
+        print(f"FAIL: {msg}", file=sys.stderr)
+
+
+# ---------------------------------------------------------------------------
+# 1. Exhaustive tests for n <= 5
+# ---------------------------------------------------------------------------
+
+def test_exhaustive():
+    """Exhaustive forward + backward + extraction for all instances with n <= 5."""
+    global passed, failed
+    count = 0
+    for n in range(0, 6):
+        # Generate elements from {1, ..., 10} to keep it tractable
+        max_val = min(10, 20)
+        if n == 0:
+            element_lists = [[]]
+        elif n <= 3:
+            element_lists = list(itertools.product(range(1, max_val + 1), repeat=n))
+        elif n == 4:
+            element_lists = list(itertools.product(range(1, 7), repeat=n))
+        else:
+            # n=5: use smaller range
+            element_lists = list(itertools.product(range(1, 5), repeat=n))
+
+        for elems in element_lists:
+            elems = list(elems)
+            sigma = sum(elems)
+            # Test various targets including edge cases
+            targets = set(range(0, sigma + 2))  # 0 to sigma+1
+            # Also add some larger targets
+            targets.add(sigma + 5)
+            for T in targets:
+                ss = SubsetSumInstance(elems, T)
+                part = reduce(ss)
+
+                src_feasible = is_feasible_source(ss)
+                tgt_feasible = is_feasible_target(part)
+
+                # Forward: source feasible => target feasible
+                if src_feasible:
+                    check(tgt_feasible,
+                          f"Forward failed: S={elems}, T={T}, sigma={sigma}")
+
+                # Backward: target feasible => source feasible
+                if tgt_feasible:
+                    check(src_feasible,
+                          f"Backward failed: S={elems}, T={T}, sigma={sigma}")
+
+                # Equivalence
+                check(src_feasible == tgt_feasible,
+                      f"Equivalence failed: S={elems}, T={T}, src={src_feasible}, tgt={tgt_feasible}")
+
+                # Extraction test: if target has a solution, extract and verify
+                if tgt_feasible:
+                    tgt_sol = find_target_solution(part)
+                    if tgt_sol is not None:
+                        extracted = extract_solution(ss, tgt_sol)
+                        ext_sum = sum(e * x for e, x in zip(ss.elements, extracted))
+                        check(ext_sum == T,
+                              f"Extraction failed: S={elems}, T={T}, extracted_sum={ext_sum}")
+
+                # Overhead: partition has at most n+1 elements
+                check(len(part.elements) <= n + 1,
+                      f"Overhead failed: S={elems}, T={T}, |S'|={len(part.elements)}, n+1={n+1}")
+
+                # When sigma == 2T, should have exactly n elements
+                if sigma == 2 * T:
+                    check(len(part.elements) == n,
+                          f"Overhead d=0 case: S={elems}, T={T}, |S'|={len(part.elements)} != {n}")
+
+                count += 1
+                if count % 5000 == 0:
+                    print(f"  Exhaustive progress: {count} instances checked...")
+
+    print(f"  Exhaustive tests completed: {count} instances")
+
+
+# ---------------------------------------------------------------------------
+# 2. YES example from Typst
+# ---------------------------------------------------------------------------
+
+def test_yes_example():
+    """Reproduce the YES example from the Typst proof."""
+    S = [3, 5, 7, 1, 4]
+    T = 8
+    ss = SubsetSumInstance(S, T)
+
+    check(ss.sigma == 20, f"YES: sigma should be 20, got {ss.sigma}")
+    check(ss.sigma > 2 * T, f"YES: should have sigma > 2T")
+
+    d = abs(ss.sigma - 2 * T)
+    check(d == 4, f"YES: d should be 4, got {d}")
+
+    part = reduce(ss)
+    check(part.elements == [3, 5, 7, 1, 4, 4], f"YES: S' should be [3,5,7,1,4,4], got {part.elements}")
+    check(part.sigma_prime == 24, f"YES: Sigma' should be 24, got {part.sigma_prime}")
+    check(part.half == 12, f"YES: H should be 12, got {part.half}")
+
+    # The proof says A = {3, 5} sums to 8 = T
+    check(3 + 5 == T, "YES: 3+5 should equal T=8")
+
+    # Check that the subset sum instance is feasible
+    check(is_feasible_source(ss), "YES: source should be feasible")
+
+    # Check partition feasibility
+    check(is_feasible_target(part), "YES: target should be feasible")
+
+    # Verify the specific partition from the proof:
+    # config = [0, 0, 1, 1, 1, 0] (0 = side with A union {d})
+    config = [0, 0, 1, 1, 1, 0]
+    side0 = sum(part.elements[i] for i in range(6) if config[i] == 0)
+    side1 = sum(part.elements[i] for i in range(6) if config[i] == 1)
+    check(side0 == 12, f"YES: side 0 sum should be 12, got {side0}")
+    check(side1 == 12, f"YES: side 1 sum should be 12, got {side1}")
+
+    # Extraction from this config
+    extracted = extract_solution(ss, config)
+    ext_sum = sum(e * x for e, x in zip(ss.elements, extracted))
+    check(ext_sum == T, f"YES: extracted sum should be 8, got {ext_sum}")
+
+    # The extracted subset should be {3, 5} (indices 0, 1)
+    check(extracted == [1, 1, 0, 0, 0], f"YES: extracted should be [1,1,0,0,0], got {extracted}")
+
+
+# ---------------------------------------------------------------------------
+# 3. NO example from Typst
+# ---------------------------------------------------------------------------
+
+def test_no_example():
+    """Reproduce the NO example from the Typst proof."""
+    S = [3, 7, 11]
+    T = 5
+    ss = SubsetSumInstance(S, T)
+
+    check(ss.sigma == 21, f"NO: sigma should be 21, got {ss.sigma}")
+    check(ss.sigma > 2 * T, f"NO: should have sigma > 2T")
+
+    d = abs(ss.sigma - 2 * T)
+    check(d == 11, f"NO: d should be 11, got {d}")
+
+    part = reduce(ss)
+    check(part.elements == [3, 7, 11, 11], f"NO: S' should be [3,7,11,11], got {part.elements}")
+    check(part.sigma_prime == 32, f"NO: Sigma' should be 32, got {part.sigma_prime}")
+    check(part.half == 16, f"NO: H should be 16, got {part.half}")
+
+    # Source should be infeasible
+    check(not is_feasible_source(ss), "NO: source should be infeasible")
+
+    # Target should be infeasible
+    check(not is_feasible_target(part), "NO: target should be infeasible")
+
+    # Verify by listing all possible subset sums of {3, 7, 11}
+    possible_sums = set()
+    for mask in range(1 << 3):
+        s = sum(S[i] for i in range(3) if mask & (1 << i))
+        possible_sums.add(s)
+    check(5 not in possible_sums, f"NO: 5 should not be achievable, sums = {possible_sums}")
+    expected_sums = {0, 3, 7, 10, 11, 14, 18, 21}
+    check(possible_sums == expected_sums, f"NO: possible sums should be {expected_sums}, got {possible_sums}")
+
+
+# ---------------------------------------------------------------------------
+# 4. Overhead formula verification
+# ---------------------------------------------------------------------------
+
+def test_overhead():
+    """Verify overhead formula: |S'| = n+1 when d > 0, |S'| = n when d == 0."""
+    count = 0
+    for n in range(1, 6):
+        for _ in range(200):
+            import random
+            elems = [random.randint(1, 20) for _ in range(n)]
+            sigma = sum(elems)
+            T = random.randint(0, sigma + 5)
+            ss = SubsetSumInstance(elems, T)
+            part = reduce(ss)
+            d = abs(sigma - 2 * T)
+            if d == 0:
+                check(len(part.elements) == n,
+                      f"Overhead: d=0, expected {n} elements, got {len(part.elements)}")
+            else:
+                check(len(part.elements) == n + 1,
+                      f"Overhead: d>0, expected {n+1} elements, got {len(part.elements)}")
+            count += 1
+    print(f"  Overhead tests: {count} instances")
+
+
+# ---------------------------------------------------------------------------
+# 5. Case analysis tests
+# ---------------------------------------------------------------------------
+
+def test_case_analysis():
+    """Test the three cases from the proof explicitly."""
+    count = 0
+
+    # Case 1: Sigma = 2T (d = 0)
+    for _ in range(100):
+        import random
+        n = random.randint(2, 6)
+        elems = [random.randint(1, 10) for _ in range(n)]
+        sigma = sum(elems)
+        if sigma % 2 != 0:
+            elems[0] += 1
+            sigma = sum(elems)
+        T = sigma // 2
+        ss = SubsetSumInstance(elems, T)
+        part = reduce(ss)
+        d = abs(sigma - 2 * T)
+        check(d == 0, f"Case1: d should be 0")
+        check(len(part.elements) == n, f"Case1: |S'| should be {n}")
+        check(part.sigma_prime == sigma, f"Case1: Sigma' should be {sigma}")
+        check(part.half == T, f"Case1: H should be {T}")
+        # Equivalence
+        check(is_feasible_source(ss) == is_feasible_target(part), "Case1: equivalence")
+        count += 6
+
+    # Case 2: Sigma > 2T (d = Sigma - 2T, H = Sigma - T)
+    for _ in range(100):
+        import random
+        n = random.randint(2, 6)
+        elems = [random.randint(1, 10) for _ in range(n)]
+        sigma = sum(elems)
+        T = random.randint(0, max(0, sigma // 2 - 1))
+        ss = SubsetSumInstance(elems, T)
+        if sigma <= 2 * T:
+            continue
+        part = reduce(ss)
+        d = sigma - 2 * T
+        check(d > 0, "Case2: d > 0")
+        check(len(part.elements) == n + 1, f"Case2: |S'| should be {n+1}")
+        expected_H = sigma - T
+        check(part.sigma_prime == 2 * expected_H, f"Case2: Sigma' = 2H")
+        check(part.half == expected_H, f"Case2: H = Sigma - T")
+        check(is_feasible_source(ss) == is_feasible_target(part), "Case2: equivalence")
+        count += 5
+
+    # Case 3: Sigma < 2T (d = 2T - Sigma, H = T)
+    for _ in range(100):
+        import random
+        n = random.randint(2, 6)
+        elems = [random.randint(1, 10) for _ in range(n)]
+        sigma = sum(elems)
+        T = random.randint(sigma // 2 + 1, sigma)
+        ss = SubsetSumInstance(elems, T)
+        if sigma >= 2 * T:
+            continue
+        part = reduce(ss)
+        d = 2 * T - sigma
+        check(d > 0, "Case3: d > 0")
+        check(len(part.elements) == n + 1, f"Case3: |S'| should be {n+1}")
+        check(part.half == T, f"Case3: H = T")
+        check(is_feasible_source(ss) == is_feasible_target(part), "Case3: equivalence")
+        count += 4
+
+    # Infeasible case: T > Sigma
+    for _ in range(50):
+        import random
+        n = random.randint(1, 5)
+        elems = [random.randint(1, 10) for _ in range(n)]
+        sigma = sum(elems)
+        T = sigma + random.randint(1, 10)
+        ss = SubsetSumInstance(elems, T)
+        part = reduce(ss)
+        check(not is_feasible_source(ss), "Infeasible: source not feasible")
+        check(not is_feasible_target(part), "Infeasible: target not feasible")
+        count += 2
+
+    print(f"  Case analysis tests: {count} checks")
+
+
+# ---------------------------------------------------------------------------
+# 6. Hypothesis property-based tests
+# ---------------------------------------------------------------------------
+
+hypothesis_checks = 0
+
+
+@given(st.lists(st.integers(1, 20), min_size=1, max_size=8),
+       st.integers(0, 100))
+@settings(max_examples=1000, suppress_health_check=[HealthCheck.too_slow])
+def test_hyp_equivalence(elements, target):
+    """Property: source feasible iff target feasible."""
+    global hypothesis_checks, passed, failed
+    ss = SubsetSumInstance(elements, target)
+    part = reduce(ss)
+    src = is_feasible_source(ss)
+    tgt = is_feasible_target(part)
+    check(src == tgt,
+          f"Hyp equiv: S={elements}, T={target}, src={src}, tgt={tgt}")
+    hypothesis_checks += 1
+
+
+@given(st.lists(st.integers(1, 15), min_size=2, max_size=7))
+@settings(max_examples=1000, suppress_health_check=[HealthCheck.too_slow])
+def test_hyp_roundtrip(elements):
+    """Property: if source is feasible, extraction recovers a valid solution."""
+    global hypothesis_checks, passed, failed
+    # Pick target = sum of a random subset
+    sigma = sum(elements)
+    # Use first element as target for determinism
+    T = elements[0]
+    ss = SubsetSumInstance(elements, T)
+    part = reduce(ss)
+    if is_feasible_source(ss) and is_feasible_target(part):
+        tgt_sol = find_target_solution(part)
+        if tgt_sol is not None:
+            extracted = extract_solution(ss, tgt_sol)
+            ext_sum = sum(e * x for e, x in zip(ss.elements, extracted))
+            check(ext_sum == T,
+                  f"Hyp roundtrip: S={elements}, T={T}, ext_sum={ext_sum}")
+    hypothesis_checks += 1
+
+
+@given(st.lists(st.integers(1, 30), min_size=1, max_size=6),
+       st.integers(1, 50))
+@settings(max_examples=1000, suppress_health_check=[HealthCheck.too_slow])
+def test_hyp_overhead(elements, target):
+    """Property: overhead is at most n+1 elements."""
+    global hypothesis_checks, passed, failed
+    ss = SubsetSumInstance(elements, target)
+    part = reduce(ss)
+    n = len(elements)
+    check(len(part.elements) <= n + 1,
+          f"Hyp overhead: |S'|={len(part.elements)}, n+1={n+1}")
+    d = abs(sum(elements) - 2 * target)
+    if d == 0:
+        check(len(part.elements) == n,
+              f"Hyp overhead d=0: |S'|={len(part.elements)}, n={n}")
+    else:
+        check(len(part.elements) == n + 1,
+              f"Hyp overhead d>0: |S'|={len(part.elements)}, n+1={n+1}")
+    hypothesis_checks += 1
+
+
+@given(st.lists(st.integers(1, 10), min_size=2, max_size=6))
+@settings(max_examples=500, suppress_health_check=[HealthCheck.too_slow])
+def test_hyp_all_valid_targets(elements):
+    """For each achievable subset sum T, verify the full pipeline."""
+    global hypothesis_checks, passed, failed
+    sigma = sum(elements)
+    n = len(elements)
+    # Find all achievable subset sums
+    achievable = set()
+    for mask in range(1 << n):
+        s = sum(elements[i] for i in range(n) if mask & (1 << i))
+        achievable.add(s)
+    # Test a few
+    for T in list(achievable)[:5]:
+        ss = SubsetSumInstance(elements, T)
+        part = reduce(ss)
+        check(is_feasible_target(part),
+              f"Hyp all_valid: S={elements}, T={T} should be feasible")
+        tgt_sol = find_target_solution(part)
+        if tgt_sol is not None:
+            extracted = extract_solution(ss, tgt_sol)
+            ext_sum = sum(e * x for e, x in zip(ss.elements, extracted))
+            check(ext_sum == T,
+                  f"Hyp all_valid extraction: S={elements}, T={T}, ext_sum={ext_sum}")
+    hypothesis_checks += 1
+
+
+# ---------------------------------------------------------------------------
+# 7. Edge cases
+# ---------------------------------------------------------------------------
+
+def test_edge_cases():
+    """Test boundary conditions."""
+    count = 0
+
+    # Single element, target equals element
+    ss = SubsetSumInstance([5], 5)
+    part = reduce(ss)
+    check(is_feasible_source(ss), "Edge: single elem, T=elem, feasible")
+    check(is_feasible_target(part), "Edge: single elem partition feasible")
+    count += 2
+
+    # Single element, target = 0
+    ss = SubsetSumInstance([5], 0)
+    part = reduce(ss)
+    check(is_feasible_source(ss), "Edge: T=0 always feasible (empty subset)")
+    check(is_feasible_target(part), "Edge: T=0 partition feasible")
+    count += 2
+
+    # All elements equal
+    ss = SubsetSumInstance([3, 3, 3, 3], 6)
+    part = reduce(ss)
+    check(is_feasible_source(ss), "Edge: all equal, T=6 feasible")
+    check(is_feasible_target(part), "Edge: all equal partition feasible")
+    count += 2
+
+    # Target = sigma (pick all elements)
+    ss = SubsetSumInstance([1, 2, 3], 6)
+    part = reduce(ss)
+    check(is_feasible_source(ss), "Edge: T=sigma feasible")
+    check(is_feasible_target(part), "Edge: T=sigma partition feasible")
+    count += 2
+
+    # Target > sigma (infeasible)
+    ss = SubsetSumInstance([1, 2, 3], 7)
+    part = reduce(ss)
+    check(not is_feasible_source(ss), "Edge: T>sigma infeasible")
+    check(not is_feasible_target(part), "Edge: T>sigma partition infeasible")
+    count += 2
+
+    # Large padding (T >> sigma)
+    ss = SubsetSumInstance([1, 1], 100)
+    part = reduce(ss)
+    check(not is_feasible_source(ss), "Edge: T>>sigma infeasible")
+    check(not is_feasible_target(part), "Edge: T>>sigma partition infeasible")
+    count += 2
+
+    # T = sigma/2 exactly (Case 1)
+    ss = SubsetSumInstance([2, 4, 6], 6)
+    part = reduce(ss)
+    d = abs(ss.sigma - 2 * ss.target)
+    check(d == 0, "Edge: T=sigma/2, d=0")
+    check(len(part.elements) == 3, "Edge: T=sigma/2, no padding")
+    count += 2
+
+    # Empty elements, T=0
+    ss = SubsetSumInstance([], 0)
+    part = reduce(ss)
+    check(is_feasible_source(ss), "Edge: empty S, T=0 feasible")
+    check(is_feasible_target(part), "Edge: empty partition feasible")
+    count += 2
+
+    # Empty elements, T>0
+    ss = SubsetSumInstance([], 5)
+    part = reduce(ss)
+    check(not is_feasible_source(ss), "Edge: empty S, T=5 infeasible")
+    check(not is_feasible_target(part), "Edge: empty S, T=5 partition infeasible")
+    count += 2
+
+    print(f"  Edge case tests: {count} checks")
+
+
+# ---------------------------------------------------------------------------
+# 8. Padding element correctness
+# ---------------------------------------------------------------------------
+
+def test_padding_values():
+    """Verify the padding element d is computed correctly for all three cases."""
+    import random
+    count = 0
+    for _ in range(500):
+        n = random.randint(1, 6)
+        elems = [random.randint(1, 15) for _ in range(n)]
+        sigma = sum(elems)
+        T = random.randint(0, sigma + 5)
+        ss = SubsetSumInstance(elems, T)
+        part = reduce(ss)
+        d = abs(sigma - 2 * T)
+
+        if sigma == 2 * T:
+            # Case 1: no padding
+            check(part.elements == elems, f"Padding Case1: S'=S")
+            check(part.sigma_prime == sigma, f"Padding Case1: Sigma'=Sigma")
+        elif sigma > 2 * T:
+            # Case 2: d = sigma - 2T, H = sigma - T
+            check(d == sigma - 2 * T, f"Padding Case2: d formula")
+            check(part.elements == elems + [d], f"Padding Case2: S'=S+[d]")
+            H = sigma - T
+            check(part.sigma_prime == 2 * H, f"Padding Case2: Sigma'=2H")
+        else:
+            # Case 3: d = 2T - sigma, H = T
+            check(d == 2 * T - sigma, f"Padding Case3: d formula")
+            check(part.elements == elems + [d], f"Padding Case3: S'=S+[d]")
+            check(part.sigma_prime == 2 * T, f"Padding Case3: Sigma'=2T")
+        count += 3
+
+    print(f"  Padding value tests: {count} checks")
+
+
+# ---------------------------------------------------------------------------
+# Main
+# ---------------------------------------------------------------------------
+
+def main():
+    global passed, failed, bugs
+
+    print("=" * 60)
+    print("ADVERSARY: SubsetSum -> Partition verification")
+    print("=" * 60)
+
+    print("\n[1] Exhaustive tests (n <= 5)...")
+    test_exhaustive()
+
+    print("\n[2] YES example from Typst...")
+    test_yes_example()
+
+    print("\n[3] NO example from Typst...")
+    test_no_example()
+
+    print("\n[4] Overhead formula verification...")
+    test_overhead()
+
+    print("\n[5] Case analysis tests...")
+    test_case_analysis()
+
+    print("\n[6] Hypothesis property-based tests...")
+    test_hyp_equivalence()
+    test_hyp_roundtrip()
+    test_hyp_overhead()
+    test_hyp_all_valid_targets()
+
+    print("\n[7] Edge cases...")
+    test_edge_cases()
+
+    print("\n[8] Padding value tests...")
+    test_padding_values()
+
+    total = passed + failed
+    print("\n" + "=" * 60)
+    print(f"ADVERSARY: SubsetSum -> Partition: {passed} passed, {failed} failed")
+    if bugs:
+        print(f"BUGS FOUND: {bugs[:20]}")  # Show first 20
+    else:
+        print("BUGS FOUND: none")
+    print(f"Total checks: {total}")
+    if total < 5000:
+        print(f"WARNING: Only {total} checks, need >= 5000")
+
+    return failed
+
+
+if __name__ == "__main__":
+    sys.exit(main())
diff --git a/docs/paper/verify-reductions/cross_compare_subsetsum_partition.py b/docs/paper/verify-reductions/cross_compare_subsetsum_partition.py
new file mode 100644
index 00000000..453bb184
--- /dev/null
+++ b/docs/paper/verify-reductions/cross_compare_subsetsum_partition.py
@@ -0,0 +1,92 @@
+#!/usr/bin/env python3
+"""Cross-compare constructor and adversary for SubsetSum → Partition."""
+import itertools
+import sys
+sys.path.insert(0, "docs/paper/verify-reductions")
+
+from verify_subsetsum_partition import (
+    reduce as c_reduce,
+    is_subset_sum_feasible as c_is_source_feasible,
+    is_partition_feasible as c_is_target_feasible,
+    extract_subsetsum_solution as c_extract,
+)
+from adversary_subsetsum_partition import (
+    reduce as a_reduce_raw,
+    is_feasible_source as a_is_source_feasible_raw,
+    is_feasible_target as a_is_target_feasible_raw,
+    SubsetSumInstance,
+)
+
+agree = disagree = 0
+feasibility_mismatch = 0
+extraction_mismatch = 0
+
+
+def a_reduce(sizes, target):
+    """Adapter for adversary reduce."""
+    ss = SubsetSumInstance(list(sizes), target)
+    part = a_reduce_raw(ss)
+    return part.elements
+
+
+for n in range(1, 6):
+    max_val = min(8, 2**n)
+    instances_tested = 0
+    max_instances = 200
+
+    if n <= 3:
+        all_size_combos = list(itertools.product(range(1, max_val + 1), repeat=n))
+    else:
+        import random
+        random.seed(999 + n)
+        all_size_combos = [tuple(random.randint(1, max_val) for _ in range(n))
+                           for _ in range(100)]
+
+    for sizes in all_size_combos:
+        sizes = list(sizes)
+        sigma = sum(sizes)
+        targets = [0, 1, sigma // 2, sigma, sigma + 1]
+
+        for target in targets:
+            if target < 0 or instances_tested >= max_instances:
+                continue
+
+            # Run both reductions
+            c_part, c_d, c_sigma = c_reduce(sizes, target)
+            a_part = a_reduce(sizes, target)
+
+            # Compare structural equivalence
+            if c_part == a_part:
+                agree += 1
+            else:
+                disagree += 1
+                print(f"  DISAGREE on sizes={sizes}, T={target}")
+                print(f"    Constructor: {c_part}")
+                print(f"    Adversary:   {a_part}")
+
+            # Compare source feasibility
+            c_sf = c_is_source_feasible(sizes, target)
+            a_sf = a_is_source_feasible_raw(SubsetSumInstance(sizes, target))
+            if c_sf != a_sf:
+                feasibility_mismatch += 1
+                print(f"  SOURCE FEASIBILITY MISMATCH: sizes={sizes}, T={target}")
+
+            # Compare target feasibility
+            c_tf = c_is_target_feasible(c_part)
+            a_tf = a_is_target_feasible_raw(a_reduce_raw(SubsetSumInstance(sizes, target)))
+            if c_tf != a_tf:
+                feasibility_mismatch += 1
+                print(f"  TARGET FEASIBILITY MISMATCH: sizes={sizes}, T={target}")
+
+            instances_tested += 1
+
+    print(f"n={n}: tested {instances_tested} instances")
+
+print(f"\nCross-comparison: {agree} agree, {disagree} disagree, "
+      f"{feasibility_mismatch} feasibility mismatches")
+if disagree > 0 or feasibility_mismatch > 0:
+    print("ACTION REQUIRED: investigate discrepancies before proceeding")
+    sys.exit(1)
+else:
+    print("All instances agree between constructor and adversary.")
+    sys.exit(0)
diff --git a/docs/paper/verify-reductions/subsetsum_partition.pdf b/docs/paper/verify-reductions/subsetsum_partition.pdf
new file mode 100644
index 00000000..6adf6a72
Binary files /dev/null and b/docs/paper/verify-reductions/subsetsum_partition.pdf differ
diff --git a/docs/paper/verify-reductions/subsetsum_partition.typ b/docs/paper/verify-reductions/subsetsum_partition.typ
new file mode 100644
index 00000000..04f6a82d
--- /dev/null
+++ b/docs/paper/verify-reductions/subsetsum_partition.typ
@@ -0,0 +1,162 @@
+// Verification proof: SubsetSum → Partition (#973)
+#import "@preview/ctheorems:1.1.3": thmbox, thmplain, thmproof, thmrules
+
+#set page(paper: "a4", margin: (x: 2cm, y: 2.5cm))
+#set text(font: "New Computer Modern", size: 10pt)
+#set par(justify: true)
+#set heading(numbering: "1.1")
+
+#show: thmrules.with(qed-symbol: $square$)
+#let theorem = thmbox("theorem", "Theorem", fill: rgb("#e8e8f8"))
+#let proof = thmproof("proof", "Proof")
+
+== Subset Sum $arrow.r$ Partition <sec:subsetsum-partition>
+
+#theorem[
+  Subset Sum is polynomial-time reducible to Partition.
+  Given a Subset Sum instance with $n$ elements and target $T$, the
+  constructed Partition instance has at most $n + 1$ elements.
+] <thm:subsetsum-partition>
+
+#proof[
+  _Construction._
+  Let $(S, T)$ be a Subset Sum instance where $S = {s_1, dots, s_n}$ is a
+  multiset of positive integers and $T$ is the target sum. Define
+  $Sigma = sum_(i=1)^n s_i$.
+
+  Construct a Partition instance $S'$ as follows.
+
+  + Compute the padding value $d = |Sigma - 2T|$.
+
+  + If $d = 0$ (equivalently, $Sigma = 2T$): set $S' = S$, containing the
+    same $n$ elements.
+
+  + If $d > 0$: set $S' = S union {d}$, appending $d$ as the $(n+1)$-th
+    element.
+
+  Denote $Sigma' = sum_(a in S') a$ (the total sum of the Partition instance)
+  and $H = Sigma' / 2$ (the half-sum target for Partition). We compute $H$
+  for each case:
+  - If $Sigma = 2T$: $Sigma' = Sigma = 2T$, so $H = T$.
+  - If $Sigma > 2T$: $d = Sigma - 2T$, so $Sigma' = Sigma + d = 2(Sigma - T)$, and $H = Sigma - T$.
+  - If $Sigma < 2T$: $d = 2T - Sigma$, so $Sigma' = Sigma + d = 2T$, and $H = T$.
+
+  _Correctness._
+
+  We prove the equivalence in three cases.
+
+  *Case 1: $Sigma = 2T$ (no padding, $d = 0$).*
+
+  ($arrow.r.double$) Suppose $A subset.eq S$ with $sum_(a in A) a = T$. Then
+  $sum_(a in S without A) a = Sigma - T = 2T - T = T$. The partition
+  $(A, S without A)$ has equal sums $T = H$.
+
+  ($arrow.l.double$) Suppose $(P_1, P_2)$ is a balanced partition of $S'$ with
+  $sum P_1 = sum P_2 = H = T$. Then $P_1 subset.eq S$ and
+  $sum_(a in P_1) a = T$, so $P_1$ is a valid Subset Sum solution.
+
+  *Case 2: $Sigma > 2T$ ($d = Sigma - 2T > 0$, $H = Sigma - T$).*
+
+  ($arrow.r.double$) Suppose $A subset.eq S$ with $sum_(a in A) a = T$. Place
+  $A union {d}$ on one side and $S without A$ on the other:
+  $ sum (A union {d}) = T + (Sigma - 2T) = Sigma - T = H. $
+  $ sum (S without A) = Sigma - T = H. $
+
+  ($arrow.l.double$) Suppose $(P_1, P_2)$ is a balanced partition of $S'$
+  with $sum P_1 = sum P_2 = H = Sigma - T$. The padding element $d$ lies in
+  exactly one part; without loss of generality say $d in P_1$. The
+  $S$-elements in $P_1$ sum to $H - d = (Sigma - T) - (Sigma - 2T) = T$.
+  These elements form a valid Subset Sum solution.
+
+  *Case 3: $Sigma < 2T$ ($d = 2T - Sigma > 0$, $H = T$).*
+
+  ($arrow.r.double$) Suppose $A subset.eq S$ with $sum_(a in A) a = T$. Place
+  $A$ on one side and $(S without A) union {d}$ on the other:
+  $ sum A = T = H. $
+  $ sum ((S without A) union {d}) = (Sigma - T) + (2T - Sigma) = T = H. $
+
+  ($arrow.l.double$) Suppose $(P_1, P_2)$ is a balanced partition of $S'$
+  with $sum P_1 = sum P_2 = H = T$. The padding element $d$ lies in exactly
+  one part; without loss of generality say $d in P_1$. The $S$-elements in
+  $P_2$ (the part without $d$) sum to $H = T$, forming a valid Subset Sum
+  solution.
+
+  *Infeasible case: $T > Sigma$.*
+  No subset of $S$ can sum to $T$ because the total sum of all elements is
+  only $Sigma < T$. Here $d = 2T - Sigma > Sigma$, so $Sigma' = 2T$ and
+  $H = T$. Since $d > Sigma >= s_i$ for all $i$, the padding element $d$
+  alone exceeds the sum of all original elements. In any partition, the side
+  containing $d$ has sum at least $d = 2T - Sigma > T = H$ (because $T > Sigma$
+  implies $2T - Sigma > T$). So no balanced partition exists.
+
+  _Solution extraction._
+  Given a balanced partition $(P_1, P_2)$ of $S'$:
+  - If $d = 0$: either side is a valid Subset Sum solution. Return the
+    indicator of $P_1$ restricted to the original elements.
+  - If $Sigma > 2T$: the $S$-elements on the *same side as $d$* sum to $T$.
+    Return those elements.
+  - If $Sigma < 2T$: the $S$-elements on the *opposite side from $d$* sum to
+    $T$. Return those elements.
+
+  In all cases, the extraction identifies which original elements form a
+  subset summing to $T$ by locating the padding element (if present) and
+  selecting the appropriate side.
+]
+
+*Overhead.*
+#table(
+  columns: (auto, auto),
+  align: (left, left),
+  table.header([Target metric], [Formula]),
+  [`num_elements`], [$n + 1$ (worst case); $n$ when $Sigma = 2T$],
+)
+
+*Feasible example (YES instance).*
+Consider the Subset Sum instance with elements $S = {3, 5, 7, 1, 4}$ ($n = 5$)
+and target $T = 8$.
+
+$Sigma = 3 + 5 + 7 + 1 + 4 = 20$, and $2T = 16$, so $Sigma > 2T$. The padding
+value is $d = Sigma - 2T = 20 - 16 = 4$.
+
+Constructed Partition instance: $S' = {3, 5, 7, 1, 4, 4}$ ($n + 1 = 6$ elements).
+$Sigma' = 24$, $H = 12$.
+
+The subset $A = {3, 5}$ satisfies $3 + 5 = 8 = T$.
+
+Partition solution (Case 2, $Sigma > 2T$): place $A union {d} = {3, 5, 4_"pad"}$
+on one side (sum $= 8 + 4 = 12 = H$) and ${7, 1, 4}$ on the other
+(sum $= 7 + 1 + 4 = 12 = H$).
+
+In binary config over $S' = {3, 5, 7, 1, 4, 4_"pad"}$:
+config $= [0, 0, 1, 1, 1, 0]$ (where 0 = side with $A union {d}$,
+1 = other side).
+
+Extraction: padding element (index 5) is on side 0. Since $Sigma > 2T$,
+the $S$-elements on the same side as padding are ${s_1 = 3, s_2 = 5}$, which
+sum to $8 = T$. $checkmark$
+
+Verification:
+- Side 0: $3 + 5 + 4_"pad" = 12$ $checkmark$
+- Side 1: $7 + 1 + 4 = 12$ $checkmark$
+- Extracted subset: ${3, 5}$, sum $= 8 = T$ $checkmark$
+
+*Infeasible example (NO instance).*
+Consider the Subset Sum instance with elements $S = {3, 7, 11}$ ($n = 3$) and
+target $T = 5$.
+
+$Sigma = 3 + 7 + 11 = 21$, and $2T = 10$, so $Sigma > 2T$. The padding value
+is $d = Sigma - 2T = 21 - 10 = 11$.
+
+Constructed Partition instance: $S' = {3, 7, 11, 11}$ ($n + 1 = 4$ elements).
+$Sigma' = 32$, $H = 16$.
+
+No subset of $S = {3, 7, 11}$ sums to $T = 5$: the possible subset sums are
+$0, 3, 7, 10, 11, 14, 18, 21$, none of which equals 5.
+
+For the Partition instance, the half-sum target is $H = 16$. There are
+$2^4 = 16$ possible binary assignments over 4 elements. The achievable
+subset sums of ${3, 7, 11, 11}$ are:
+$0, 3, 7, 10, 11, 14, 18, 21, 22, 25, 29, 32$, none of which equals 16.
+(Here 11 appears twice, but the two copies are distinguishable as original
+vs padding.) Since no subset sums to $H = 16$, no balanced partition
+exists. $checkmark$
diff --git a/docs/paper/verify-reductions/verify_subsetsum_partition.py b/docs/paper/verify-reductions/verify_subsetsum_partition.py
new file mode 100644
index 00000000..49e7eda9
--- /dev/null
+++ b/docs/paper/verify-reductions/verify_subsetsum_partition.py
@@ -0,0 +1,452 @@
+#!/usr/bin/env python3
+"""§1.1 SubsetSum → Partition (#973): exhaustive + structural verification."""
+import itertools
+import sys
+from sympy import symbols, simplify, Abs
+
+passed = failed = 0
+
+
+def check(condition, msg=""):
+    global passed, failed
+    if condition:
+        passed += 1
+    else:
+        failed += 1
+        print(f"  FAIL: {msg}")
+
+
+# ── Reduction implementation ──────────────────────────────────────────────
+
+
+def reduce(sizes, target):
+    """Reduce SubsetSum(sizes, target) to Partition(sizes').
+
+    Returns:
+        partition_sizes: list of positive integers for the Partition instance
+        d: the padding value (0 if no padding needed)
+        sigma: sum of original sizes
+    """
+    sigma = sum(sizes)
+    d = abs(sigma - 2 * target)
+    if d == 0:
+        partition_sizes = list(sizes)
+    else:
+        partition_sizes = list(sizes) + [d]
+    return partition_sizes, d, sigma
+
+
+def is_subset_sum_feasible(sizes, target):
+    """Brute force: does any subset of sizes sum to target?"""
+    n = len(sizes)
+    for bits in range(2**n):
+        s = sum(sizes[i] for i in range(n) if (bits >> i) & 1)
+        if s == target:
+            return True
+    return False
+
+
+def find_subset_sum_solution(sizes, target):
+    """Return a config (0/1 list) for a subset summing to target, or None."""
+    n = len(sizes)
+    for bits in range(2**n):
+        s = sum(sizes[i] for i in range(n) if (bits >> i) & 1)
+        if s == target:
+            return [(bits >> i) & 1 for i in range(n)]
+    return None
+
+
+def is_partition_feasible(sizes):
+    """Brute force: can sizes be partitioned into two equal-sum subsets?"""
+    total = sum(sizes)
+    if total % 2 != 0:
+        return False
+    half = total // 2
+    n = len(sizes)
+    for bits in range(2**n):
+        s = sum(sizes[i] for i in range(n) if (bits >> i) & 1)
+        if s == half:
+            return True
+    return False
+
+
+def find_partition_solution(sizes):
+    """Return a config (0/1 list) for a balanced partition, or None."""
+    total = sum(sizes)
+    if total % 2 != 0:
+        return None
+    half = total // 2
+    n = len(sizes)
+    for bits in range(2**n):
+        s = sum(sizes[i] for i in range(n) if (bits >> i) & 1)
+        if s == half:
+            return [(bits >> i) & 1 for i in range(n)]
+    return None
+
+
+def extract_subsetsum_solution(sizes, target, partition_config, d, sigma):
+    """Extract SubsetSum solution from Partition config.
+
+    partition_config: 0/1 list over partition_sizes
+    Returns: 0/1 list over original sizes (1 = in subset)
+    """
+    n = len(sizes)
+    if d == 0:
+        # Either side works; return the side that sums to target
+        side0 = [i for i in range(n) if partition_config[i] == 0]
+        side1 = [i for i in range(n) if partition_config[i] == 1]
+        if sum(sizes[i] for i in side0) == target:
+            return [1 - partition_config[i] for i in range(n)]  # side 0 selected
+        else:
+            return [partition_config[i] for i in range(n)]  # side 1 selected
+    elif sigma > 2 * target:
+        # S-elements on SAME side as padding sum to T
+        pad_side = partition_config[n]  # padding is last element
+        return [1 if partition_config[i] == pad_side else 0 for i in range(n)]
+    else:  # sigma < 2 * target
+        # S-elements on OPPOSITE side from padding sum to T
+        pad_side = partition_config[n]
+        return [1 if partition_config[i] != pad_side else 0 for i in range(n)]
+
+
+def main():
+    # === Section 1: Symbolic checks (sympy) — MANDATORY ===
+    print("=== Section 1: Symbolic overhead verification ===")
+
+    n_sym, sigma_sym, T_sym = symbols("n Sigma T", positive=True, integer=True)
+
+    # Overhead: num_elements = n + 1 (worst case)
+    overhead = n_sym + 1
+    check(simplify(overhead - (n_sym + 1)) == 0, "overhead = n + 1")
+
+    # Case 1: Sigma = 2T => d = 0, Sigma' = 2T, H = T
+    d1 = Abs(sigma_sym - 2 * T_sym).subs(sigma_sym, 2 * T_sym)
+    check(simplify(d1) == 0, "Case 1: d = 0 when Sigma = 2T")
+
+    # Case 2: Sigma > 2T => d = Sigma - 2T, Sigma' = 2(Sigma - T), H = Sigma - T
+    d2 = sigma_sym - 2 * T_sym  # when sigma > 2T
+    sigma_prime_2 = sigma_sym + d2
+    H2 = sigma_prime_2 / 2
+    check(simplify(sigma_prime_2 - 2 * (sigma_sym - T_sym)) == 0,
+          "Case 2: Sigma' = 2(Sigma - T)")
+    check(simplify(H2 - (sigma_sym - T_sym)) == 0,
+          "Case 2: H = Sigma - T")
+
+    # Case 3: Sigma < 2T => d = 2T - Sigma, Sigma' = 2T, H = T
+    d3 = 2 * T_sym - sigma_sym  # when sigma < 2T
+    sigma_prime_3 = sigma_sym + d3
+    H3 = sigma_prime_3 / 2
+    check(simplify(sigma_prime_3 - 2 * T_sym) == 0,
+          "Case 3: Sigma' = 2T")
+    check(simplify(H3 - T_sym) == 0,
+          "Case 3: H = T")
+
+    # Verify forward direction algebra for Case 2
+    # A sums to T, A ∪ {d} sums to T + d = T + (Sigma - 2T) = Sigma - T = H
+    forward_case2 = T_sym + (sigma_sym - 2 * T_sym)
+    check(simplify(forward_case2 - (sigma_sym - T_sym)) == 0,
+          "Case 2 forward: T + d = Sigma - T")
+
+    # Verify backward direction algebra for Case 2
+    # Side with d: S-elements sum to H - d = (Sigma - T) - (Sigma - 2T) = T
+    back_case2 = (sigma_sym - T_sym) - (sigma_sym - 2 * T_sym)
+    check(simplify(back_case2 - T_sym) == 0,
+          "Case 2 backward: H - d = T")
+
+    # Verify forward direction algebra for Case 3
+    # (S\A) ∪ {d}: (Sigma - T) + (2T - Sigma) = T
+    forward_case3 = (sigma_sym - T_sym) + (2 * T_sym - sigma_sym)
+    check(simplify(forward_case3 - T_sym) == 0,
+          "Case 3 forward: (Sigma-T) + d = T")
+
+    # Numeric checks for various (n, sigma, T)
+    for n_val in range(1, 8):
+        for sigma_val in range(n_val, 3 * n_val + 5):
+            for t_val in range(0, sigma_val + 3):
+                d_val = abs(sigma_val - 2 * t_val)
+                if d_val == 0:
+                    sp = sigma_val
+                else:
+                    sp = sigma_val + d_val
+                check(sp % 2 == 0,
+                      f"Sigma'={sp} is even for n={n_val},Sigma={sigma_val},T={t_val}")
+
+    print(f"  Section 1: {passed} passed, {failed} failed")
+
+    # === Section 2: Exhaustive forward + backward — MANDATORY ===
+    print("\n=== Section 2: Exhaustive forward + backward (n ≤ 5) ===")
+    sec2_start = passed
+
+    for n in range(1, 6):
+        # Generate SubsetSum instances: sizes from 1..max_val, various targets
+        max_val = min(10, 2**n)
+        num_tested = 0
+
+        # All multisets of size n with elements in 1..max_val (sample)
+        if n <= 3:
+            size_range = range(1, max_val + 1)
+            all_size_combos = list(itertools.product(size_range, repeat=n))
+        else:
+            # Sample for larger n
+            import random
+            random.seed(42 + n)
+            all_size_combos = [tuple(random.randint(1, max_val) for _ in range(n))
+                               for _ in range(200)]
+
+        for sizes in all_size_combos:
+            sigma = sum(sizes)
+            # Test several targets including edge cases
+            targets = set([0, 1, sigma // 2, sigma, sigma + 1])
+            targets.update(range(max(0, sigma // 2 - 2), min(sigma + 2, sigma // 2 + 3)))
+            if n <= 3:
+                targets = set(range(0, sigma + 2))
+
+            for target in targets:
+                if target < 0:
+                    continue
+                source_feasible = is_subset_sum_feasible(list(sizes), target)
+                part_sizes, d, sig = reduce(list(sizes), target)
+                target_feasible = is_partition_feasible(part_sizes)
+
+                check(source_feasible == target_feasible,
+                      f"n={n}, sizes={sizes}, T={target}: "
+                      f"source={source_feasible}, target={target_feasible}")
+                num_tested += 1
+
+        print(f"  n={n}: tested {num_tested} instances")
+
+    print(f"  Section 2: {passed - sec2_start} new checks")
+
+    # === Section 3: Solution extraction — MANDATORY ===
+    print("\n=== Section 3: Solution extraction ===")
+    sec3_start = passed
+
+    for n in range(1, 6):
+        max_val = min(10, 2**n)
+        num_extracted = 0
+
+        if n <= 3:
+            all_size_combos = list(itertools.product(range(1, max_val + 1), repeat=n))
+        else:
+            import random
+            random.seed(100 + n)
+            all_size_combos = [tuple(random.randint(1, max_val) for _ in range(n))
+                               for _ in range(150)]
+
+        for sizes in all_size_combos:
+            sizes = list(sizes)
+            sigma = sum(sizes)
+
+            for target in range(0, sigma + 1):
+                if not is_subset_sum_feasible(sizes, target):
+                    continue
+
+                part_sizes, d, sig = reduce(sizes, target)
+                part_config = find_partition_solution(part_sizes)
+                if part_config is None:
+                    check(False, f"Feasible source but no partition config: sizes={sizes}, T={target}")
+                    continue
+
+                extracted = extract_subsetsum_solution(sizes, target, part_config, d, sig)
+                extracted_sum = sum(sizes[i] for i in range(n) if extracted[i] == 1)
+
+                check(extracted_sum == target,
+                      f"extraction: sizes={sizes}, T={target}, got sum={extracted_sum}")
+                num_extracted += 1
+
+                if num_extracted >= 300:
+                    break
+            if num_extracted >= 300:
+                break
+
+        print(f"  n={n}: extracted {num_extracted} solutions")
+
+    print(f"  Section 3: {passed - sec3_start} new checks")
+
+    # === Section 4: Overhead formula — MANDATORY ===
+    print("\n=== Section 4: Overhead formula verification ===")
+    sec4_start = passed
+
+    for n in range(1, 6):
+        max_val = min(10, 2**n)
+        if n <= 3:
+            all_size_combos = list(itertools.product(range(1, max_val + 1), repeat=n))
+        else:
+            import random
+            random.seed(200 + n)
+            all_size_combos = [tuple(random.randint(1, max_val) for _ in range(n))
+                               for _ in range(100)]
+
+        count = 0
+        for sizes in all_size_combos:
+            sizes = list(sizes)
+            sigma = sum(sizes)
+            for target in [0, sigma // 2, sigma, sigma + 1, 1]:
+                if target < 0:
+                    continue
+                part_sizes, d, sig = reduce(sizes, target)
+
+                # Overhead: num_elements
+                if d == 0:
+                    check(len(part_sizes) == n,
+                          f"overhead d=0: got {len(part_sizes)}, expected {n}")
+                else:
+                    check(len(part_sizes) == n + 1,
+                          f"overhead d>0: got {len(part_sizes)}, expected {n+1}")
+
+                # Verify Sigma' and H
+                sp = sum(part_sizes)
+                check(sp % 2 == 0,
+                      f"Sigma' = {sp} must be even")
+
+                half = sp // 2
+                if sigma == 2 * target:
+                    check(half == target, f"Case 1: H={half} should be T={target}")
+                elif sigma > 2 * target:
+                    check(half == sigma - target,
+                          f"Case 2: H={half} should be Sigma-T={sigma - target}")
+                else:
+                    check(half == target, f"Case 3: H={half} should be T={target}")
+
+                count += 1
+            if count >= 500:
+                break
+
+    print(f"  Section 4: {passed - sec4_start} new checks")
+
+    # === Section 5: Structural properties — MANDATORY ===
+    print("\n=== Section 5: Structural properties ===")
+    sec5_start = passed
+
+    for n in range(1, 6):
+        max_val = min(10, 2**n)
+        if n <= 3:
+            all_size_combos = list(itertools.product(range(1, max_val + 1), repeat=n))
+        else:
+            import random
+            random.seed(300 + n)
+            all_size_combos = [tuple(random.randint(1, max_val) for _ in range(n))
+                               for _ in range(100)]
+
+        for sizes in all_size_combos:
+            sizes = list(sizes)
+            sigma = sum(sizes)
+            for target in [0, sigma // 2, sigma, sigma + 1]:
+                if target < 0:
+                    continue
+                part_sizes, d, sig = reduce(sizes, target)
+
+                # All elements must be positive
+                for i, s in enumerate(part_sizes):
+                    check(s > 0, f"element {i} = {s} must be positive")
+
+                # Padding value correctness
+                check(d == abs(sigma - 2 * target),
+                      f"d = {d}, expected |{sigma} - {2*target}| = {abs(sigma - 2*target)}")
+
+                # Original elements preserved
+                for i in range(n):
+                    check(part_sizes[i] == sizes[i],
+                          f"element {i} preserved: {part_sizes[i]} vs {sizes[i]}")
+
+                # If d > 0, padding is last element
+                if d > 0:
+                    check(part_sizes[-1] == d,
+                          f"padding element: {part_sizes[-1]} vs d={d}")
+
+                # Infeasible case check: T > Sigma => d > Sigma
+                if target > sigma:
+                    check(d > sigma,
+                          f"T > Sigma: d={d} should be > Sigma={sigma}")
+
+    print(f"  Section 5: {passed - sec5_start} new checks")
+
+    # === Section 6: YES example from Typst — MANDATORY ===
+    print("\n=== Section 6: YES example verification ===")
+    sec6_start = passed
+
+    # From Typst: S = {3, 5, 7, 1, 4}, T = 8
+    # Sigma = 20, 2T = 16, Sigma > 2T, d = 4
+    # S' = {3, 5, 7, 1, 4, 4}, Sigma' = 24, H = 12
+    yes_sizes = [3, 5, 7, 1, 4]
+    yes_target = 8
+    yes_sigma = 20
+
+    check(sum(yes_sizes) == yes_sigma, f"YES: Sigma = {sum(yes_sizes)}")
+    check(yes_sigma > 2 * yes_target, "YES: Sigma > 2T (Case 2)")
+
+    part_sizes, d, sigma = reduce(yes_sizes, yes_target)
+    check(d == 4, f"YES: d = {d}, expected 4")
+    check(part_sizes == [3, 5, 7, 1, 4, 4], f"YES: S' = {part_sizes}")
+    check(sum(part_sizes) == 24, f"YES: Sigma' = {sum(part_sizes)}")
+    check(sum(part_sizes) // 2 == 12, f"YES: H = {sum(part_sizes) // 2}")
+
+    # Verify subset {3, 5} sums to T = 8
+    check(3 + 5 == yes_target, "YES: subset {3,5} sums to T")
+
+    # Verify partition: {3, 5, 4_pad} vs {7, 1, 4}
+    check(3 + 5 + 4 == 12, "YES: side with A∪{d} = 12 = H")
+    check(7 + 1 + 4 == 12, "YES: other side = 12 = H")
+
+    # Verify config from Typst: [0, 0, 1, 1, 1, 0]
+    yes_config = [0, 0, 1, 1, 1, 0]
+    side0_sum = sum(part_sizes[i] for i in range(6) if yes_config[i] == 0)
+    side1_sum = sum(part_sizes[i] for i in range(6) if yes_config[i] == 1)
+    check(side0_sum == 12, f"YES config: side 0 sum = {side0_sum}")
+    check(side1_sum == 12, f"YES config: side 1 sum = {side1_sum}")
+
+    # Verify extraction
+    extracted = extract_subsetsum_solution(yes_sizes, yes_target, yes_config, d, sigma)
+    extracted_sum = sum(yes_sizes[i] for i in range(5) if extracted[i] == 1)
+    check(extracted_sum == yes_target,
+          f"YES extraction: sum = {extracted_sum}, expected {yes_target}")
+
+    check(is_subset_sum_feasible(yes_sizes, yes_target), "YES: source is feasible")
+    check(is_partition_feasible(part_sizes), "YES: target is feasible")
+
+    print(f"  Section 6: {passed - sec6_start} new checks")
+
+    # === Section 7: NO example from Typst — MANDATORY ===
+    print("\n=== Section 7: NO example verification ===")
+    sec7_start = passed
+
+    # From Typst: S = {3, 7, 11}, T = 5
+    # Sigma = 21, 2T = 10, Sigma > 2T, d = 11
+    # S' = {3, 7, 11, 11}, Sigma' = 32, H = 16
+    no_sizes = [3, 7, 11]
+    no_target = 5
+    no_sigma = 21
+
+    check(sum(no_sizes) == no_sigma, f"NO: Sigma = {sum(no_sizes)}")
+    check(no_sigma > 2 * no_target, "NO: Sigma > 2T (Case 2)")
+
+    part_sizes_no, d_no, sigma_no = reduce(no_sizes, no_target)
+    check(d_no == 11, f"NO: d = {d_no}, expected 11")
+    check(part_sizes_no == [3, 7, 11, 11], f"NO: S' = {part_sizes_no}")
+    check(sum(part_sizes_no) == 32, f"NO: Sigma' = {sum(part_sizes_no)}")
+    check(sum(part_sizes_no) // 2 == 16, f"NO: H = {sum(part_sizes_no) // 2}")
+
+    # Verify source infeasible: no subset of {3,7,11} sums to 5
+    check(not is_subset_sum_feasible(no_sizes, no_target), "NO: source is infeasible")
+
+    # Verify target infeasible
+    check(not is_partition_feasible(part_sizes_no), "NO: target is infeasible")
+
+    # Verify achievable subset sums of {3,7,11,11} match Typst
+    achievable = set()
+    for bits in range(16):
+        achievable.add(sum(part_sizes_no[i] for i in range(4) if (bits >> i) & 1))
+    expected_sums = {0, 3, 7, 10, 11, 14, 18, 21, 22, 25, 29, 32}
+    check(achievable == expected_sums,
+          f"NO: achievable sums = {sorted(achievable)}, expected {sorted(expected_sums)}")
+    check(16 not in achievable, "NO: 16 not achievable")
+
+    print(f"  Section 7: {passed - sec7_start} new checks")
+
+    # ── Final report ──
+    print(f"\nSubsetSum → Partition: {passed} passed, {failed} failed")
+    return 1 if failed else 0
+
+
+if __name__ == "__main__":
+    sys.exit(main())