Changing one truth-table entry

An existing shared De Morgan circuit can be modified at one input assignment using at most 2 * n additional internal gates. A nonempty minterm, or its dual clause, uses at most n negations and n - 1 binary gates; one final OR or AND sets the requested value. The original circuit is used once.

The zero-input case is included: either Boolean constant has a one-gate implementation, and every zero-input, one-output circuit already has a gate. All internal gates, including constants and identities, are counted.

theorem Algebraic.DeMorgan.exists_update_circuit {n : ℕ} (circuit : Circuit signature n 1) (function : ScalarFunction Bool n) (computes : circuit.ComputesWith interpretation fun (input : Fin n → Bool) (x : Fin 1) => function input) (point : Fin n → Bool) (value : Bool) : ∃ (result : Circuit signature n 1), (result.ComputesWith interpretation fun (input : Fin n → Bool) (x : Fin 1) => Function.update function point value input) ∧ result.size ≤ circuit.size + 2 * n

Modify one truth-table entry without duplicating the original circuit. The bound counts every internal gate in the De Morgan signature.