A 13-gate NAND-only circuit computes a 1-bit full adder, checked by exhaustive replay of all 8 input rows

Identifier: F:cas-boolean-circuit-nand-only-full-adder
Proof route: cas-certificate
External status: proved
Axiom footprint: cas.boolean-circuit-exhaustive-replay-is-self-contained: check_boolean_circuit re-simulates every gate for all 2^n input rows directly from the gate list, gate semantics (BooleanGateOp::apply) and the artifact's own declared truth table -- there is no producer-only claim that is not replayed. On a mismatch BooleanCircuitCheck::Failed names the exact input row and both the expected and observed output values, which nand_only_full_adder_truth_table_mutation_is_rejected exercises directly (row 3, expected 3, observed 1). This is a cleaner instance than most cas-internal facts in this crate: there is no residue left unchecked, because the whole claim IS the truth table and the whole truth table is replayed., cas.rust-boolean-arithmetic-not-kernel-terms: the gate-by-gate simulation runs in axeyum-cas's own Rust evaluator (BooleanGateOp::apply over bool), not through crate::Kernel::add_declaration. Nothing here has been type-checked by the trusted kernel., cas.no-kernel-boolean-circuit-bridge-exists: crate::Kernel has rat_prelude/decidable.rs and rat_prelude/boolean.rs, which the 2026-09-01 CAS certificate audit (docs/research/11-design-review/2026-09-01-cas-certificate-reconstruction-audit.md) names as the missing-piece target for a bridge test importing axeyum_cas::boolean_circuit -- and names this module as the cheapest COULD RECONSTRUCT case in the crate. No such bridge was attempted for this fact; the audit's sizing was read from the two crates, not tried, and this fact does not change that.

Recorded description

There is a Boolean circuit built entirely from 13 NAND gates -- three inputs a, b, cin and two outputs sum, cout -- that computes sum = a XOR b XOR cin and cout = (a AND b) OR (cin AND (a XOR b)) for every one of the 2^3 = 8 input rows. The evidence is not a claim that NAND is universal in general; it is a specific, named 13-gate circuit whose truth table is re-simulated gate by gate for all 8 rows and compared row by row against the arithmetic definition of one-bit addition, via axeyum_cas::boolean_circuit::check_boolean_circuit. The circuit is built from the standard 4-NAND XOR gadget applied twice (to (a,b) then to (a XOR b, cin)) for the sum, and from NAND-realized AND/OR gates combined by De Morgan's law for the carry. Cas-internal under ADR-0601 SS2: this kernel has rat_prelude/decidable.rs and rat_prelude/boolean.rs, but no bridge test imports axeyum_cas::boolean_circuit, so no kernel re-check exists.

Formal statement

(boolean-circuit-artifact
  (inputs a b cin)
  (gates
    (n1 nand a b) (n2 nand a n1) (n3 nand b n1) (xor_ab nand n2 n3)
    (n5 nand xor_ab cin) (n6 nand xor_ab n5) (n7 nand cin n5) (sum nand n6 n7)
    (ab nand n1 n1) (cin_xor nand n5 n5) (na nand ab ab) (nb nand cin_xor cin_xor)
    (cout nand na nb))
  (outputs sum cout)
  (assert (forall (a b cin) (= sum (xor a (xor b cin)))))
  (assert (forall (a b cin) (= cout (or (and a b) (and cin (xor a b)))))))

Dependencies

The graph shows direct ledger edges. Follow a node to open its artifact page.

0 direct dependencies 0 direct dependents

Evidence

cas-boolean-circuit-nand-full-adder-replay

Kind: witness-replay
Status: checked

Supports: the named 13-gate NAND-only circuit's truth table matches one-bit binary addition (sum, carry-out) for all 8 input rows

Checker command

cargo test -p axeyum-cas --lib boolean_circuit::tests::nand_only_full_adder_matches_arithmetic_for_every_row -- --exact 2>/dev/null | grep -cE '^test boolean_circuit::tests::nand_only_full_adder_matches_arithmetic_for_every_row \.\.\. ok$'

Evidence notes

Verified on this host both directions: the real test path gives count=1, exit 0; a deliberately absent test path (this repository's own tested trap -- a bare `cargo test` with a nonmatching filter prints `0 filtered out` and exits 0) gives count=0, exit 1 through this grep -cE shape. gate_counts in the Verified variant is pinned to {Nand: 13} in the test, so the assertion also fixes the gate count and the single gate kind used, not merely that 8 rows passed.

Provenance

{
  "date": "2026-09-01",
  "established_by": "cas-facts-circuit-tensor lane, landing the two 'one fact away' modules named by docs/research/11-design-review/2026-09-01-cas-certificate-reconstruction-audit.md's 'What did not get done' section (boolean_circuit and gf2_tensor, both replaying exhaustively and both naming a counterexample). The checker (check_boolean_circuit) pre-existed; the specific 13-gate NAND circuit, its test, and this ledger row are new to this lane, verified correct by an independent Python simulation of the same gate list before being committed as Rust.",
  "source": "NAND's functional completeness for combinational logic is classical (any Boolean function is expressible using only NAND gates, since NOT, AND and OR each reduce to NAND); the specific 13-gate full-adder realization composes the standard 4-NAND XOR gadget with a De Morgan NAND-OR.",
  "prior_art": [
    {
      "who": "folklore / standard digital logic",
      "what": "NAND (and dually NOR) is a universal gate; the 4-NAND XOR gadget and the full adder built from two XOR stages plus a carry network are textbook constructions",
      "year": null,
      "where": "standard digital logic design texts",
      "attribution": "no single primary source consulted; this is common knowledge in digital circuit design, and the specific 13-gate wiring and its correctness for all 8 rows were verified independently for this fact rather than copied from a citation"
    }
  ]
}