---
license: mit
tags:
- pytorch
- safetensors
- formal-verification
- coq
- mod7
- modular-arithmetic
- threshold-network
- neuromorphic
---

# tiny-mod7-prover

Formally verified neural network that computes the MOD-7 function (Hamming weight mod 7) on 8-bit inputs. For Coq source code, see [mod7-verified](https://github.com/CharlesCNorton/mod7-verified).

## Overview

Threshold network computing `mod7(x) = HW(x) mod 7` for 8-bit binary inputs. Outputs 0-6 corresponding to the seven residue classes.

**Key properties:**
- 100% accuracy on all 256 possible inputs
- Correctness proven in Coq (axiom-free)
- Integer weights, Heaviside activation
- Part of the verified MOD-m family

## Architecture

| Layer | Neurons | Function |
|-------|---------|----------|
| Input | 8 | Binary input bits |
| Hidden 1 | 9 | Thermometer encoding |
| Hidden 2 | 6 | MOD-7 detection |
| Output | 7 | Classification |

**Total: 22 neurons, 190 parameters**

## Algebraic Insight

For MOD-m, use weights `(1, 1, ..., 1, 1-m)` with `m-1` ones before the reset.

MOD-7 uses `(1, 1, 1, 1, 1, 1, -6)`:
```
HW=0: cumsum=0, HW=1: cumsum=1, ..., HW=6: cumsum=6
HW=7: cumsum=0 (reset: 1+1+1+1+1+1-6=0)
HW=8: cumsum=1
```

## Formal Verification

```coq
Theorem network_correct_exhaustive : verify_all = true.
Theorem network_correct_constructive : forall x0 x1 x2 x3 x4 x5 x6 x7,
  predict [x0; x1; x2; x3; x4; x5; x6; x7] = mod7 [x0; x1; x2; x3; x4; x5; x6; x7].
Theorem cumsum_eq_mod7 : forall k,
  (k <= 8)%nat -> cumsum k = Z.of_nat (Nat.modulo k 7).
```

All proofs axiom-free.

## The MOD-m Family

| Model | Function | Neurons | Params | Weight Pattern |
|-------|----------|---------|--------|----------------|
| tiny-parity-prover | MOD-2 | 14 | 139 | (1, -1) |
| tiny-mod3-prover | MOD-3 | 14 | 110 | (1, 1, -2) |
| tiny-mod5-prover | MOD-5 | 18 | 146 | (1, 1, 1, 1, -4) |
| **tiny-mod7-prover** | MOD-7 | 22 | 190 | (1, 1, 1, 1, 1, 1, -6) |

## Related

- [mod7-verified](https://github.com/CharlesCNorton/mod7-verified) — Coq proofs
- [tiny-mod5-prover](https://huggingface.co/phanerozoic/tiny-mod5-prover)
- [tiny-mod3-prover](https://huggingface.co/phanerozoic/tiny-mod3-prover)
- [tiny-parity-prover](https://huggingface.co/phanerozoic/tiny-parity-prover)

## License

MIT