Documentation

Complexitylib.Algebraic.MassProduction.Nonuniform.PreparedInputs

Shared generated values with preserved original inputs #

A preprocessing circuit runs once and retains all original input wires. Downstream wiring can select generated values or original values without duplicating the preprocessing computation or adding charged gates.

source
def Algebraic.MassProduction.Nonuniform.PreparedInputs.circuit {inputs outputs : ℕ} (generated : Circuit DeMorgan.signature inputs outputs) :
Circuit DeMorgan.signature inputs (outputs + inputs)

Preserve the original inputs after the generated output block.

Equations
Instances For
    source
    @[simp]
    theorem Algebraic.MassProduction.Nonuniform.PreparedInputs.circuit_size {inputs outputs : ℕ} (generated : Circuit DeMorgan.signature inputs outputs) :
    (circuit generated).size = generated.size

    The exact gate count of circuit.

    source
    def Algebraic.MassProduction.Nonuniform.PreparedInputs.original {inputs : ℕ} (outputs : ℕ) (wire : DeMorgan.Wiring inputs) :
    DeMorgan.Wiring (outputs + inputs)

    Lift an original wire or constant past the generated output block.

    Equations
    Instances For
      source
      def Algebraic.MassProduction.Nonuniform.PreparedInputs.output {outputs : ℕ} (inputs : ℕ) (index : Fin outputs) :
      DeMorgan.Wiring (outputs + inputs)

      Select one generated output wire.

      Equations
      Instances For
        source
        theorem Algebraic.MassProduction.Nonuniform.PreparedInputs.circuit_eval {inputs outputs : ℕ} (generated : Circuit DeMorgan.signature inputs outputs) (input : Fin inputs → Bool) :
        (circuit generated).eval DeMorgan.interpretation input = Fin.append (generated.eval DeMorgan.interpretation input) input

        The preprocessing output is its generated values followed by the original input.

        source
        theorem Algebraic.MassProduction.Nonuniform.PreparedInputs.original_eval {inputs outputs : ℕ} (generated : Circuit DeMorgan.signature inputs outputs) (wire : DeMorgan.Wiring inputs) (input : Fin inputs → Bool) :
        DeMorgan.Wiring.eval ((circuit generated).eval DeMorgan.interpretation input) (original outputs wire) = DeMorgan.Wiring.eval input wire

        Original values survive preprocessing exactly.

        source
        theorem Algebraic.MassProduction.Nonuniform.PreparedInputs.output_eval {inputs outputs : ℕ} (generated : Circuit DeMorgan.signature inputs outputs) (index : Fin outputs) (input : Fin inputs → Bool) :
        DeMorgan.Wiring.eval ((circuit generated).eval DeMorgan.interpretation input) (output inputs index) = generated.eval DeMorgan.interpretation input index

        Generated values are available as fixed wires.

        source
        theorem Algebraic.MassProduction.Nonuniform.PreparedInputs.circuit_cost {inputs outputs : ℕ} (generated : Circuit DeMorgan.signature inputs outputs) :
        (circuit generated).cost DeMorgan.standardCost = generated.cost DeMorgan.standardCost

        Keeping the original inputs adds no charged gates.