Shannon and Lupanov bounds for De Morgan complexity

CSLib's sharp Boolean bounds transfer through the realizations in DeMorgan.CSLib. Identity elimination preserves the Shannon lower bound on total internal gates; importing Lupanov circuits preserves their total size. For standardCost, which makes constants free, the lower bound has an additive two-gate allowance supplied by withSharedConstants.

The local explicit mass-production constructions retain their finite cost ledgers. The results here use CSLib's asymptotic existence theorems.

theorem Algebraic.DeMorgan.exists_complexity_gt_two_pow_div : ∃ (N : ℕ), ∀ n ≥ N, ∃ (function : ScalarFunction Bool n), 2 ^ n / ↑n < ↑(complexity function)

For all sufficiently large input widths, some Boolean function requires strictly more than 2^n / n internal gates, including constants and identities.

theorem Algebraic.DeMorgan.eventually_complexity_le_lupanov (ε : ℝ) (positive : 0 < ε) : ∃ (N : ℕ), ∀ n ≥ N, ∀ (function : ScalarFunction Bool n), ↑(complexity function) ≤ (1 + ε) * 2 ^ n / ↑n

Lupanov's leading coefficient one bounds the minimum total gate count uniformly over all Boolean functions of a sufficiently large input width.

theorem Algebraic.DeMorgan.exists_standardCost_add_two_gt_two_pow_div : ∃ (N : ℕ), ∀ n ≥ N, ∃ (function : ScalarFunction Bool n), ∀ (circuit : Circuit signature n 1), (circuit.ComputesWith interpretation fun (input : Fin n → Bool) (x : Fin 1) => function input) → 2 ^ n / ↑n < ↑(circuit.cost standardCost) + 2

Free constants change the Shannon lower bound by at most two gates.

theorem Algebraic.DeMorgan.exists_standardCost_le_lupanov (ε : ℝ) (positive : 0 < ε) : ∃ (N : ℕ), ∀ n ≥ N, ∀ (function : ScalarFunction Bool n), ∃ (circuit : Circuit signature n 1), (circuit.ComputesWith interpretation fun (input : Fin n → Bool) (x : Fin 1) => function input) ∧ ↑(circuit.cost standardCost) ≤ (1 + ε) * 2 ^ n / ↑n

The standard weighted cost also satisfies Lupanov's sharp upper bound.