Rename from tiny-NOT-verified

README.md

@@ -0,0 +1,74 @@
+---
+license: mit
+tags:
+- pytorch
+- safetensors
+- threshold-logic
+- neuromorphic
+---
+
+# threshold-not
+
+The minimal threshold circuit. One neuron, one weight, one bias.
+
+## Circuit
+
+```
+      x
+      │
+      ▼
+  ┌───────┐
+  │ w: -1 │
+  │ b:  0 │
+  └───────┘
+      │
+      ▼
+   NOT(x)
+```
+
+## Mechanism
+
+A threshold neuron fires when its weighted input plus bias reaches zero. NOT uses weight -1 and bias 0:
+
+- Input 0: sum = 0, fires (output 1)
+- Input 1: sum = -1, silent (output 0)
+
+The negative weight flips the relationship between input magnitude and firing.
+
+## Parameters
+
+| | |
+|---|---|
+| Weight | -1 |
+| Bias | 0 |
+| Total | 2 parameters |
+
+## Properties
+
+- Involutive: NOT(NOT(x)) = x
+- Foundation for NAND, NOR
+
+## Usage
+
+```python
+from safetensors.torch import load_file
+
+w = load_file('model.safetensors')
+
+def not_gate(x):
+    return int(x * w['weight'].item() + w['bias'].item() >= 0)
+```
+
+## Files
+
+```
+threshold-not/
+├── model.safetensors
+├── model.py
+├── config.json
+└── README.md
+```
+
+## License
+
+MIT

config.json

@@ -0,0 +1,21 @@
+{
+  "model_type": "threshold_network",
+  "task": "not_gate",
+  "architecture": "1 -> 1",
+  "input_size": 1,
+  "output_size": 1,
+  "num_neurons": 1,
+  "num_parameters": 2,
+  "activation": "heaviside",
+  "weight_constraints": "integer",
+  "verification": {
+    "method": "coq_proof",
+    "exhaustive": true,
+    "inputs_tested": 2
+  },
+  "accuracy": {
+    "all_inputs": "2/2",
+    "percentage": 100.0
+  },
+  "github": "https://github.com/CharlesCNorton/coq-circuits"
+}

model.py

@@ -0,0 +1,58 @@
+"""
+Threshold Network for NOT Gate
+
+A formally verified single-neuron threshold network computing logical negation.
+Weights are integer-constrained and activation uses the Heaviside step function.
+"""
+
+import torch
+from safetensors.torch import load_file
+
+
+class ThresholdNOT:
+    """
+    NOT gate implemented as a threshold neuron.
+
+    Circuit: output = (weight * input + bias >= 0)
+    With weight=-1, bias=0: NOT(0)=1, NOT(1)=0
+    """
+
+    def __init__(self, weights_dict):
+        self.weight = weights_dict['weight']
+        self.bias = weights_dict['bias']
+
+    def __call__(self, x):
+        x = torch.as_tensor(x, dtype=torch.float32)
+        return (x * self.weight + self.bias >= 0).float()
+
+    @classmethod
+    def from_safetensors(cls, path="model.safetensors"):
+        return cls(load_file(path))
+
+
+def forward(x, weights):
+    """
+    Forward pass with Heaviside activation.
+
+    Args:
+        x: Input tensor (0 or 1)
+        weights: Dict with 'weight' and 'bias' tensors
+
+    Returns:
+        NOT(x)
+    """
+    x = torch.as_tensor(x, dtype=torch.float32)
+    return (x * weights['weight'] + weights['bias'] >= 0).float()
+
+
+if __name__ == "__main__":
+    weights = load_file("model.safetensors")
+    model = ThresholdNOT(weights)
+
+    print("NOT Gate Truth Table:")
+    print("-" * 20)
+    for inp in [0, 1]:
+        out = int(model(inp).item())
+        expected = 1 - inp
+        status = "OK" if out == expected else "FAIL"
+        print(f"NOT({inp}) = {out}  [{status}]")

model.safetensors

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