Shannon synthesis parameters

This module specializes the native Shannon circuit cost ledger to the standard O(2^N / N) address-width choice.

A uniform O(2^N / N) specialization

The parameter choice and arithmetic below follow the full-column-library proof in ShannonUpper.lean. The circuit construction above is new to Algebraic; only the elementary choice k = floor(log_2 N) - 1 and its inequalities are reused.

def Algebraic.MassProduction.ShannonSynthesis.shannonAddressWidth (inputs : ℕ) : ℕ

Number of short address variables in the uniform specialization.

Equations

• Algebraic.MassProduction.ShannonSynthesis.shannonAddressWidth inputs = Nat.log 2 inputs - 1

def Algebraic.MassProduction.ShannonSynthesis.shannonDataWidth (inputs : ℕ) : ℕ

Number of remaining data variables.

Equations

• Algebraic.MassProduction.ShannonSynthesis.shannonDataWidth inputs = inputs - Algebraic.MassProduction.ShannonSynthesis.shannonAddressWidth inputs

theorem Algebraic.MassProduction.ShannonSynthesis.shannonAddressWidth_ge_three (inputs : ℕ) (inputsLarge : 16 ≤ inputs) : 3 ≤ shannonAddressWidth inputs

theorem Algebraic.MassProduction.ShannonSynthesis.shannonDataWidth_pos (inputs : ℕ) (inputsLarge : 16 ≤ inputs) : 0 < shannonDataWidth inputs

theorem Algebraic.MassProduction.ShannonSynthesis.shannonAddressDataSum (inputs : ℕ) (inputsLarge : 16 ≤ inputs) : shannonAddressWidth inputs + shannonDataWidth inputs = inputs

The selected address/data split has exactly the original input width.

theorem Algebraic.MassProduction.ShannonSynthesis.shannonArithmetic (inputs : ℕ) (inputsLarge : 16 ≤ inputs) : costBound (shannonAddressWidth inputs) (shannonDataWidth inputs) * inputs ≤ 27 * 2 ^ inputs

The full native Shannon cost ledger, multiplied by N, is bounded by 27 * 2^N.

theorem Algebraic.MassProduction.ShannonSynthesis.shannonCostBound_le (inputs : ℕ) (inputsLarge : 16 ≤ inputs) : costBound (shannonAddressWidth inputs) (shannonDataWidth inputs) ≤ 27 * 2 ^ inputs / inputs

The selected finite cost ledger is at most 27 * 2^N / N.