Tight binary-gate budgets force read-once semantics #
This argument retains arbitrary sharing and free designated output wires. Unfolding a selected wire increases the number of formula input occurrences by at most the binary cost of that gate. Essential-input counting forces every intermediate formula to remain read-once at the tight budget.
theorem
Algebraic.DeMorgan.exists_readOnce_of_binaryCost_le
{n : ℕ}
(circuit : Circuit signature n 1)
{function : ScalarFunction Bool n}
(computes : circuit.ComputesWith interpretation fun (input : Fin n → Bool) (x : Fin 1) => function input)
(essential : ∀ (i : Fin n), EssentialAt function i)
(tight : circuit.cost binaryCost + 1 ≤ n)
:
∃ (expression : Expression n),
expression.ReadOnce ∧ (fun (input : Fin n → Bool) => Expression.eval input expression) = function
A shared circuit using the minimum possible number of binary gates has read-once semantics.
theorem
Algebraic.DeMorgan.unate_of_binaryCost_le
{n : ℕ}
(circuit : Circuit signature n 1)
{function : ScalarFunction Bool n}
(computes : circuit.ComputesWith interpretation fun (input : Fin n → Bool) (x : Fin 1) => function input)
(essential : ∀ (i : Fin n), EssentialAt function i)
(tight : circuit.cost binaryCost + 1 ≤ n)
:
Unate function
Unateness is forced at the tight binary-gate budget, even with arbitrary circuit sharing.
theorem
Algebraic.DeMorgan.size_ge_of_essential_nonunate
{n : ℕ}
(circuit : Circuit signature n 1)
{function : ScalarFunction Bool n}
(computes : circuit.ComputesWith interpretation fun (input : Fin n → Bool) (x : Fin 1) => function input)
(essential : ∀ (i : Fin n), EssentialAt function i)
(nonunate : ¬Unate function)
:
An essential non-unate function needs at least n+1 native gates in an arbitrary shared circuit.
theorem
Algebraic.DeMorgan.complexity_ge_of_essential_nonunate
{n : ℕ}
(function : ScalarFunction Bool n)
(essential : ∀ (i : Fin n), EssentialAt function i)
(nonunate : ¬Unate function)
:
Minimum native circuit size inherits the essential non-unate lower bound.