Shared pattern tables

A Boolean matrix is synthesized by sharing its column patterns across rows. The leading cost is one OR per selected pattern; input tests and the pattern bank are built only once. This is the elementary table construction used in the sparse and partial-function specializations of local coding.

def Complexity.CircuitSparseSynthesis.Internal.assignmentIndex (width : ℕ) : (Fin width → Bool) ≃ Fin (2 ^ width)

Binary numbering of all assignments to width input bits.

Equations

• Complexity.CircuitSparseSynthesis.Internal.assignmentIndex width = ((Equiv.refl (Fin width)).arrowCongr finTwoEquiv.symm).trans finFunctionFinEquiv

def Complexity.CircuitSparseSynthesis.Internal.columnAt {k l : ℕ} (x : Fin (k + l) → Bool) : Fin (2 ^ k)

Column index selected by the first k input bits.

Equations

• Complexity.CircuitSparseSynthesis.Internal.columnAt x = (Complexity.CircuitSparseSynthesis.Internal.assignmentIndex k) fun (i : Fin k) => x (Fin.castAdd l i)

def Complexity.CircuitSparseSynthesis.Internal.rowAt {k l : ℕ} (x : Fin (k + l) → Bool) : Fin (2 ^ l)

Row index selected by the remaining l input bits.

Equations

• Complexity.CircuitSparseSynthesis.Internal.rowAt x = (Complexity.CircuitSparseSynthesis.Internal.assignmentIndex l) fun (i : Fin l) => x (Fin.natAdd k i)

def Complexity.CircuitSparseSynthesis.Internal.matrixInput {k l : ℕ} (row : Fin (2 ^ l)) (column : Fin (2 ^ k)) : Fin (k + l) → Bool

Reconstruct an input from its row and column indices.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Complexity.CircuitSparseSynthesis.Internal.columnAt_matrixInput {k l : ℕ} (r : Fin (2 ^ l)) (c : Fin (2 ^ k)) : columnAt (matrixInput r c) = c

@[simp]

theorem Complexity.CircuitSparseSynthesis.Internal.rowAt_matrixInput {k l : ℕ} (r : Fin (2 ^ l)) (c : Fin (2 ^ k)) : rowAt (matrixInput r c) = r

@[simp]

theorem Complexity.CircuitSparseSynthesis.Internal.matrixInput_rowAt_columnAt {k l : ℕ} (x : Fin (k + l) → Bool) : matrixInput (rowAt x) (columnAt x) = x

def Complexity.CircuitSparseSynthesis.Internal.matrixEquiv (k l : ℕ) : (Fin (k + l) → Bool) ≃ Fin (2 ^ l) × Fin (2 ^ k)

The truth-table indexing equivalence used to sum support sizes over rows.

Equations

• One or more equations did not get rendered due to their size.

def Complexity.CircuitSparseSynthesis.Internal.rowDomain {k l : ℕ} (domain : Finset (Fin (k + l) → Bool)) (r : Fin (2 ^ l)) : Finset (Fin (2 ^ k))

Columns of one row whose corresponding inputs belong to the domain.

Equations

• Complexity.CircuitSparseSynthesis.Internal.rowDomain domain r = {c : Fin (2 ^ k) | Complexity.CircuitSparseSynthesis.Internal.matrixInput r c ∈ domain}

theorem Complexity.CircuitSparseSynthesis.Internal.sum_rowDomain_card {k l : ℕ} (domain : Finset (Fin (k + l) → Bool)) : ∑ r : Fin (2 ^ l), (rowDomain domain r).card = domain.card

def Complexity.CircuitSparseSynthesis.Internal.matrixMinterm {k l : ℕ} : Fin (2 ^ k) ⊕ Fin (2 ^ l) → Cslib.BooleanFunction (k + l)

Shared equality tests for every column and row index.

Equations

• Complexity.CircuitSparseSynthesis.Internal.matrixMinterm (Sum.inl c) = fun (x : Cslib.BitString (k + l)) => decide (Complexity.CircuitSparseSynthesis.Internal.columnAt x = c)
• Complexity.CircuitSparseSynthesis.Internal.matrixMinterm (Sum.inr r) = fun (x : Cslib.BitString (k + l)) => decide (Complexity.CircuitSparseSynthesis.Internal.rowAt x = r)

theorem Complexity.CircuitSparseSynthesis.Internal.matrixMinterms_synthesis (k l : ℕ) : Cslib.Circuits.Synthesis Cslib.Circuits.Boolean.interpretation (Cslib.Circuits.inputs (k + l)) (Set.range matrixMinterm) ((2 ^ k + 2 ^ l) * (2 * (k + l) + 1))

theorem Complexity.CircuitSparseSynthesis.Internal.pattern_synthesis {k l : ℕ} (pattern : Fin (2 ^ k) → Bool) : Cslib.Circuits.Synthesis Cslib.Circuits.Boolean.interpretation (Set.range matrixMinterm) {fun (x : Fin (k + l) → Bool) => pattern (columnAt x)} ({c : Fin (2 ^ k) | pattern c = true}.card + 1)

theorem Complexity.CircuitSparseSynthesis.Internal.matrix_synthesis {k l : ℕ} {B : Type} [Fintype B] (patterns : B → Fin (2 ^ k) → Bool) (patternSize : ℕ) (small : ∀ (b : B), {c : Fin (2 ^ k) | patterns b c = true}.card ≤ patternSize) (count : Fin (2 ^ l) → ℕ) (chosen : (row : Fin (2 ^ l)) → Fin (count row) → B) : Cslib.Circuits.Synthesis Cslib.Circuits.Boolean.interpretation (Cslib.Circuits.inputs (k + l)) {fun (x : Fin (k + l) → Bool) => decide (∃ (j : Fin (count (rowAt x))), patterns (chosen (rowAt x) j) (columnAt x) = true)} ((2 ^ k + 2 ^ l) * (2 * (k + l) + 1) + Fintype.card B * (patternSize + 1) + ∑ row : Fin (2 ^ l), count row + 3 * 2 ^ l + 1)