Minimum-magnitude threshold circuit for 2:1 MUX. Magnitude 7 is proven optimal via exhaustive Coq computation.
All solutions use weights from {-1, 0, 1} only.
Solutions 1 & 3 are symmetric (swap N1 ↔ N2 and adjust output weights).
Solutions 2 & 4 are similarly related.
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).
1Theorem mag_6 : any_mux (configs_at_mag 6) = false.
2Proof. native_compute. reflexivity. Qed.
3
4Theorem mag_7 : any_mux (configs_at_mag 7) = true.
5Proof. native_compute. reflexivity. Qed.
1from safetensors.torch import load_file
2import torch
3
4w = load_file('solution1.safetensors')
5
6def mux(a, b, s):
7 inp = torch.tensor([float(a), float(b), float(s)])
8 hidden = (inp @ w['layer1.weight'].T + w['layer1.bias'] >= 0).float()
9 out = (hidden @ w['layer2.weight'].T + w['layer2.bias'] >= 0).float()
10 return int(out.item())
11
12# Test
13assert mux(1, 0, 0) == 1 # selects a
14assert mux(1, 0, 1) == 0 # selects b
15assert mux(0, 1, 0) == 0 # selects a
16assert mux(0, 1, 1) == 1 # selects b
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
