Remove Coq export functionality from pruner

- Remove export_coq config option and coq_output_dir
- Remove export_coq() function
- Remove --export-coq CLI argument
- Update method count in docstring (17 -> 15)

prune.py

@@ -2,14 +2,13 @@
 Threshold Circuit Pruner
 
 Comprehensive pruning framework for threshold logic circuits.
-Supports 17 pruning methods with GPU-optimized parallel evaluation.
+Supports 15 pruning methods with GPU-optimized parallel evaluation.
 
 Usage:
     python prune.py threshold-hamming74decoder
     python prune.py threshold-hamming74decoder --methods evo,depth,symmetry
     python prune.py --list
     python prune.py --all --max-inputs 8
-    python prune.py threshold-xor --export-coq
 """
 
 import torch
@@ -126,24 +125,22 @@ class Config:
     run_quantize: bool = True
     run_evolutionary: bool = True
     run_annealing: bool = True
-    run_neuron: bool = True
-    run_lottery: bool = True
+    run_structural: bool = True
     run_topology: bool = True
-    run_structured: bool = True
     run_sensitivity: bool = True
     run_weight_sharing: bool = True
-    run_random: bool = True
-    run_pareto: bool = True
     run_depth: bool = True
     run_gate_subst: bool = True
     run_symmetry: bool = True
     run_fanin: bool = True
-    run_exhaustive: bool = True
+    run_exhaustive_mag: bool = True
+    run_exhaustive_sparse: bool = True
 
     magnitude_passes: int = 100
 
     exhaustive_range: int = 2
     exhaustive_max_params: int = 12
+    sparse_max_weight: int = 3
 
     evo_generations: int = 2000
     evo_pop_size: int = 0
@@ -161,10 +158,6 @@ class Config:
     annealing_parallel_chains: int = 0
 
     quantize_targets: List[float] = field(default_factory=lambda: [-1.0, 0.0, 1.0])
-    pareto_levels: List[float] = field(default_factory=lambda: [1.0, 0.99, 0.95, 0.90, 0.80])
-
-    lottery_rounds: int = 10
-    lottery_prune_rate: float = 0.2
 
     topology_generations: int = 500
     topology_remove_prob: float = 0.2
@@ -172,14 +165,9 @@ class Config:
 
     sensitivity_samples: int = 1000
 
-    random_iterations: int = 10000
-
     depth_max_collapse: int = 3
     fanin_target: int = 4
 
-    export_coq: bool = False
-    coq_output_dir: Path = field(default_factory=lambda: Path('D:/threshold-pruner/coq_exports'))
-
 
 @dataclass
 class CircuitSpec:
@@ -260,6 +248,7 @@ class ComputationGraph:
                 }
                 self.layer_groups[depth].append(neuron_name)
 
+        self._infer_depth_from_shapes()
         self._identify_outputs()
 
     def _estimate_depth(self, name: str) -> int:
@@ -285,6 +274,36 @@ class ComputationGraph:
 
         return depth
 
+    def _infer_depth_from_shapes(self):
+        """Second pass: infer depth from weight shapes when naming is ambiguous."""
+        neurons_at_depth_0 = []
+        neurons_needing_inference = []
+
+        for name, info in self.neurons.items():
+            input_size = info.get('input_size', 0)
+            if input_size == self.n_inputs:
+                info['depth'] = 0
+                info['input_source'] = 'raw'
+                info['input_neurons'] = []
+                neurons_at_depth_0.append(name)
+            elif input_size > 0 and input_size != self.n_inputs:
+                neurons_needing_inference.append((name, input_size))
+
+        for name, input_size in neurons_needing_inference:
+            if input_size == len(neurons_at_depth_0):
+                self.neurons[name]['depth'] = 1
+                self.neurons[name]['input_source'] = 'neurons'
+                self.neurons[name]['input_neurons'] = sorted(neurons_at_depth_0)
+            elif input_size < len(neurons_at_depth_0) and input_size > 0:
+                candidates = sorted(neurons_at_depth_0)[:input_size]
+                self.neurons[name]['depth'] = 1
+                self.neurons[name]['input_source'] = 'neurons'
+                self.neurons[name]['input_neurons'] = candidates
+
+        self.layer_groups = defaultdict(list)
+        for name, info in self.neurons.items():
+            self.layer_groups[info['depth']].append(name)
+
     def _identify_outputs(self):
         """Identify which neurons are outputs based on n_outputs and topology."""
 
@@ -398,11 +417,17 @@ class ComputationGraph:
         return outputs
 
     def _get_neuron_input(self, neuron_name: str, activations: Dict, raw_input: torch.Tensor, expected_size: int) -> torch.Tensor:
-        """Determine input for a neuron based on naming conventions."""
-        if expected_size == self.n_inputs or expected_size == raw_input.shape[-1]:
+        """Determine input for a neuron based on topology inference or naming conventions."""
+        info = self.neurons.get(neuron_name, {})
+
+        if info.get('input_source') == 'raw' or expected_size == self.n_inputs or expected_size == raw_input.shape[-1]:
             return raw_input
 
-        parts = neuron_name.split('.')
+        if info.get('input_source') == 'neurons' and info.get('input_neurons'):
+            input_neurons = info['input_neurons']
+            vals = [activations[n] for n in input_neurons if n in activations]
+            if len(vals) == len(input_neurons):
+                return torch.stack(vals, dim=-1)
 
         if 'layer2' in neuron_name:
             base = neuron_name.replace('.layer2', '')
@@ -1058,6 +1083,36 @@ class BatchedEvaluator:
             if original_fitness < 0.999 and self.cfg.verbose:
                 print(f"  [EVAL ERROR] Native eval fitness={original_fitness:.4f}")
 
+        if self.batched_ready and not self.use_native_eval:
+            try:
+                test_vecs = []
+                base = self.circuit.base_vector.clone()
+                test_vecs.append(base)
+                for _ in range(3):
+                    perturbed = base.clone()
+                    mask = torch.rand_like(perturbed) < 0.3
+                    perturbed[mask] = torch.randint(-2, 3, (mask.sum().item(),), device=self.device, dtype=torch.float32)
+                    test_vecs.append(perturbed)
+
+                test_pop = torch.stack(test_vecs)
+                single_results = torch.tensor([
+                    self.evaluate_single(self.circuit.vector_to_weights(v)) for v in test_vecs
+                ], device=self.device)
+
+                batched_results = self._evaluate_batched(test_pop)
+
+                if not torch.allclose(single_results, batched_results, atol=0.01):
+                    if self.cfg.verbose:
+                        print(f"  [EVAL WARNING] Batched eval mismatch (single={single_results.tolist()}, batched={batched_results.tolist()})")
+                        print(f"  [EVAL WARNING] Falling back to native eval")
+                    self.use_native_eval = self.circuit.has_native
+                    self.batched_ready = False
+            except Exception as e:
+                if self.cfg.verbose:
+                    print(f"  [EVAL WARNING] Batched eval failed ({e}), falling back to native eval")
+                self.use_native_eval = self.circuit.has_native
+                self.batched_ready = False
+
     def _setup_vmap(self):
         """Setup vmap-based parallel evaluation."""
         try:
@@ -1123,24 +1178,25 @@ class BatchedEvaluator:
 
                 input_size = w_shape[-1] if w_shape else 0
 
-                input_source = 'raw'
-                input_neurons = []
-
-                if input_size == self.n_inputs:
-                    input_source = 'raw'
-                elif 'layer2' in neuron_name:
-                    base = neuron_name.replace('.layer2', '')
-                    or_key = f'{base}.layer1.or'
-                    nand_key = f'{base}.layer1.nand'
-                    if or_key in graph.neurons and nand_key in graph.neurons:
-                        input_source = 'neurons'
-                        input_neurons = [or_key, nand_key]
-                elif 'xor_final' in neuron_name:
-                    prefix = neuron_name.split('.xor_final')[0]
-                    candidates = [n for n in graph.neurons if n.startswith(prefix) and 'xor_' in n and 'final' not in n and 'layer2' in n]
-                    if len(candidates) >= 2:
-                        input_source = 'neurons'
-                        input_neurons = sorted(candidates)[-2:]
+                input_source = info.get('input_source', 'raw')
+                input_neurons = info.get('input_neurons', [])
+
+                if input_source == 'raw' and input_size != self.n_inputs:
+                    if input_size == self.n_inputs:
+                        input_source = 'raw'
+                    elif 'layer2' in neuron_name:
+                        base = neuron_name.replace('.layer2', '')
+                        or_key = f'{base}.layer1.or'
+                        nand_key = f'{base}.layer1.nand'
+                        if or_key in graph.neurons and nand_key in graph.neurons:
+                            input_source = 'neurons'
+                            input_neurons = [or_key, nand_key]
+                    elif 'xor_final' in neuron_name:
+                        prefix = neuron_name.split('.xor_final')[0]
+                        candidates = [n for n in graph.neurons if n.startswith(prefix) and 'xor_' in n and 'final' not in n and 'layer2' in n]
+                        if len(candidates) >= 2:
+                            input_source = 'neurons'
+                            input_neurons = sorted(candidates)[-2:]
 
                 self.neuron_eval_order.append(neuron_name)
                 self.neuron_weight_slices[neuron_name] = {
@@ -1836,194 +1892,6 @@ def prune_annealing(circuit: AdaptiveCircuit, evaluator: BatchedEvaluator, cfg:
     )
 
 
-def prune_neuron(circuit: AdaptiveCircuit, evaluator: BatchedEvaluator, cfg: Config) -> PruneResult:
-    """
-    Truly exhaustive neuron-level pruning.
-
-    For each neuron, fix its parameters to zero and exhaustively search
-    all weight configurations for the REMAINING neurons. If any config
-    works, the neuron is provably unnecessary.
-    """
-    start = time.perf_counter()
-    original = circuit.stats()
-
-    neuron_groups = defaultdict(list)
-    for key in circuit.weights.keys():
-        parts = key.rsplit('.', 1)
-        neuron_name = parts[0] if len(parts) == 2 else key.split('.')[0]
-        neuron_groups[neuron_name].append(key)
-
-    neuron_names = list(neuron_groups.keys())
-    weight_keys = list(circuit.weights.keys())
-    weight_shapes = {k: circuit.weights[k].shape for k in weight_keys}
-    weight_sizes = {k: circuit.weights[k].numel() for k in weight_keys}
-    n_total_params = sum(weight_sizes.values())
-
-    if cfg.verbose:
-        print(f"    Found {len(neuron_groups)} neuron groups")
-        print(f"    Total parameters: {n_total_params}")
-
-    search_range = cfg.exhaustive_range
-    values = list(range(-search_range, search_range + 1))
-
-    def vector_to_weights(vec):
-        weights = {}
-        idx = 0
-        for k in weight_keys:
-            size = weight_sizes[k]
-            weights[k] = torch.tensor(vec[idx:idx+size], dtype=torch.float32, device=cfg.device).view(weight_shapes[k])
-            idx += size
-        return weights
-
-    def get_neuron_param_indices(neuron_name):
-        indices = []
-        idx = 0
-        for k in weight_keys:
-            size = weight_sizes[k]
-            if k in neuron_groups[neuron_name]:
-                indices.extend(range(idx, idx + size))
-            idx += size
-        return indices
-
-    best_weights = circuit.clone_weights()
-    best_neurons_removed = 0
-    removed_neuron_names = []
-
-    for neuron_name in neuron_names:
-        neuron_indices = set(get_neuron_param_indices(neuron_name))
-        other_indices = [i for i in range(n_total_params) if i not in neuron_indices]
-        n_other_params = len(other_indices)
-
-        if n_other_params > cfg.exhaustive_max_params:
-            if cfg.verbose:
-                print(f"    [{neuron_name}] Skipping: {n_other_params} remaining params > max {cfg.exhaustive_max_params}")
-            continue
-
-        search_space = (2 * search_range + 1) ** n_other_params
-
-        if cfg.verbose:
-            print(f"    [{neuron_name}] Testing removal: searching {search_space:,} configs for {n_other_params} remaining params")
-
-        found_valid = False
-        best_config = None
-        best_mag = float('inf')
-        tested = 0
-        report_interval = max(1, search_space // 10)
-
-        for combo in product(values, repeat=n_other_params):
-            tested += 1
-
-            full_vec = [0] * n_total_params
-            for i, val in zip(other_indices, combo):
-                full_vec[i] = val
-
-            weights = vector_to_weights(full_vec)
-            fitness = evaluator.evaluate_single(weights)
-
-            if fitness >= cfg.fitness_threshold:
-                mag = sum(abs(v) for v in combo)
-                if not found_valid or mag < best_mag:
-                    found_valid = True
-                    best_mag = mag
-                    best_config = full_vec
-
-            if cfg.verbose and tested % report_interval == 0:
-                elapsed = time.perf_counter() - start
-                pct = 100 * tested / search_space
-                print(f"      [{elapsed:6.1f}s] {pct:5.1f}% | valid={'YES' if found_valid else 'no '} | best_mag={best_mag if found_valid else '-'}")
-
-        if found_valid:
-            if cfg.verbose:
-                print(f"      [REMOVABLE] {neuron_name} can be removed! Best remaining mag={best_mag}")
-            removed_neuron_names.append(neuron_name)
-            best_neurons_removed += 1
-            best_weights = vector_to_weights(best_config)
-        else:
-            if cfg.verbose:
-                print(f"      [REQUIRED] {neuron_name} is necessary")
-
-    if cfg.verbose:
-        elapsed = time.perf_counter() - start
-        print(f"    [NEURON COMPLETE] {best_neurons_removed} neurons removable out of {len(neuron_names)}")
-        print(f"    Removable: {removed_neuron_names if removed_neuron_names else 'none'}")
-        print(f"    Time: {elapsed:.1f}s")
-
-    return PruneResult(
-        method='neuron',
-        original_stats=original,
-        final_stats=circuit.stats(best_weights),
-        final_weights=best_weights,
-        fitness=evaluator.evaluate_single(best_weights),
-        time_seconds=time.perf_counter() - start,
-        metadata={'neurons_removed': best_neurons_removed, 'removed_names': removed_neuron_names}
-    )
-
-
-def prune_lottery(circuit: AdaptiveCircuit, evaluator: BatchedEvaluator, cfg: Config) -> PruneResult:
-    """Lottery Ticket pruning."""
-    start = time.perf_counter()
-    original = circuit.stats()
-
-    weights = circuit.clone_weights()
-    initial = circuit.clone_weights()
-    history = []
-
-    if cfg.verbose:
-        print(f"    Lottery: {cfg.lottery_rounds} rounds, {cfg.lottery_prune_rate * 100:.0f}% per round")
-
-    mask = {k: torch.ones_like(v) for k, v in weights.items()}
-
-    for rnd in range(cfg.lottery_rounds):
-        all_weights = []
-        for name, tensor in weights.items():
-            flat = tensor.flatten()
-            m_flat = mask[name].flatten()
-            for i in range(len(flat)):
-                if m_flat[i] > 0 and flat[i].item() != 0:
-                    all_weights.append((abs(flat[i].item()), name, i))
-
-        if not all_weights:
-            break
-
-        all_weights.sort(key=lambda x: x[0])
-        n_prune = max(1, int(len(all_weights) * cfg.lottery_prune_rate))
-        to_prune = all_weights[:n_prune]
-
-        for _, name, idx in to_prune:
-            m_flat = mask[name].flatten()
-            m_flat[idx] = 0
-            mask[name] = m_flat.view(mask[name].shape)
-
-        for name in weights:
-            weights[name] = initial[name] * mask[name]
-
-        fitness = evaluator.evaluate_single(weights)
-        stats = circuit.stats(weights)
-        history.append({'round': rnd, 'pruned': n_prune, 'fitness': fitness, 'magnitude': stats['magnitude']})
-
-        if cfg.verbose:
-            print(f"      Round {rnd}: pruned {n_prune}, fitness={fitness:.4f}")
-
-        if fitness < cfg.fitness_threshold:
-            for _, name, idx in to_prune:
-                m_flat = mask[name].flatten()
-                m_flat[idx] = 1
-                mask[name] = m_flat.view(mask[name].shape)
-            for name in weights:
-                weights[name] = initial[name] * mask[name]
-            break
-
-    return PruneResult(
-        method='lottery',
-        original_stats=original,
-        final_stats=circuit.stats(weights),
-        final_weights=weights,
-        fitness=evaluator.evaluate_single(weights),
-        time_seconds=time.perf_counter() - start,
-        history=history
-    )
-
-
 def prune_topology(circuit: AdaptiveCircuit, evaluator: BatchedEvaluator, cfg: Config) -> PruneResult:
     """Topology search - remove connection groups."""
     start = time.perf_counter()
@@ -2092,14 +1960,14 @@ def prune_topology(circuit: AdaptiveCircuit, evaluator: BatchedEvaluator, cfg: C
     )
 
 
-def prune_structured(circuit: AdaptiveCircuit, evaluator: BatchedEvaluator, cfg: Config) -> PruneResult:
-    """Structured pruning - remove entire rows/columns of weight matrices."""
+def prune_structural(circuit: AdaptiveCircuit, evaluator: BatchedEvaluator, cfg: Config) -> PruneResult:
+    """Structural pruning - remove entire rows/columns of weight matrices."""
     start = time.perf_counter()
     weights = circuit.clone_weights()
     original = circuit.stats(weights)
 
     if cfg.verbose:
-        print(f"    Structured pruning (rows/columns)...")
+        print(f"    Structural pruning (rows/columns)...")
 
     removed = 0
 
@@ -2137,7 +2005,7 @@ def prune_structured(circuit: AdaptiveCircuit, evaluator: BatchedEvaluator, cfg:
         print(f"    Removed {removed} rows/columns")
 
     return PruneResult(
-        method='structured',
+        method='structural',
         original_stats=original,
         final_stats=circuit.stats(weights),
         final_weights=weights,
@@ -2279,99 +2147,6 @@ def prune_weight_sharing(circuit: AdaptiveCircuit, evaluator: BatchedEvaluator,
     )
 
 
-def prune_random(circuit: AdaptiveCircuit, evaluator: BatchedEvaluator, cfg: Config) -> PruneResult:
-    """Random search baseline."""
-    start = time.perf_counter()
-    original = circuit.stats()
-
-    if cfg.verbose:
-        print(f"    Random search ({cfg.random_iterations:,} iterations)...")
-
-    base_vector = circuit.weights_to_vector(circuit.weights)
-    best_weights = circuit.clone_weights()
-    best_mag = sum(t.abs().sum().item() for t in best_weights.values())
-    best_fitness = evaluator.evaluate_single(best_weights)
-
-    n_valid = 0
-
-    batch_size = min(10000, evaluator.max_batch)
-    n_batches = cfg.random_iterations // batch_size
-
-    for batch in range(n_batches):
-        population = base_vector.unsqueeze(0).expand(batch_size, -1).clone()
-        noise = torch.randn_like(population) * 2
-        population = (population + noise).round()
-
-        fitness = evaluator.evaluate_population(population)
-
-        valid_mask = fitness >= cfg.fitness_threshold
-        n_valid += valid_mask.sum().item()
-
-        if valid_mask.any():
-            magnitudes = population.abs().sum(dim=1)
-            magnitudes[~valid_mask] = float('inf')
-            best_idx = magnitudes.argmin().item()
-
-            if magnitudes[best_idx] < best_mag:
-                best_mag = magnitudes[best_idx].item()
-                best_weights = circuit.vector_to_weights(population[best_idx])
-                best_fitness = fitness[best_idx].item()
-
-        if cfg.verbose and batch % 10 == 0:
-            print(f"      Batch {batch}/{n_batches}: valid={n_valid}, best_mag={best_mag:.0f}")
-
-    return PruneResult(
-        method='random',
-        original_stats=original,
-        final_stats=circuit.stats(best_weights),
-        final_weights=best_weights,
-        fitness=best_fitness,
-        time_seconds=time.perf_counter() - start,
-        metadata={'total_valid': n_valid, 'total_tested': cfg.random_iterations}
-    )
-
-
-def prune_pareto(circuit: AdaptiveCircuit, evaluator: BatchedEvaluator, cfg: Config) -> PruneResult:
-    """Explore Pareto frontier of correctness vs. size."""
-    start = time.perf_counter()
-    original = circuit.stats()
-    frontier = []
-
-    if cfg.verbose:
-        print(f"    Exploring Pareto frontier...")
-
-    for target in cfg.pareto_levels:
-        relaxed_cfg = Config(
-            device=cfg.device,
-            fitness_threshold=target,
-            magnitude_passes=30,
-            verbose=False,
-            vram=cfg.vram
-        )
-
-        result = prune_magnitude(circuit, evaluator, relaxed_cfg)
-
-        frontier.append({
-            'target': target,
-            'actual': result.fitness,
-            'magnitude': result.final_stats['magnitude'],
-            'nonzero': result.final_stats['nonzero']
-        })
-
-        if cfg.verbose:
-            print(f"      Target {target:.2f}: fitness={result.fitness:.4f}, mag={result.final_stats['magnitude']:.0f}")
-
-    return PruneResult(
-        method='pareto',
-        original_stats=original,
-        final_stats=frontier[-1] if frontier else original,
-        final_weights=circuit.clone_weights(),
-        fitness=frontier[0]['actual'] if frontier else 1.0,
-        time_seconds=time.perf_counter() - start,
-        history=frontier
-    )
-
-
 def prune_depth(circuit: AdaptiveCircuit, evaluator: BatchedEvaluator, cfg: Config) -> PruneResult:
     """
     Depth reduction - attempt to collapse consecutive layers.
@@ -2790,9 +2565,9 @@ def _configs_at_magnitude(mag: int, n_params: int):
             yield tuple(signed)
 
 
-def prune_exhaustive(circuit: AdaptiveCircuit, evaluator: BatchedEvaluator, cfg: Config) -> PruneResult:
+def prune_exhaustive_mag(circuit: AdaptiveCircuit, evaluator: BatchedEvaluator, cfg: Config) -> PruneResult:
     """
-    Exhaustive search by magnitude level - finds provably optimal solutions.
+    Exhaustive search by magnitude level - finds provably minimum-magnitude solutions.
 
     Searches magnitude 0, then 1, then 2, ... until valid solutions found.
     Returns ALL valid solutions at the minimum magnitude (to discover families).
@@ -2924,7 +2699,7 @@ def prune_exhaustive(circuit: AdaptiveCircuit, evaluator: BatchedEvaluator, cfg:
         print(f"      - Time: {elapsed:.1f}s")
 
     return PruneResult(
-        method='exhaustive',
+        method='exhaustive_mag',
         original_stats=original,
         final_stats=circuit.stats(best_weights),
         final_weights=best_weights,
@@ -2939,71 +2714,194 @@ def prune_exhaustive(circuit: AdaptiveCircuit, evaluator: BatchedEvaluator, cfg:
     )
 
 
-def export_coq(circuit: AdaptiveCircuit, weights: Dict[str, torch.Tensor], cfg: Config) -> Path:
+def _configs_with_k_nonzeros(k: int, n_params: int, max_weight: int):
     """
-    Export threshold circuit to Coq for formal verification.
-    Generates a Coq file with the circuit definition and correctness theorem.
+    Generate all n_params-length configs with exactly k nonzero values.
+    Nonzero values range from -max_weight to +max_weight (excluding 0).
     """
-    cfg.coq_output_dir.mkdir(parents=True, exist_ok=True)
-
-    name = circuit.spec.name.replace('-', '_')
-    output_path = cfg.coq_output_dir / f'{name}.v'
-
-    lines = [
-        f'(* Threshold circuit: {circuit.spec.name} *)',
-        f'(* Auto-generated by threshold-pruner *)',
-        f'(* Inputs: {circuit.spec.inputs}, Outputs: {circuit.spec.outputs} *)',
-        '',
-        'Require Import ZArith.',
-        'Require Import List.',
-        'Import ListNotations.',
-        '',
-        '(* Threshold gate: output 1 if weighted sum >= 0 *)',
-        'Definition threshold (weights : list Z) (bias : Z) (inputs : list Z) : Z :=',
-        '  let sum := fold_left (fun acc wb => acc + fst wb * snd wb) ',
-        '              (combine weights inputs) bias in',
-        '  if Z.geb sum 0 then 1 else 0.',
-        '',
-        f'(* Circuit definition for {name} *)',
-    ]
+    if k > n_params or k < 0:
+        return
+
+    nonzero_vals = list(range(-max_weight, 0)) + list(range(1, max_weight + 1))
+
+    for positions in combinations(range(n_params), k):
+        position_set = set(positions)
+        for vals in product(nonzero_vals, repeat=k):
+            config = [0] * n_params
+            for pos, val in zip(positions, vals):
+                config[pos] = val
+            yield tuple(config)
+
+
+def prune_exhaustive_sparse(circuit: AdaptiveCircuit, evaluator: BatchedEvaluator, cfg: Config) -> PruneResult:
+    """
+    Exhaustive search by sparsity level - finds provably maximum-sparsity solutions.
+
+    Searches from 1 nonzero, then 2, then 3, ... until valid solutions found.
+    Returns ALL valid solutions at the minimum nonzero count (to discover families).
+
+    Useful for hardware where connection count matters more than weight magnitude.
+    """
+    start = time.perf_counter()
+    original = circuit.stats()
+
+    n_params = original['total']
+    original_nonzeros = original['nonzero']
+    max_weight = cfg.sparse_max_weight
+
+    if n_params > cfg.exhaustive_max_params:
+        if cfg.verbose:
+            print(f"    [SPARSE] Skipping: {n_params} params exceeds max {cfg.exhaustive_max_params}")
+        return PruneResult(
+            method='exhaustive_sparse',
+            original_stats=original,
+            final_stats=original,
+            final_weights=circuit.clone_weights(),
+            fitness=evaluator.evaluate_single(circuit.weights),
+            time_seconds=time.perf_counter() - start,
+            metadata={'skipped': True, 'reason': 'too_many_params'}
+        )
+
+    if cfg.verbose:
+        print(f"    [SPARSE] Parameters: {n_params}")
+        print(f"    [SPARSE] Original nonzeros: {original_nonzeros}")
+        print(f"    [SPARSE] Max weight magnitude: {max_weight}")
+        print(f"    [SPARSE] Searching by nonzero count (1, 2, 3, ...)")
+
+    weight_keys = list(circuit.weights.keys())
+    weight_shapes = {k: circuit.weights[k].shape for k in weight_keys}
+    weight_sizes = {k: circuit.weights[k].numel() for k in weight_keys}
+
+    def vector_to_weights(vec):
+        weights = {}
+        idx = 0
+        for k in weight_keys:
+            size = weight_sizes[k]
+            weights[k] = torch.tensor(vec[idx:idx+size], dtype=torch.float32, device=cfg.device).view(weight_shapes[k])
+            idx += size
+        return weights
+
+    total_tested = 0
+    all_solutions = []
+    optimal_nonzeros = None
+
+    for n_nonzero in range(1, n_params + 1):
+        nz_start = time.perf_counter()
+
+        n_positions = math.comb(n_params, n_nonzero)
+        n_value_combos = (2 * max_weight) ** n_nonzero
+        n_configs = n_positions * n_value_combos
+
+        if cfg.verbose:
+            print(f"    Nonzeros {n_nonzero}: {n_configs:,} configurations...", end=" ", flush=True)
+
+        valid_at_nz = []
+
+        batch_configs = []
+        batch_size = min(100000, n_configs)
+
+        for config in _configs_with_k_nonzeros(n_nonzero, n_params, max_weight):
+            batch_configs.append(config)
 
-    neuron_defs = []
-    for neuron_name in circuit.graph.neuron_order:
-        info = circuit.graph.neurons[neuron_name]
-        w_key = info.get('weight_key')
-        b_key = info.get('bias_key')
+            if len(batch_configs) >= batch_size:
+                population = torch.tensor(batch_configs, dtype=torch.float32, device=cfg.device)
 
-        if w_key and w_key in weights:
-            w = weights[w_key].flatten().tolist()
-            b = weights[b_key].item() if b_key and b_key in weights else 0
+                try:
+                    fitness_batch = evaluator.evaluate_population(population)
+                except:
+                    fitness_batch = torch.tensor([
+                        evaluator.evaluate_single(vector_to_weights(c))
+                        for c in batch_configs
+                    ], device=cfg.device)
 
-            w_str = '[' + '; '.join(str(int(x)) for x in w) + ']'
-            safe_name = neuron_name.replace('.', '_').replace('-', '_')
+                valid_mask = fitness_batch >= cfg.fitness_threshold
+                for i, is_valid in enumerate(valid_mask.tolist()):
+                    if is_valid:
+                        valid_at_nz.append(batch_configs[i])
+
+                total_tested += len(batch_configs)
+                batch_configs = []
+
+        if batch_configs:
+            population = torch.tensor(batch_configs, dtype=torch.float32, device=cfg.device)
+
+            try:
+                fitness_batch = evaluator.evaluate_population(population)
+            except:
+                fitness_batch = torch.tensor([
+                    evaluator.evaluate_single(vector_to_weights(c))
+                    for c in batch_configs
+                ], device=cfg.device)
+
+            valid_mask = fitness_batch >= cfg.fitness_threshold
+            for i, is_valid in enumerate(valid_mask.tolist()):
+                if is_valid:
+                    valid_at_nz.append(batch_configs[i])
+
+            total_tested += len(batch_configs)
+
+        nz_time = time.perf_counter() - nz_start
+
+        if valid_at_nz:
+            if cfg.verbose:
+                print(f"FOUND {len(valid_at_nz)} solutions! ({nz_time:.2f}s)")
+
+            optimal_nonzeros = n_nonzero
+            all_solutions = valid_at_nz
+
+            if cfg.verbose:
+                print(f"    [SPARSE] Optimal nonzeros: {optimal_nonzeros}")
+                print(f"    [SPARSE] Solutions found: {len(all_solutions)}")
+                print(f"    [SPARSE] Solution analysis:")
+                print(f"      {'#':<3} {'NZ':<4} {'Mag':<6} {'Max|w|':<7} {'Weights'}")
+                print(f"      {'-'*60}")
+                for i, sol in enumerate(all_solutions[:20]):
+                    nz = sum(1 for v in sol if v != 0)
+                    mag = sum(abs(v) for v in sol)
+                    max_w = max(abs(v) for v in sol) if any(v != 0 for v in sol) else 0
+                    print(f"      {i+1:<3} {nz:<4} {mag:<6} {max_w:<7} {sol}")
+                if len(all_solutions) > 20:
+                    print(f"      ... and {len(all_solutions) - 20} more")
 
-            neuron_defs.append(f'Definition {safe_name}_weights : list Z := {w_str}.')
-            neuron_defs.append(f'Definition {safe_name}_bias : Z := {int(b)}.')
-            neuron_defs.append('')
+            break
+        else:
+            if cfg.verbose:
+                print(f"none ({nz_time:.2f}s)")
 
-    lines.extend(neuron_defs)
+    elapsed = time.perf_counter() - start
 
-    lines.extend([
-        '',
-        f'(* Correctness theorem placeholder *)',
-        f'(* To be completed with specific input/output verification *)',
-        f'Theorem {name}_correct : forall inputs,',
-        f'  length inputs = {circuit.spec.inputs}%nat ->',
-        f'  (* output matches expected *)',
-        f'  True.',
-        'Proof.',
-        '  intros.',
-        '  (* Proof to be completed *)',
-        'Admitted.',
-    ])
+    if all_solutions:
+        best_combo = min(all_solutions, key=lambda x: sum(abs(v) for v in x))
+        best_weights = vector_to_weights(best_combo)
+        best_fitness = evaluator.evaluate_single(best_weights)
+    else:
+        best_weights = circuit.clone_weights()
+        best_fitness = evaluator.evaluate_single(best_weights)
+        optimal_nonzeros = original_nonzeros
 
-    with open(output_path, 'w', encoding='utf-8') as f:
-        f.write('\n'.join(lines))
+    if cfg.verbose:
+        final_stats = circuit.stats(best_weights)
+        print(f"    [SPARSE COMPLETE]")
+        print(f"      - Configurations tested: {total_tested:,}")
+        print(f"      - Optimal nonzeros: {optimal_nonzeros} (original: {original_nonzeros})")
+        print(f"      - Total solutions at optimal: {len(all_solutions)}")
+        print(f"      - Sparsity: {(1 - optimal_nonzeros/n_params)*100:.1f}%")
+        print(f"      - Time: {elapsed:.1f}s")
 
-    return output_path
+    return PruneResult(
+        method='exhaustive_sparse',
+        original_stats=original,
+        final_stats=circuit.stats(best_weights),
+        final_weights=best_weights,
+        fitness=best_fitness,
+        time_seconds=elapsed,
+        metadata={
+            'optimal_nonzeros': optimal_nonzeros,
+            'total_tested': total_tested,
+            'solutions_count': len(all_solutions),
+            'all_solutions': all_solutions[:100]
+        }
+    )
 
 
 def run_all_methods(circuit: AdaptiveCircuit, cfg: Config) -> Dict[str, PruneResult]:
@@ -3040,21 +2938,18 @@ def run_all_methods(circuit: AdaptiveCircuit, cfg: Config) -> Dict[str, PruneRes
         ('magnitude', cfg.run_magnitude, lambda: prune_magnitude(circuit, evaluator, cfg)),
         ('zero', cfg.run_zero, lambda: prune_zero(circuit, evaluator, cfg)),
         ('quantize', cfg.run_quantize, lambda: prune_quantize(circuit, evaluator, cfg)),
-        ('neuron', cfg.run_neuron, lambda: prune_neuron(circuit, evaluator, cfg)),
-        ('lottery', cfg.run_lottery, lambda: prune_lottery(circuit, evaluator, cfg)),
+        ('structural', cfg.run_structural, lambda: prune_structural(circuit, evaluator, cfg)),
         ('topology', cfg.run_topology, lambda: prune_topology(circuit, evaluator, cfg)),
-        ('structured', cfg.run_structured, lambda: prune_structured(circuit, evaluator, cfg)),
         ('sensitivity', cfg.run_sensitivity, lambda: prune_sensitivity(circuit, evaluator, cfg)),
         ('weight_sharing', cfg.run_weight_sharing, lambda: prune_weight_sharing(circuit, evaluator, cfg)),
         ('depth', cfg.run_depth, lambda: prune_depth(circuit, evaluator, cfg)),
         ('gate_subst', cfg.run_gate_subst, lambda: prune_gate_substitution(circuit, evaluator, cfg)),
         ('symmetry', cfg.run_symmetry, lambda: prune_symmetry(circuit, evaluator, cfg)),
         ('fanin', cfg.run_fanin, lambda: prune_fanin(circuit, evaluator, cfg)),
-        ('exhaustive', cfg.run_exhaustive, lambda: prune_exhaustive(circuit, evaluator, cfg)),
-        ('random', cfg.run_random, lambda: prune_random(circuit, evaluator, cfg)),
+        ('exhaustive_mag', cfg.run_exhaustive_mag, lambda: prune_exhaustive_mag(circuit, evaluator, cfg)),
+        ('exhaustive_sparse', cfg.run_exhaustive_sparse, lambda: prune_exhaustive_sparse(circuit, evaluator, cfg)),
         ('evolutionary', cfg.run_evolutionary, lambda: prune_evolutionary(circuit, evaluator, cfg)),
         ('annealing', cfg.run_annealing, lambda: prune_annealing(circuit, evaluator, cfg)),
-        ('pareto', cfg.run_pareto, lambda: prune_pareto(circuit, evaluator, cfg)),
     ]
 
     enabled_methods = [(name, fn) for name, enabled, fn in methods if enabled]
@@ -3100,10 +2995,6 @@ def run_all_methods(circuit: AdaptiveCircuit, cfg: Config) -> Dict[str, PruneRes
         reduction = 1 - best_mag / original['magnitude']
         print(f"\n BEST: {best_method} ({reduction * 100:.1f}% magnitude reduction)")
 
-        if cfg.export_coq:
-            coq_path = export_coq(circuit, results[best_method].final_weights, cfg)
-            print(f" Coq export: {coq_path}")
-
     return results
 
 
@@ -3228,8 +3119,9 @@ def main():
     parser.add_argument('--sa-iters', type=int, default=50000, help='Simulated annealing iterations')
     parser.add_argument('--sa-chains', type=int, default=0, help='Parallel SA chains (0=auto)')
     parser.add_argument('--vram-target', type=float, default=0.75)
-    parser.add_argument('--export-coq', action='store_true')
     parser.add_argument('--fanin-target', type=int, default=4)
+    parser.add_argument('--sparse-max-weight', type=int, default=3, help='Max weight magnitude for sparse search')
+    parser.add_argument('--exhaustive-max-params', type=int, default=12, help='Max params for exhaustive search')
 
     args = parser.parse_args()
 
@@ -3251,15 +3143,16 @@ def main():
         evo_generations=args.evo_gens,
         annealing_iterations=args.sa_iters,
         annealing_parallel_chains=args.sa_chains,
-        export_coq=args.export_coq,
-        fanin_target=args.fanin_target
+        fanin_target=args.fanin_target,
+        sparse_max_weight=args.sparse_max_weight,
+        exhaustive_max_params=args.exhaustive_max_params
     )
 
     if args.methods:
         all_methods = ['magnitude', 'zero', 'quantize', 'evolutionary', 'annealing',
-                       'neuron', 'lottery', 'topology', 'structured', 'sensitivity',
-                       'weight_sharing', 'random', 'pareto', 'depth', 'gate_subst',
-                       'symmetry', 'fanin', 'exhaustive']
+                       'structural', 'topology', 'sensitivity', 'weight_sharing',
+                       'depth', 'gate_subst', 'symmetry', 'fanin',
+                       'exhaustive_mag', 'exhaustive_sparse']
         for m in all_methods:
             setattr(cfg, f'run_{m}', False)
 
@@ -3271,19 +3164,16 @@ def main():
                 'quant': 'quantize', 'quantize': 'quantize',
                 'evo': 'evolutionary', 'evolutionary': 'evolutionary',
                 'anneal': 'annealing', 'annealing': 'annealing', 'sa': 'annealing',
-                'neuron': 'neuron',
-                'lottery': 'lottery',
+                'structural': 'structural', 'struct': 'structural',
                 'topo': 'topology', 'topology': 'topology',
-                'struct': 'structured', 'structured': 'structured',
                 'sens': 'sensitivity', 'sensitivity': 'sensitivity',
                 'share': 'weight_sharing', 'weight_sharing': 'weight_sharing', 'sharing': 'weight_sharing',
-                'rand': 'random', 'random': 'random',
-                'pareto': 'pareto',
                 'depth': 'depth',
                 'gate': 'gate_subst', 'gate_subst': 'gate_subst', 'subst': 'gate_subst',
                 'sym': 'symmetry', 'symmetry': 'symmetry',
                 'fanin': 'fanin', 'fan': 'fanin',
-                'exhaustive': 'exhaustive', 'exh': 'exhaustive', 'brute': 'exhaustive'
+                'exhaustive_mag': 'exhaustive_mag', 'exh_mag': 'exhaustive_mag', 'exh': 'exhaustive_mag', 'brute': 'exhaustive_mag',
+                'exhaustive_sparse': 'exhaustive_sparse', 'exh_sparse': 'exhaustive_sparse', 'sparse': 'exhaustive_sparse'
             }
             if m in method_map:
                 setattr(cfg, f'run_{method_map[m]}', True)
@@ -3343,6 +3233,11 @@ def main():
         print("  python prune.py threshold-hamming74decoder --methods evo")
         print("  python prune.py threshold-xor --methods evo --evo-pop 500000 --evo-gens 5000")
         print("")
+        print("  # Exhaustive search (provably optimal):")
+        print("  python prune.py threshold-xor --methods exh_mag        # minimize magnitude")
+        print("  python prune.py threshold-xor --methods exh_sparse     # minimize nonzeros")
+        print("  python prune.py threshold-mux --methods sparse --sparse-max-weight 2")
+        print("")
         print("  # Pipeline mode (chained, each stage feeds into next):")
         print("  python prune.py threshold-hamming74decoder --pipeline evo,mag,zero,quant --save")
         print("  python prune.py threshold-xor --pipeline anneal,mag,zero --sa-iters 100000")