Add pruned variant documentation

README.md

@@ -21,7 +21,18 @@ This is a ternary threshold network trained to compute the parity function on 8-
 
 **Key feature**: Correctness is mathematically proven in Coq for all 256 possible inputs.
 
-## Architecture
+## Variants
+
+Two variants are available:
+
+| Variant | Architecture | Parameters | Location |
+|---------|--------------|------------|----------|
+| Full | 8 → 32 → 16 → 1 | 833 | `model.safetensors` |
+| Pruned | 8 → 11 → 3 → 1 | 139 | `pruned/model.safetensors` |
+
+The pruned variant was extracted via neuron ablation analysis, which identified that only 11 of 32 Layer-1 neurons and 3 of 16 Layer-2 neurons are critical for correct operation. Both variants achieve 100% accuracy and are formally verified in Coq.
+
+## Architecture (Full Network)
 
 | Layer | Neurons | Weights | Activation |
 |-------|---------|---------|------------|
@@ -30,7 +41,7 @@ This is a ternary threshold network trained to compute the parity function on 8-
 | Hidden 2 | 16 | Ternary {-1, 0, +1} | Heaviside |
 | Output | 1 | Ternary {-1, 0, +1} | Heaviside |
 
-- **Total parameters**: 833
+- **Total parameters**: 833 (full), 139 (pruned)
 - **Weight quantization**: Ternary (-1, 0, +1)
 - **Bias quantization**: Bounded integers
 
@@ -47,7 +58,7 @@ Evolutionary search circumvents this problem by evaluating candidate solutions d
 
 ## Verification
 
-Correctness is proven in the Coq proof assistant:
+Correctness is proven in the Coq proof assistant for both variants:
 
 ```coq
 Theorem network_verified :
@@ -62,8 +73,13 @@ The proof uses exhaustive enumeration via `vm_compute` over all 256 inputs.
 from model import ThresholdNetwork
 import torch
 
+# Full network
 model = ThresholdNetwork.from_safetensors('model.safetensors')
 
+# Or pruned network
+from pruned.model import PrunedThresholdNetwork
+model = PrunedThresholdNetwork.from_safetensors('pruned/model.safetensors')
+
 input_bits = torch.tensor([[1, 0, 1, 1, 0, 0, 1, 0]], dtype=torch.float32)
 output = model(input_bits)
 print(f"Parity: {int(output.item())}")  # 0 (four 1-bits, even count)
@@ -71,16 +87,17 @@ print(f"Parity: {int(output.item())}")  # 0 (four 1-bits, even count)
 
 ## Performance
 
-| Metric | Value |
-|--------|-------|
-| Accuracy | 100% (256/256) |
-| Verification | Coq-proven |
+| Metric | Full | Pruned |
+|--------|------|--------|
+| Accuracy | 100% (256/256) | 100% (256/256) |
+| Parameters | 833 | 139 |
+| Verification | Coq-proven | Coq-proven |
 
 ## Limitations
 
 - Fixed 8-bit input size
 - Threshold activation (not differentiable)
-- Architecture found by search, not optimized for size
+- Fragile to input noise (Heaviside has zero margin)
 
 ## Repository