Documentation

Complexity.Computability.Circuit.Boolean.Modular.InnerProduct.PolyTime

Native modular inner-product generation #

Unary array count and word width generate all block selectors, complete product circuits and the balanced sum. Binary wire numbers and every generated code list are charged.

Main results #

source
def Cslib.Circuits.Boolean.Modular.innerProductCode (k w : ℕ) :
List (Op × List ℕ) × List ℕ

Generate every product and its zero carry-save companion before the complete sum.

Instances For
    source
    theorem Cslib.Circuits.Boolean.Modular.innerProductCode_eq_code (k w : ℕ) :
    innerProductCode k w = (innerProduct k w).code

    Gate-for-gate agreement includes empty arrays and zero-width words.

    source
    theorem Cslib.Circuits.Boolean.Modular.computableInPolyTime_innerProduct :
    Turing.MultiTapeTM.ComputableInPolyTime (fun (p : ℕ × ℕ) => (innerProduct p.1 p.2).code) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) encCode

    The full constructor is uniform in unary count and width.