Upload README.md with huggingface_hub

README.md

@@ -39,6 +39,44 @@ A complete 8-bit processor where every operation—from Boolean logic to arithme
 
 ---
 
+## Background
+
+### Threshold Logic
+
+A threshold gate computes a Boolean function by taking a weighted sum of binary inputs and comparing it to a threshold. If the sum meets or exceeds the threshold, the output is 1; otherwise, 0. This can be expressed as a neuron with Heaviside step activation: `output = 1 if (Σ wᵢxᵢ + b) ≥ 0 else 0`, where weights `wᵢ` and bias `b` are integers.
+
+Threshold gates are strictly more powerful than standard Boolean gates. A single threshold gate can compute any linearly separable Boolean function—this includes AND, OR, NAND, NOR, and many others that require multiple levels of conventional gates. Functions that are not linearly separable (such as XOR or parity) require multiple threshold gates arranged in layers.
+
+### Historical Development
+
+Warren McCulloch and Walter Pitts introduced the threshold neuron model in 1943, proving that networks of such neurons could compute any Boolean function. This work preceded both the perceptron and modern neural networks, establishing the theoretical foundation for neural computation.
+
+The 1960s saw significant development in threshold logic synthesis. Researchers including Saburo Muroga, Robert McNaughton, and Michael Dertouzos developed algebraic methods for determining whether a Boolean function could be implemented as a single threshold gate, and if so, how to calculate appropriate weights. This work produced systematic techniques for threshold gate design but focused on individual gates rather than complete systems.
+
+Frank Rosenblatt's Mark I Perceptron (1957-1960) implemented threshold neurons in hardware using potentiometers for weights, but it was a pattern classifier that learned its weights through training—the final weight configurations were not published. Bernard Widrow's ADALINE and MADALINE systems (1960-1963) similarly used adaptive threshold elements with weights learned via the LMS algorithm.
+
+Hava Siegelmann and Eduardo Sontag proved in the 1990s that recurrent neural networks are Turing complete. Their construction, however, relied on continuous sigmoid activation functions with infinite precision—not the discrete step function used in threshold logic. Other theoretical work on neural Turing machines and differentiable computers followed similar patterns: proving computational universality using continuous, differentiable activations suitable for gradient-based training.
+
+### Neuromorphic Hardware
+
+Modern neuromorphic processors implement large arrays of configurable threshold-like neurons in silicon:
+
+**Intel Loihi** (2017) provides 128 neuromorphic cores with programmable synaptic weights, spike-based communication, and on-chip learning. The architecture supports integer weights and configurable neuron dynamics.
+
+**IBM TrueNorth** (2014) integrates one million neurons and 256 million synapses in a 4096-core array. Each neurosynaptic core implements 256 neurons with configurable weights and thresholds. The chip was designed as an alternative to von Neumann architecture rather than an implementation of one.
+
+**BrainChip Akida** (2021) targets edge deployment with event-based processing and integer weights. The architecture supports standard neural network operations mapped onto neuromorphic primitives.
+
+**SpiNNaker** (University of Manchester) uses ARM processor cores to simulate spiking neural networks at scale. The platform has hosted various neural models but is simulation-based rather than native neuromorphic silicon.
+
+Despite the availability of these platforms, published work has focused on neural network inference, sensory processing, and pattern recognition. A 2024 paper demonstrated basic logic gates, adders, and decoders on SpiNNaker and Dynap-SE1, describing this as "a first step toward the construction of a spiking computer"—the implementation lacked instruction fetch, program counter, memory systems, and control logic.
+
+### This Implementation
+
+The weights in this repository implement a complete 8-bit computer: registers, ALU with 16 operations, status flags, conditional branching, subroutine calls, stack operations, and memory access. Every component is built from threshold neurons with integer weights. The weight configurations are published in safetensors format for direct loading and deployment.
+
+---
+
 ## Circuit Categories
 
 | Category | Circuits | Examples |
@@ -84,27 +122,27 @@ The model includes `iron_eval.py` which exhaustively tests all circuits:
 
 ```bash
 python iron_eval.py
-# Output: Fitness: 1.000000 (4478 tests)
+# Output: Fitness: 1.000000
 ```
 
 ### Verification Status
 
 | Category | Status | Notes |
 |----------|--------|-------|
-| Boolean gates | Coq-derived | Original formal proofs |
-| Arithmetic | Coq-derived | Adders, comparators |
-| ALU | Coq-derived | All 16 operations |
-| Control flow | Coq-derived | Jumps, stack ops |
-| Threshold | Coq-derived | k-of-n gates |
-| **Modular (mod 3,5,6,7,9,10,11,12)** | **Hand-verified** | Multi-layer circuits added manually |
-| **Parity** | **Hand-verified** | XOR tree structure added manually |
-| Modular (mod 2,4,8) | Exact | Single-layer, trivial |
+| Boolean gates | Exhaustively tested | Coq proofs available |
+| Arithmetic | Exhaustively tested | Coq proofs available |
+| ALU | Exhaustively tested | Coq proofs available |
+| Control flow | Exhaustively tested | Coq proofs available |
+| Threshold | Exhaustively tested | Coq proofs available |
+| Modular (mod 3,5,6,7,9,10,11,12) | Exhaustively tested | Multi-layer, hand-constructed |
+| Parity | Exhaustively tested | XOR tree, hand-constructed |
+| Modular (mod 2,4,8) | Exhaustively tested | Single-layer, trivial |
 
 The modular arithmetic circuits for non-powers-of-2 and the parity circuits were hand-constructed because:
 - Divisibility by 3, 5, etc. is **not linearly separable** in binary
 - 8-bit parity (XOR of all bits) requires a tree of XOR gates
 
-These circuits pass exhaustive testing but lack formal proofs.
+All circuits pass exhaustive testing over their full input domains.
 
 ---
 
@@ -137,8 +175,9 @@ All weights are integers. All activations are Heaviside step. Designed for:
 
 | File | Description |
 |------|-------------|
-| `neural_computer.safetensors` | All 1,482 circuit tensors (~152 KB) |
-| `iron_eval.py` | Comprehensive test suite (4,416 tests) |
+| `neural_computer.safetensors` | 3,122 tensors, 5,648 parameters |
+| `iron_eval.py` | Comprehensive test suite |
+| `prune_weights.py` | Weight optimization tool |
 
 ---
 
@@ -164,5 +203,5 @@ MIT
 
 ## Links
 
-- [Coq Proofs](https://github.com/CharlesCNorton/coq-circuits) — Original formal verification
+- [Coq Proofs](https://github.com/CharlesCNorton/coq-circuits) — Formal verification for core circuits
 - [HuggingFace](https://huggingface.co/phanerozoic) — Other models