Rename from tiny-mod3-verified

README.md

@@ -0,0 +1,109 @@
+---
+license: mit
+tags:
+- pytorch
+- safetensors
+- threshold-logic
+- neuromorphic
+- modular-arithmetic
+---
+
+# threshold-mod3
+
+Computes Hamming weight mod 3 for 8-bit inputs. Multi-layer network using thermometer encoding.
+
+## Circuit
+
+```
+  x₀ x₁ x₂ x₃ x₄ x₅ x₆ x₇
+   │  │  │  │  │  │  │  │
+   └──┴──┴──┴──┼──┴──┴──┴──┘
+               ▼
+       ┌─────────────┐
+       │ Thermometer │  Layer 1: 9 neurons
+       │  Encoding   │  Fires when HW ≥ k
+       └─────────────┘
+               │
+               ▼
+       ┌─────────────┐
+       │  MOD-3      │  Layer 2: 2 neurons
+       │  Detection  │  Weight pattern (1,1,-2)
+       └─────────────┘
+               │
+               ▼
+       ┌─────────────┐
+       │  Classify   │  Output: 3 classes
+       └─────────────┘
+               │
+               ▼
+          {0, 1, 2}
+```
+
+## Algebraic Insight
+
+The weight pattern `(1, 1, -2)` causes cumulative sums to cycle mod 3:
+
+```
+HW=0: sum=0 → 0 mod 3
+HW=1: sum=1 → 1 mod 3
+HW=2: sum=2 → 2 mod 3
+HW=3: sum=0 → 0 mod 3  (reset: 1+1-2=0)
+HW=4: sum=1 → 1 mod 3
+...
+```
+
+The key: `1 + 1 + (1-3) = 0`. Every 3 increments, the sum resets.
+
+This generalizes to MOD-m: use `(1, 1, ..., 1, 1-m)` with m-1 ones.
+
+## Architecture
+
+| Layer | Neurons | Function |
+|-------|---------|----------|
+| Input | 8 | Binary bits |
+| Hidden 1 | 9 | Thermometer: fires when HW ≥ k |
+| Hidden 2 | 2 | MOD-3 detection |
+| Output | 3 | One-hot classification |
+
+**Total: 14 neurons, 110 parameters**
+
+## Output Distribution
+
+| Class | HW values | Count/256 |
+|-------|-----------|-----------|
+| 0 | 0, 3, 6 | 85 |
+| 1 | 1, 4, 7 | 86 |
+| 2 | 2, 5, 8 | 85 |
+
+## Usage
+
+```python
+from safetensors.torch import load_file
+import torch
+
+w = load_file('model.safetensors')
+
+def forward(x):
+    x = x.float()
+    x = (x @ w['layer1.weight'].T + w['layer1.bias'] >= 0).float()
+    x = (x @ w['layer2.weight'].T + w['layer2.bias'] >= 0).float()
+    out = x @ w['output.weight'].T + w['output.bias']
+    return out.argmax(dim=-1)
+
+inp = torch.tensor([[1,0,1,1,0,0,1,0]])  # HW=4
+print(forward(inp).item())  # 1 (4 mod 3 = 1)
+```
+
+## Files
+
+```
+threshold-mod3/
+├── model.safetensors
+├── model.py
+├── config.json
+└── README.md
+```
+
+## License
+
+MIT

config.json

@@ -0,0 +1,30 @@
+{
+  "model_type": "threshold_network",
+  "task": "mod3_classification",
+  "architecture": "8 -> 9 -> 2 -> 3",
+  "input_size": 8,
+  "hidden1_size": 9,
+  "hidden2_size": 2,
+  "output_size": 3,
+  "num_parameters": 110,
+  "num_neurons": 14,
+  "activation": "heaviside",
+  "weight_constraints": "integer",
+  "verification": {
+    "method": "coq_proof",
+    "exhaustive": true,
+    "constructive": true,
+    "algebraic": true,
+    "axiom_free": true
+  },
+  "accuracy": {
+    "all_inputs": "256/256",
+    "percentage": 100.0
+  },
+  "algebraic_insight": "Weights (1,1,-2) on thermometer encoding produce cumsum = HW mod 3",
+  "github": "https://github.com/CharlesCNorton/mod3-verified",
+  "related": {
+    "parity_model": "https://huggingface.co/phanerozoic/tiny-parity-prover",
+    "parity_proofs": "https://github.com/CharlesCNorton/threshold-logic-verified"
+  }
+}

model.py

@@ -0,0 +1,119 @@
+"""
+Inference code for mod3-verified threshold network.
+
+This network computes MOD-3 (Hamming weight mod 3) on 8-bit binary inputs.
+"""
+
+import torch
+import torch.nn as nn
+from safetensors.torch import load_file
+
+
+def heaviside(x):
+    """Heaviside step function: 1 if x >= 0, else 0."""
+    return (x >= 0).float()
+
+
+class Mod3Network(nn.Module):
+    """
+    Verified threshold network for MOD-3 computation.
+
+    Architecture: 8 -> 9 -> 2 -> 3
+    - Layer 1: Thermometer encoding (9 neurons detect HW >= k)
+    - Layer 2: MOD-3 detection using (1,1,-2) weight pattern
+    - Output: 3-class classification
+    """
+
+    def __init__(self):
+        super().__init__()
+        self.layer1 = nn.Linear(8, 9)
+        self.layer2 = nn.Linear(9, 2)
+        self.output = nn.Linear(2, 3)
+
+    def forward(self, x):
+        """Forward pass with Heaviside activation."""
+        x = x.float()
+        x = heaviside(self.layer1(x))
+        x = heaviside(self.layer2(x))
+        x = self.output(x)
+        return x
+
+    def predict(self, x):
+        """Get predicted class (0, 1, or 2)."""
+        return self.forward(x).argmax(dim=-1)
+
+    @classmethod
+    def from_safetensors(cls, path):
+        """Load model from safetensors file."""
+        model = cls()
+        weights = load_file(path)
+
+        model.layer1.weight.data = weights['layer1.weight']
+        model.layer1.bias.data = weights['layer1.bias']
+        model.layer2.weight.data = weights['layer2.weight']
+        model.layer2.bias.data = weights['layer2.bias']
+        model.output.weight.data = weights['output.weight']
+        model.output.bias.data = weights['output.bias']
+
+        return model
+
+
+def mod3_reference(x):
+    """Reference implementation: Hamming weight mod 3."""
+    return (x.sum(dim=-1) % 3).long()
+
+
+def verify(model, verbose=True):
+    """Verify model on all 256 inputs."""
+    inputs = torch.zeros(256, 8)
+    for i in range(256):
+        for j in range(8):
+            inputs[i, j] = (i >> j) & 1
+
+    targets = mod3_reference(inputs)
+    predictions = model.predict(inputs)
+
+    correct = (predictions == targets).sum().item()
+
+    if verbose:
+        print(f"Verification: {correct}/256 ({100*correct/256:.1f}%)")
+
+        if correct < 256:
+            errors = (predictions != targets).nonzero(as_tuple=True)[0]
+            print(f"Errors at indices: {errors[:10].tolist()}")
+
+    return correct == 256
+
+
+def demo():
+    """Demonstration of MOD-3 computation."""
+    print("Loading mod3-verified model...")
+    model = Mod3Network.from_safetensors('model.safetensors')
+
+    print("\nVerifying on all 256 inputs...")
+    verify(model)
+
+    print("\nExample predictions:")
+    test_cases = [
+        [0, 0, 0, 0, 0, 0, 0, 0],  # HW=0, 0 mod 3 = 0
+        [1, 0, 0, 0, 0, 0, 0, 0],  # HW=1, 1 mod 3 = 1
+        [1, 1, 0, 0, 0, 0, 0, 0],  # HW=2, 2 mod 3 = 2
+        [1, 1, 1, 0, 0, 0, 0, 0],  # HW=3, 3 mod 3 = 0
+        [1, 1, 1, 1, 0, 0, 0, 0],  # HW=4, 4 mod 3 = 1
+        [1, 1, 1, 1, 1, 0, 0, 0],  # HW=5, 5 mod 3 = 2
+        [1, 1, 1, 1, 1, 1, 0, 0],  # HW=6, 6 mod 3 = 0
+        [1, 1, 1, 1, 1, 1, 1, 0],  # HW=7, 7 mod 3 = 1
+        [1, 1, 1, 1, 1, 1, 1, 1],  # HW=8, 8 mod 3 = 2
+    ]
+
+    for bits in test_cases:
+        x = torch.tensor([bits], dtype=torch.float32)
+        hw = sum(bits)
+        pred = model.predict(x).item()
+        expected = hw % 3
+        status = "OK" if pred == expected else "ERROR"
+        print(f"  {bits} -> HW={hw}, pred={pred}, expected={expected} [{status}]")
+
+
+if __name__ == '__main__':
+    demo()

model.safetensors

@@ -0,0 +1,3 @@
+version https://git-lfs.github.com/spec/v1
+oid sha256:a4dfa3053aa3ab1ec347bd4099c326bb03a2fe05da16a6beeed66cfc35bd1b57
+size 864

tmpclaude-9499-cwd

@@ -0,0 +1 @@
+/d/mod3-verified/hf