Rename from tiny-mod4-verified

README.md

@@ -0,0 +1,94 @@
+---
+license: mit
+tags:
+- pytorch
+- safetensors
+- threshold-logic
+- neuromorphic
+- modular-arithmetic
+---
+
+# threshold-mod4
+
+Computes Hamming weight mod 4 directly on inputs. Single-layer circuit using repeated weight pattern.
+
+## Circuit
+
+```
+  x₀ x₁ x₂ x₃ x₄ x₅ x₆ x₇
+   │  │  │  │  │  │  │  │
+   │  │  │  │  │  │  │  │
+   w: 1  1  1 -3  1  1  1 -3
+   └──┴──┴──┴──┼──┴──┴──┴──┘
+               ▼
+          ┌─────────┐
+          │ b:  0   │
+          └─────────┘
+               │
+               ▼
+           HW mod 4
+```
+
+## Algebraic Insight
+
+The pattern `(1, 1, 1, -3)` repeats twice across 8 inputs:
+
+- Positions 1-3: weight +1 each
+- Position 4: weight -3 (reset: 1+1+1-3 = 0)
+- Positions 5-7: weight +1 each
+- Position 8: weight -3 (reset again)
+
+Every 4 bits, the sum resets. For 8 bits, two complete cycles.
+
+```
+HW=0: sum=0 → 0 mod 4
+HW=1: sum=1 → 1 mod 4
+HW=2: sum=2 → 2 mod 4
+HW=3: sum=3 → 3 mod 4
+HW=4: sum=0 → 0 mod 4  (reset)
+...
+```
+
+## Parameters
+
+| | |
+|---|---|
+| Weights | [1, 1, 1, -3, 1, 1, 1, -3] |
+| Bias | 0 |
+| Total | 9 parameters |
+
+## MOD-m Family
+
+| m | Weight pattern |
+|---|----------------|
+| 3 | (1, 1, -2) |
+| **4** | **(1, 1, 1, -3)** |
+| 5 | (1, 1, 1, 1, -4) |
+| m | (1, ..., 1, 1-m) with m-1 ones |
+
+## Usage
+
+```python
+from safetensors.torch import load_file
+import torch
+
+w = load_file('model.safetensors')
+
+def mod4(bits):
+    inputs = torch.tensor([float(b) for b in bits])
+    return int((inputs * w['weight']).sum() + w['bias'])
+```
+
+## Files
+
+```
+threshold-mod4/
+├── model.safetensors
+├── model.py
+├── config.json
+└── README.md
+```
+
+## License
+
+MIT

config.json

@@ -0,0 +1,23 @@
+{
+  "model_type": "threshold_network",
+  "task": "mod4_classification",
+  "architecture": "8 -> 1",
+  "input_size": 8,
+  "output_size": 1,
+  "num_neurons": 1,
+  "num_parameters": 9,
+  "modulus": 4,
+  "activation": "heaviside",
+  "weight_constraints": "integer",
+  "weight_pattern": "[1, 1, 1, -3, 1, 1, 1, -3]",
+  "verification": {
+    "method": "coq_proof",
+    "exhaustive": true,
+    "inputs_tested": 256
+  },
+  "accuracy": {
+    "all_inputs": "256/256",
+    "percentage": 100.0
+  },
+  "github": "https://github.com/CharlesCNorton/coq-circuits"
+}

model.py

@@ -0,0 +1,54 @@
+"""
+Threshold Network for MOD-4 Circuit
+
+A formally verified threshold network computing Hamming weight mod 4.
+Uses the algebraic weight pattern [1, 1, 1, -3, 1, 1, 1, -3].
+"""
+
+import torch
+from safetensors.torch import load_file
+
+
+class ThresholdMod4:
+    """
+    MOD-4 circuit using threshold logic.
+
+    Weight pattern: (1, 1, 1, 1-m) repeating for m=4
+    Computes cumulative sum that cycles mod 4.
+    """
+
+    def __init__(self, weights_dict):
+        self.weight = weights_dict['weight']
+        self.bias = weights_dict['bias']
+
+    def __call__(self, bits):
+        inputs = torch.tensor([float(b) for b in bits])
+        weighted_sum = (inputs * self.weight).sum() + self.bias
+        return weighted_sum
+
+    def get_residue(self, bits):
+        """Returns Hamming weight mod 4."""
+        return sum(bits) % 4
+
+    @classmethod
+    def from_safetensors(cls, path="model.safetensors"):
+        return cls(load_file(path))
+
+
+def forward(x, weights):
+    x = torch.as_tensor(x, dtype=torch.float32)
+    weighted_sum = (x * weights['weight']).sum(dim=-1) + weights['bias']
+    return weighted_sum
+
+
+if __name__ == "__main__":
+    weights = load_file("model.safetensors")
+    model = ThresholdMod4(weights)
+
+    print("MOD-4 Circuit Tests:")
+    print("-" * 40)
+    for hw in range(9):
+        bits = [1]*hw + [0]*(8-hw)
+        out = model(bits).item()
+        expected_residue = hw % 4
+        print(f"HW={hw}: weighted_sum={out:.0f}, HW mod 4 = {expected_residue}")

model.safetensors

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