threshold-mux-mag7

Minimum-magnitude threshold circuit for 2:1 MUX. Magnitude 7 is proven optimal via exhaustive Coq computation.

Key Results

Magnitude	Valid MUX Circuits
0-6	0 (proven impossible)
7	4 (all included here)

The 4 Solutions

All solutions use weights from {-1, 0, 1} only.

Solution	Neuron 1	Neuron 2	Output
1	[0,1,-1] b=0	[-1,0,-1] b=0	[1,-1] b=-1
2	[0,-1,1] b=-1	[-1,0,-1] b=0	[-1,-1] b=0
3	[-1,0,-1] b=0	[0,1,-1] b=0	[-1,1] b=-1
4	[-1,0,-1] b=0	[0,-1,1] b=-1	[-1,-1] b=0

Solutions 1 & 3 are symmetric (swap N1 ↔ N2 and adjust output weights). Solutions 2 & 4 are similarly related.

Improvement Over Original

The original MUX circuit uses AND-NOT + AND + OR with magnitude 10:

Original (magnitude 10):
  N1 (a AND ¬s): w=[1, 0, -1], b=-1   → magnitude 3
  N2 (b AND s):  w=[0, 1, 1],  b=-2   → magnitude 4
  OR:            w=[1, 1],     b=-1   → magnitude 3

Optimized (magnitude 7, solution 1):
  N1:  w=[0, 1, -1], b=0    → magnitude 2
  N2:  w=[-1, 0, -1], b=0   → magnitude 2
  Out: w=[1, -1], b=-1      → magnitude 3

30% magnitude reduction (10 → 7).

Function

MUX(a, b, s) = a if s=0, b if s=1

Truth Table

a	b	s	out
0	0	0	0
0	0	1	0
0	1	0	0
0	1	1	1
1	0	0	1
1	0	1	0
1	1	0	1
1	1	1	1

Coq Proof

optimality_proof.v contains a machine-verified proof that:

1. No configuration with magnitude ≤ 6 computes MUX
2. At least one configuration with magnitude 7 computes MUX

Theorem mag_6 : any_mux (configs_at_mag 6) = false.
Proof. native_compute. reflexivity. Qed.

Theorem mag_7 : any_mux (configs_at_mag 7) = true.
Proof. native_compute. reflexivity. Qed.

Usage

from safetensors.torch import load_file
import torch

w = load_file('solution1.safetensors')

def mux(a, b, s):
    inp = torch.tensor([float(a), float(b), float(s)])
    hidden = (inp @ w['layer1.weight'].T + w['layer1.bias'] >= 0).float()
    out = (hidden @ w['layer2.weight'].T + w['layer2.bias'] >= 0).float()
    return int(out.item())

# Test
assert mux(1, 0, 0) == 1  # selects a
assert mux(1, 0, 1) == 0  # selects b
assert mux(0, 1, 0) == 0  # selects a
assert mux(0, 1, 1) == 1  # selects b

Files

threshold-mux-mag7/
├── solution1.safetensors   # First solution
├── solution2.safetensors   # Second solution
├── solution3.safetensors   # Third solution
├── solution4.safetensors   # Fourth solution
├── optimality_proof.v      # Coq proof of optimality
├── model.py                # Python implementation
├── config.json             # Metadata
└── README.md

Compile the Proof

coqc optimality_proof.v

License

MIT