Finite Shannon synthesis

Choosing ⌊log₂ n⌋ - 1 address bits in the shared-column construction yields a circuit with at most 27 * 2 ^ n / n gates for every Boolean function on n ≥ 16 inputs. The natural-number division is applied after multiplying by 27. All gates, including constants and negations, are counted.

The synthesizer is a computable function of a supplied truth table. This module bounds the resulting circuit's size; it does not certify the synthesizer's running time.

Main definitions

• Cslib.Circuits.Boolean.ShannonSynthesis.synthesize: choose the split and build a circuit.

Main results

• Cslib.Circuits.Boolean.ShannonSynthesis.computes_synthesize: correctness of synthesis.
• Cslib.Circuits.Boolean.ShannonSynthesis.size_synthesize_le: the finite 27 * 2 ^ n / n bound.
• Cslib.Circuits.Boolean.ShannonSynthesis.exists_circuit: the corresponding existence theorem.

References

• C. E. Shannon, The Synthesis of Two-Terminal Switching Circuits.
• The parameter choice and finite constant follow MassProduction/ShannonParameters.lean and MassProduction/ShannonSynthesis.lean in S. Schlesinger, Boolean circuit mass production formalization.

def Cslib.Circuits.Boolean.ShannonSynthesis.addressWidth (n : ℕ) : ℕ

Width of the address block in finite Shannon synthesis.

def Cslib.Circuits.Boolean.ShannonSynthesis.dataWidth (n : ℕ) : ℕ

Width of the remaining data block.

@[simp]

theorem Cslib.Circuits.Boolean.ShannonSynthesis.addressWidth_add_dataWidth (n : ℕ) : addressWidth n + dataWidth n = n

theorem Cslib.Circuits.Boolean.ShannonSynthesis.bound_le {n : ℕ} (hn : 16 ≤ n) : bound (addressWidth n) (dataWidth n) ≤ 27 * 2 ^ n / n

The chosen split bounds the complete gate ledger, with natural division after scaling.

def Cslib.Circuits.Boolean.ShannonSynthesis.synthesize {n : ℕ} (f : BooleanFunction n) : Circuit signature n 1

Build a circuit from a truth table, using the chosen address/data split.

@[simp]

theorem Cslib.Circuits.Boolean.ShannonSynthesis.eval_synthesize {n : ℕ} (f : BooleanFunction n) (x : BitString n) (i : Fin 1) : (synthesize f).eval interpretation x i = f x

theorem Cslib.Circuits.Boolean.ShannonSynthesis.computes_synthesize {n : ℕ} (f : BooleanFunction n) : (synthesize f).Computes interpretation (single f)

The synthesized circuit computes the supplied Boolean function.

theorem Cslib.Circuits.Boolean.ShannonSynthesis.size_synthesize_le {n : ℕ} (hn : 16 ≤ n) (f : BooleanFunction n) : (synthesize f).size ≤ 27 * 2 ^ n / n

Every gate is counted, including constants and negations.

theorem Cslib.Circuits.Boolean.ShannonSynthesis.exists_circuit {n : ℕ} (hn : 16 ≤ n) (f : BooleanFunction n) : ∃ (c : Circuit signature n 1), c.Computes interpretation (single f) ∧ c.size ≤ 27 * 2 ^ n / n

A finite Shannon bound on the total number of gates, valid at every width at least 16.