Rename from tiny-Implies-verified

README.md

@@ -0,0 +1,90 @@
+---
+license: mit
+tags:
+- pytorch
+- safetensors
+- threshold-logic
+- neuromorphic
+---
+
+# threshold-implies
+
+Material implication: x → y. The only two-input Boolean function with asymmetric weights.
+
+## Circuit
+
+```
+    x   y
+    │   │
+    └─┬─┘
+      ▼
+  ┌───────┐
+  │w: -1,1│
+  │ b:  0 │
+  └───────┘
+      │
+      ▼
+    x → y
+```
+
+## Mechanism
+
+The antecedent x has weight -1 (inhibitory), the consequent y has weight +1 (excitatory):
+
+| x | y | sum | output | meaning |
+|---|---|-----|--------|---------|
+| 0 | 0 | 0 | 1 | false → false |
+| 0 | 1 | +1 | 1 | false → true |
+| 1 | 0 | -1 | 0 | true → false ✗ |
+| 1 | 1 | 0 | 1 | true → true |
+
+The only failure: asserting a true antecedent with a false consequent. This is the only thing implication forbids.
+
+## Equivalent Forms
+
+- x → y = ¬x ∨ y
+- x → y = ¬(x ∧ ¬y)
+
+The weights [-1, +1] directly implement ¬x + y.
+
+## Parameters
+
+| | |
+|---|---|
+| Weights | [-1, +1] |
+| Bias | 0 |
+| Total | 3 parameters |
+
+## Properties
+
+- Linearly separable (unlike XOR)
+- Not commutative: (x → y) ≠ (y → x)
+- Reflexive: x → x = 1
+- Ex falso quodlibet: 0 → y = 1
+
+## Usage
+
+```python
+from safetensors.torch import load_file
+import torch
+
+w = load_file('model.safetensors')
+
+def implies_gate(x, y):
+    inputs = torch.tensor([float(x), float(y)])
+    return int((inputs * w['weight']).sum() + w['bias'] >= 0)
+```
+
+## Files
+
+```
+threshold-implies/
+├── model.safetensors
+├── model.py
+├── config.json
+└── README.md
+```
+
+## License
+
+MIT

config.json

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

model.py

@@ -0,0 +1,61 @@
+"""
+Threshold Network for Implication Gate
+
+A formally verified single-neuron threshold network computing material conditional.
+Weights are integer-constrained and activation uses the Heaviside step function.
+"""
+
+import torch
+from safetensors.torch import load_file
+
+
+class ThresholdImplies:
+    """
+    Implication gate implemented as a threshold neuron.
+
+    Circuit: output = (w1*x + w2*y + bias >= 0)
+    With weights=[-1,1], bias=0: fails only when x=1 and y=0.
+    """
+
+    def __init__(self, weights_dict):
+        self.weight = weights_dict['weight']
+        self.bias = weights_dict['bias']
+
+    def __call__(self, x, y):
+        inputs = torch.tensor([float(x), float(y)])
+        weighted_sum = (inputs * self.weight).sum() + self.bias
+        return (weighted_sum >= 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 of shape [..., 2]
+        weights: Dict with 'weight' and 'bias' tensors
+
+    Returns:
+        Implies(x[0], x[1])
+    """
+    x = torch.as_tensor(x, dtype=torch.float32)
+    weighted_sum = (x * weights['weight']).sum(dim=-1) + weights['bias']
+    return (weighted_sum >= 0).float()
+
+
+if __name__ == "__main__":
+    weights = load_file("model.safetensors")
+    model = ThresholdImplies(weights)
+
+    print("Implication Gate Truth Table:")
+    print("-" * 30)
+    for x in [0, 1]:
+        for y in [0, 1]:
+            out = int(model(x, y).item())
+            expected = 1 if (x == 0 or y == 1) else 0
+            status = "OK" if out == expected else "FAIL"
+            print(f"Implies({x}, {y}) = {out}  [{status}]")

model.safetensors

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