Partial truth-table synthesis

Intervals containing few specified positions use a shared bank of total extensions. Every extension is masked to its interval before the row is assembled, so unconstrained values cannot affect another interval's data.

def Complexity.CircuitSparseSynthesis.Internal.partialTableBudget (k l K weight : ℕ) : ℕ

Shared minterms, interval-masked extension bank, and one OR per partial chunk.

Equations

• Complexity.CircuitSparseSynthesis.Internal.partialTableBudget k l K weight = (2 ^ k + 2 ^ l) * (2 * (k + l) + 1) + (2 ^ k + 1) ^ 3 * (4 * 2 ^ k + 1) * 2 ^ K + weight / K + 4 * 2 ^ l + 1

theorem Complexity.CircuitSparseSynthesis.Internal.exists_partialTable {k l : ℕ} (domain : Finset (Fin (k + l) → Bool)) (f : Cslib.BooleanFunction (k + l)) (K : ℕ) (positive : 0 < K) : ∃ (c : Cslib.Circuits.Circuit Cslib.Circuits.Boolean.signature (k + l) 1), (c.ComputesOn Cslib.Circuits.Boolean.interpretation ↑domain fun (x : Fin (k + l) → Bool) (x_1 : Fin 1) => f x) ∧ c.size ≤ partialTableBudget k l K domain.card