Documentation

Complexitylib.Algebraic.MassProduction.Nonuniform.PaddedLinePoints

A power-of-two line enumeration with fixed directions #

Enumerate all field scalars, marking the zero scalar invalid. The valid slots are exactly a punctured line. For a fixed nonuniform direction all scalar multiples are offline constants, so the point-generation circuit costs at most one gate per output bit.

source
noncomputable def Algebraic.MassProduction.Nonuniform.PaddedLinePoints.scalarAt {width : ℕ} (positive : 0 < width) (slot : Fin (2 ^ width)) :
BinaryExtension width

All field scalars, indexed by exactly 2^width slots.

Equations
Instances For
    source
    theorem Algebraic.MassProduction.Nonuniform.PaddedLinePoints.scalarAt_injective {width : ℕ} (positive : 0 < width) :
    Function.Injective (scalarAt positive)

    Every scalar occurs once.

    source
    theorem Algebraic.MassProduction.Nonuniform.PaddedLinePoints.scalarAt_surjective {width : ℕ} (positive : 0 < width) :
    Function.Surjective (scalarAt positive)

    The padded enumeration covers the whole field.

    source
    noncomputable def Algebraic.MassProduction.Nonuniform.PaddedLinePoints.valid {width : ℕ} (positive : 0 < width) (slot : Fin (2 ^ width)) :
    Bool

    The zero-scalar slot is padding; every other slot is valid.

    Equations
    Instances For
      source
      theorem Algebraic.MassProduction.Nonuniform.PaddedLinePoints.valid_eq_true_iff {width : ℕ} (positive : 0 < width) (slot : Fin (2 ^ width)) :
      valid positive slot = true ↔ scalarAt positive slot ≠ 0

      Validity is exactly nonzero scalar membership.

      source
      noncomputable def Algebraic.MassProduction.Nonuniform.PaddedLinePoints.point {width dimension : ℕ} (positive : 0 < width) (target : Fin dimension → BinaryExtension width) (direction : Projectivization (BinaryExtension width) (Fin dimension → BinaryExtension width)) (slot : Fin (2 ^ width)) :
      Fin dimension → BinaryExtension width

      The point at a padded scalar slot of a fixed projective direction.

      Equations
      Instances For
        source
        theorem Algebraic.MassProduction.Nonuniform.PaddedLinePoints.pointBits_injective {width dimension : ℕ} (positive : 0 < width) (target : Fin dimension → BinaryExtension width) (direction : Projectivization (BinaryExtension width) (Fin dimension → BinaryExtension width)) :
        Function.Injective fun (slot : Fin (2 ^ width)) => binaryExtensionVectorBits positive (point positive target direction slot)

        Points within one line have distinct encodings, including the padded target.

        source
        theorem Algebraic.MassProduction.Nonuniform.PaddedLinePoints.pointSet_eq {width dimension : ℕ} (positive : 0 < width) (target : Fin dimension → BinaryExtension width) (direction : Projectivization (BinaryExtension width) (Fin dimension → BinaryExtension width)) :
        (EnumeratedClean.pointSet (valid positive) fun (slot : Fin (2 ^ width)) => binaryExtensionVectorBits positive (point positive target direction slot)) = Finset.image (binaryExtensionVectorBits positive) (puncturedLine target direction)

        The valid encoded slots are exactly the encoded punctured line.

        source
        theorem Algebraic.MassProduction.Nonuniform.PaddedLinePoints.vectorBits_add {width dimension : ℕ} (positive : 0 < width) (left right : Fin dimension → BinaryExtension width) (bit : Fin (dimension * width)) :
        binaryExtensionVectorBits positive (left + right) bit = (binaryExtensionVectorBits positive left bit ^^ binaryExtensionVectorBits positive right bit)

        Vector addition is bitwise XOR in the fixed binary basis.

        source
        noncomputable def Algebraic.MassProduction.Nonuniform.PaddedLinePoints.circuit {width dimension : ℕ} (positive : 0 < width) (direction : Projectivization (BinaryExtension width) (Fin dimension → BinaryExtension width)) :
        Circuit DeMorgan.signature (dimension * width) (2 ^ width * (dimension * width))

        A fixed-direction line generator uses the target bits as its only inputs.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          @[simp]
          theorem Algebraic.MassProduction.Nonuniform.PaddedLinePoints.circuit_size {width dimension : ℕ} (positive : 0 < width) (direction : Projectivization (BinaryExtension width) (Fin dimension → BinaryExtension width)) :
          (circuit positive direction).size = (ConstantTranslations.circuit (fun (slot : Fin (2 ^ width)) => binaryExtensionVectorBits positive (scalarAt positive slot • direction.rep)) fun (x : Fin (2 ^ width)) (bit : Fin (dimension * width)) => DeMorgan.Wiring.input bit).size

          circuit has exactly the gates of ConstantTranslations.circuit; the surrounding wiring adds none.

          source
          theorem Algebraic.MassProduction.Nonuniform.PaddedLinePoints.circuit_eval {width dimension : ℕ} (positive : 0 < width) (target : Fin dimension → BinaryExtension width) (direction : Projectivization (BinaryExtension width) (Fin dimension → BinaryExtension width)) (slot : Fin (2 ^ width)) (bit : Fin (dimension * width)) :
          (circuit positive direction).eval DeMorgan.interpretation (binaryExtensionVectorBits positive target) (finProdFinEquiv (slot, bit)) = binaryExtensionVectorBits positive (point positive target direction slot) bit

          The circuit emits the complete padded affine line in slot order.

          source
          theorem Algebraic.MassProduction.Nonuniform.PaddedLinePoints.circuit_cost_le {width dimension : ℕ} (positive : 0 < width) (direction : Projectivization (BinaryExtension width) (Fin dimension → BinaryExtension width)) :
          (circuit positive direction).cost DeMorgan.standardCost ≤ 2 ^ width * (dimension * width)

          At most one charged gate per bit of each of the 2^width points.