Rename from tiny-mod7-verified

README.md

@@ -0,0 +1,94 @@
+---
+license: mit
+tags:
+- pytorch
+- safetensors
+- threshold-logic
+- neuromorphic
+- modular-arithmetic
+---
+
+# threshold-mod7
+
+Computes Hamming weight mod 7 for 8-bit inputs. Multi-layer network with thermometer encoding.
+
+## Circuit
+
+```
+  x₀ x₁ x₂ x₃ x₄ x₅ x₆ x₇
+   │  │  │  │  │  │  │  │
+   └──┴──┴──┴──┼──┴──┴──┴──┘
+               ▼
+       ┌─────────────┐
+       │ Thermometer │  Layer 1: 9 neurons
+       └─────────────┘
+               │
+               ▼
+       ┌─────────────┐
+       │  MOD-7      │  Layer 2: 6 neurons
+       │  Detection  │  Pattern (1,1,1,1,1,1,-6)
+       └─────────────┘
+               │
+               ▼
+       ┌─────────────┐
+       │  Classify   │  Output: 7 classes
+       └─────────────┘
+               │
+               ▼
+      {0, 1, 2, 3, 4, 5, 6}
+```
+
+## Algebraic Insight
+
+Pattern `(1, 1, 1, 1, 1, 1, -6)` cycles mod 7:
+
+```
+HW=0: sum=0 → 0 mod 7
+...
+HW=6: sum=6 → 6 mod 7
+HW=7: sum=0 → 0 mod 7  (reset: 1+1+1+1+1+1-6=0)
+HW=8: sum=1 → 1 mod 7
+```
+
+For 8-bit inputs, only one reset occurs (at HW=7).
+
+## Architecture
+
+| Layer | Neurons | Function |
+|-------|---------|----------|
+| Input | 8 | Binary bits |
+| Hidden 1 | 9 | Thermometer encoding |
+| Hidden 2 | 6 | MOD-7 detection |
+| Output | 7 | One-hot classification |
+
+**Total: 22 neurons, 190 parameters**
+
+## 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)
+```
+
+## Files
+
+```
+threshold-mod7/
+├── model.safetensors
+├── model.py
+├── config.json
+└── README.md
+```
+
+## License
+
+MIT

config.json

@@ -0,0 +1,31 @@
+{
+  "model_type": "threshold_network",
+  "task": "mod7_classification",
+  "architecture": "8 -> 9 -> 6 -> 7",
+  "input_size": 8,
+  "hidden1_size": 9,
+  "hidden2_size": 6,
+  "output_size": 7,
+  "num_parameters": 190,
+  "num_neurons": 22,
+  "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,1,1,1,1,-6) on thermometer encoding produce cumsum = HW mod 7",
+  "github": "https://github.com/CharlesCNorton/mod7-verified",
+  "related": {
+    "mod5_model": "https://huggingface.co/phanerozoic/tiny-mod5-prover",
+    "mod3_model": "https://huggingface.co/phanerozoic/tiny-mod3-prover",
+    "parity_model": "https://huggingface.co/phanerozoic/tiny-parity-prover"
+  }
+}

model.py

@@ -0,0 +1,68 @@
+"""
+Inference code for mod7-verified threshold network.
+
+This network computes MOD-7 (Hamming weight mod 7) on 8-bit binary inputs.
+"""
+
+import torch
+import torch.nn as nn
+from safetensors.torch import load_file
+
+
+def heaviside(x):
+    return (x >= 0).float()
+
+
+class Mod7Network(nn.Module):
+    """
+    Verified threshold network for MOD-7 computation.
+    Architecture: 8 -> 9 -> 6 -> 7
+    """
+
+    def __init__(self):
+        super().__init__()
+        self.layer1 = nn.Linear(8, 9)
+        self.layer2 = nn.Linear(9, 6)
+        self.output = nn.Linear(6, 7)
+
+    def forward(self, x):
+        x = x.float()
+        x = heaviside(self.layer1(x))
+        x = heaviside(self.layer2(x))
+        return self.output(x)
+
+    def predict(self, x):
+        return self.forward(x).argmax(dim=-1)
+
+    @classmethod
+    def from_safetensors(cls, path):
+        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 mod7_reference(x):
+    return (x.sum(dim=-1) % 7).long()
+
+
+def verify(model):
+    inputs = torch.zeros(256, 8)
+    for i in range(256):
+        for j in range(8):
+            inputs[i, j] = (i >> j) & 1
+    targets = mod7_reference(inputs)
+    predictions = model.predict(inputs)
+    correct = (predictions == targets).sum().item()
+    print(f"Verification: {correct}/256 ({100*correct/256:.1f}%)")
+    return correct == 256
+
+
+if __name__ == '__main__':
+    model = Mod7Network.from_safetensors('model.safetensors')
+    verify(model)

model.safetensors

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