Uniform Shannon synthesis

This module packages the standard O(2^N / N) Shannon circuit and connects it to Boolean mass complexity.

def Algebraic.MassProduction.ShannonSynthesis.reindexFunction {splitInputs inputs : ℕ} (inputCount : splitInputs = inputs) (function : ScalarFunction Bool inputs) : ScalarFunction Bool splitInputs

Reindex a function along an equality of finite input counts.

Equations

• Algebraic.MassProduction.ShannonSynthesis.reindexFunction inputCount function input = function (input ∘ Fin.cast ⋯)

noncomputable def Algebraic.MassProduction.ShannonSynthesis.shannonCircuit (inputs : ℕ) (inputsLarge : 16 ≤ inputs) (function : ScalarFunction Bool inputs) : Circuit DeMorgan.signature inputs 1

Uniform native Shannon circuit for an arbitrary N-input Boolean function.

Equations

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

@[simp]

theorem Algebraic.MassProduction.ShannonSynthesis.shannonCircuit_size (inputs : ℕ) (inputsLarge : 16 ≤ inputs) (function : ScalarFunction Bool inputs) : (shannonCircuit inputs inputsLarge function).size = synthesisGateCount (reindexFunction ⋯ function)

@[simp]

theorem Algebraic.MassProduction.ShannonSynthesis.shannonCircuit_eval (inputs : ℕ) (inputsLarge : 16 ≤ inputs) (function : ScalarFunction Bool inputs) (input : Fin inputs → Bool) : (shannonCircuit inputs inputsLarge function).eval DeMorgan.interpretation input 0 = function input

theorem Algebraic.MassProduction.ShannonSynthesis.shannonCircuit_computes (inputs : ℕ) (inputsLarge : 16 ≤ inputs) (function : ScalarFunction Bool inputs) : (shannonCircuit inputs inputsLarge function).ComputesWith DeMorgan.interpretation (scalarTarget function)

theorem Algebraic.MassProduction.ShannonSynthesis.shannonCircuit_cost_le (inputs : ℕ) (inputsLarge : 16 ≤ inputs) (function : ScalarFunction Bool inputs) : (shannonCircuit inputs inputsLarge function).cost DeMorgan.standardCost ≤ 27 * 2 ^ inputs / inputs

noncomputable def Algebraic.MassProduction.ShannonSynthesis.replicatedShannonCircuit (inputs : ℕ) (inputsLarge : 16 ≤ inputs) (function : ScalarFunction Bool inputs) (copies : ℕ) : Circuit DeMorgan.signature (copies * inputs) copies

The concrete independently replicated Shannon circuit.

Equations

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

@[simp]

theorem Algebraic.MassProduction.ShannonSynthesis.replicatedShannonCircuit_size (inputs : ℕ) (inputsLarge : 16 ≤ inputs) (function : ScalarFunction Bool inputs) (copies : ℕ) : (replicatedShannonCircuit inputs inputsLarge function copies).size = copies * synthesisGateCount (reindexFunction ⋯ function)

theorem Algebraic.MassProduction.ShannonSynthesis.replicatedShannonCircuit_computes (inputs : ℕ) (inputsLarge : 16 ≤ inputs) (function : ScalarFunction Bool inputs) (copies : ℕ) : (replicatedShannonCircuit inputs inputsLarge function copies).ComputesWith DeMorgan.interpretation (directProduct function copies)

noncomputable def Algebraic.MassProduction.ShannonSynthesis.minimumMassCircuit (inputs : ℕ) (inputsLarge : 16 ≤ inputs) (function : ScalarFunction Bool inputs) (copies : ℕ) : Circuit.Minimum DeMorgan.standardCost DeMorgan.interpretation (directProduct function copies)

A minimum-cost realization of a finite Boolean direct product, selected from the nonempty implementation family witnessed by Shannon replication.

Equations

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

theorem Algebraic.MassProduction.ShannonSynthesis.minimumMassCircuit_cost_eq_complexity (inputs : ℕ) (inputsLarge : 16 ≤ inputs) (function : ScalarFunction Bool inputs) (copies : ℕ) : booleanMassComplexity function copies = ↑((minimumMassCircuit inputs inputsLarge function copies).circuit.cost DeMorgan.standardCost)

The selected minimum circuit realizes booleanMassComplexity exactly.

theorem Algebraic.MassProduction.ShannonSynthesis.minimumMassCircuit_cost_le (inputs : ℕ) (inputsLarge : 16 ≤ inputs) (function : ScalarFunction Bool inputs) (copies bound : ℕ) (complexityBound : booleanMassComplexity function copies ≤ ↑bound) : (minimumMassCircuit inputs inputsLarge function copies).circuit.cost DeMorgan.standardCost ≤ bound

theorem Algebraic.MassProduction.ShannonSynthesis.booleanMassComplexity_le_replicatedShannon (inputs : ℕ) (inputsLarge : 16 ≤ inputs) (function : ScalarFunction Bool inputs) (copies : ℕ) : booleanMassComplexity function copies ≤ ↑(copies * (27 * 2 ^ inputs / inputs))

Naive replication of native Shannon synthesis bounds any finite number of independent copies. This is the base finite upper bound used before the mass-production composition improves the dependence on copies.