Documentation

Complexity.Computability.Circuit.Boolean.Modular.PartialProduct.PolyTime

Native partial-product generation #

The complete shifted word is generated from unary width and shift. Every emitted gate and binary wire is charged. Out-of-range raw shifts have total behavior; the exact circuit theorem uses a valid shift.

Main results #

source
def Cslib.Circuits.Boolean.Modular.partialProductCode (w i : ℕ) :
List (Op × List ℕ) × List ℕ

Generate all retained shifted product digits, including the zero lower positions.

Instances For
    source
    theorem Cslib.Circuits.Boolean.Modular.partialProductCode_eq_code {w : ℕ} (i : Fin w) :
    partialProductCode w ↑i = (partialProduct w i).code

    Native generation retains exactly the existing parallel partial-product circuit.

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

    The full raw partial-product code is generated uniformly in unary width and shift.