Rename from tiny-BiImplies-verified

README.md

@@ -0,0 +1,107 @@
+---
+license: mit
+tags:
+- pytorch
+- safetensors
+- threshold-logic
+- neuromorphic
+- multi-layer
+---
+
+# threshold-biimplies
+
+The biconditional: x ↔ y ("if and only if"). Functionally identical to XNOR, but framed as the logical equivalence relation.
+
+## Circuit
+
+```
+      x       y
+      │       │
+      ├───┬───┤
+      │   │   │
+      ▼   │   ▼
+  ┌──────┐│┌──────┐
+  │ NOR  │││ AND  │   Layer 1
+  │w:-1,-1││w:1,1 │
+  │b: 0  │││b: -2 │
+  └──────┘│└──────┘
+      │   │   │
+      └───┼───┘
+          ▼
+      ┌──────┐
+      │  OR  │         Layer 2
+      │w: 1,1│
+      │b: -1 │
+      └──────┘
+          │
+          ▼
+       x ↔ y
+```
+
+## Mechanism
+
+The biconditional tests whether x and y have the same truth value:
+
+| x | y | NOR | AND | x ↔ y |
+|---|---|-----|-----|-------|
+| 0 | 0 | 1 | 0 | 1 |
+| 0 | 1 | 0 | 0 | 0 |
+| 1 | 0 | 0 | 0 | 0 |
+| 1 | 1 | 0 | 1 | 1 |
+
+NOR catches "both false," AND catches "both true," OR combines.
+
+## Why Two Layers?
+
+Unlike simple implication (x → y), the biconditional is not linearly separable. It requires detecting two diagonal cases - same problem as XOR.
+
+Implication x → y can be computed with weights [-1, +1] because it fails only at (1,0). Biimplication fails at both (0,1) and (1,0) - these points cannot be separated from (0,0) and (1,1) by a single hyperplane.
+
+## Parameters
+
+| Layer | Weights | Bias |
+|-------|---------|------|
+| NOR | [-1, -1] | 0 |
+| AND | [1, 1] | -2 |
+| OR | [1, 1] | -1 |
+| **Total** | | **9** |
+
+## Properties
+
+- Reflexive: x ↔ x = 1
+- Symmetric: (x ↔ y) = (y ↔ x)
+- Transitive: (x ↔ y) ∧ (y ↔ z) → (x ↔ z)
+
+Full equivalence relation.
+
+## Usage
+
+```python
+from safetensors.torch import load_file
+import torch
+
+w = load_file('model.safetensors')
+
+def biimplies_gate(x, y):
+    inp = torch.tensor([float(x), float(y)])
+
+    nor_out = int((inp * w['layer1.neuron1.weight']).sum() + w['layer1.neuron1.bias'] >= 0)
+    and_out = int((inp * w['layer1.neuron2.weight']).sum() + w['layer1.neuron2.bias'] >= 0)
+
+    l1 = torch.tensor([float(nor_out), float(and_out)])
+    return int((l1 * w['layer2.weight']).sum() + w['layer2.bias'] >= 0)
+```
+
+## Files
+
+```
+threshold-biimplies/
+├── model.safetensors
+├── model.py
+├── config.json
+└── README.md
+```
+
+## License
+
+MIT

config.json

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

model.py

@@ -0,0 +1,80 @@
+"""
+Threshold Network for Biconditional Gate
+
+A formally verified two-layer threshold network computing logical equivalence (iff).
+Biconditional is not linearly separable, requiring at least 2 layers.
+Architecture: Layer1 computes NOR and AND, Layer2 computes OR of results.
+"""
+
+import torch
+from safetensors.torch import load_file
+
+
+class ThresholdBiImplies:
+    """
+    Biconditional gate implemented as a 2-layer threshold network.
+
+    Layer 1: NOR (neuron 1) and AND (neuron 2) in parallel
+    Layer 2: OR of layer 1 outputs
+
+    BiImplies(x,y) = OR(NOR(x,y), AND(x,y)) = (x iff y)
+    """
+
+    def __init__(self, weights_dict):
+        self.l1_n1_weight = weights_dict['layer1.neuron1.weight']
+        self.l1_n1_bias = weights_dict['layer1.neuron1.bias']
+        self.l1_n2_weight = weights_dict['layer1.neuron2.weight']
+        self.l1_n2_bias = weights_dict['layer1.neuron2.bias']
+        self.l2_weight = weights_dict['layer2.weight']
+        self.l2_bias = weights_dict['layer2.bias']
+
+    def __call__(self, x1, x2):
+        inputs = torch.tensor([float(x1), float(x2)])
+
+        nor_out = ((inputs * self.l1_n1_weight).sum() + self.l1_n1_bias >= 0).float()
+        and_out = ((inputs * self.l1_n2_weight).sum() + self.l1_n2_bias >= 0).float()
+
+        layer1_out = torch.tensor([nor_out, and_out])
+        output = ((layer1_out * self.l2_weight).sum() + self.l2_bias >= 0).float()
+
+        return output
+
+    @classmethod
+    def from_safetensors(cls, path="model.safetensors"):
+        return cls(load_file(path))
+
+
+def forward(x1, x2, weights):
+    """
+    Forward pass with Heaviside activation.
+
+    Args:
+        x1, x2: Input values (0 or 1)
+        weights: Dict with layer weights and biases
+
+    Returns:
+        BiImplies(x1, x2) = (x1 iff x2)
+    """
+    inputs = torch.tensor([float(x1), float(x2)])
+
+    nor_out = ((inputs * weights['layer1.neuron1.weight']).sum() + weights['layer1.neuron1.bias'] >= 0).float()
+    and_out = ((inputs * weights['layer1.neuron2.weight']).sum() + weights['layer1.neuron2.bias'] >= 0).float()
+
+    layer1_out = torch.tensor([nor_out, and_out])
+    output = ((layer1_out * weights['layer2.weight']).sum() + weights['layer2.bias'] >= 0).float()
+
+    return output
+
+
+if __name__ == "__main__":
+    weights = load_file("model.safetensors")
+    model = ThresholdBiImplies(weights)
+
+    print("Biconditional Gate Truth Table:")
+    print("-" * 30)
+    for x1 in [0, 1]:
+        for x2 in [0, 1]:
+            out = int(model(x1, x2).item())
+            expected = 1 if x1 == x2 else 0
+            status = "OK" if out == expected else "FAIL"
+            print(f"BiImplies({x1}, {x2}) = {out}  [{status}]")

model.safetensors

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