Documentation

Complexitylib.Algebraic.MassProduction.RuntimePacking

Runtime canonical prefix packing #

This module computes the manuscript's canonical placement from runtime prefix bits. It first divides the represented prefix index by the field-basis width, retaining the one-hot remainder j. It then performs dimension repeated divisions by the tensor-grid width and encodes each one-hot base digit in the fixed binary field basis.

The output is the row-major target point followed by the one-hot selected basis coordinate. The construction uses no new type-class instances.

source
def Algebraic.MassProduction.RuntimePacking.source {prefixWidth : ℕ} (input : Fin prefixWidth → Bool) :
Fin (2 ^ prefixWidth)

Runtime prefix source under the explicit little-endian Boolean encoding.

Equations
Instances For
    source
    theorem Algebraic.MassProduction.RuntimePacking.canonicalBitIndex_val {prefixWidth dimension width : ℕ} (packingFits : 2 ^ prefixWidth ≤ CanonicalPacking.gridWidth dimension width ^ dimension * width) (input : Fin prefixWidth → Bool) :
    ↑(CanonicalPacking.bitIndex packingFits (source input)) = ↑(source input) % width
    source
    theorem Algebraic.MassProduction.RuntimePacking.canonicalSymbolDigit_val {prefixWidth dimension width : ℕ} (packingFits : 2 ^ prefixWidth ≤ CanonicalPacking.gridWidth dimension width ^ dimension * width) (input : Fin prefixWidth → Bool) (coordinate : Fin dimension) :
    ↑(CanonicalPacking.symbolDigits packingFits (source input) coordinate) = ↑(source input) / width / CanonicalPacking.gridWidth dimension width ^ ↑coordinate % CanonicalPacking.gridWidth dimension width
    source
    @[reducible]
    noncomputable def Algebraic.MassProduction.RuntimePacking.coreOutputCount (prefixWidth dimension width : ℕ) :
    ℕ

    Output width before one-hot digits are encoded as field bits.

    Equations
    Instances For
      source
      def Algebraic.MassProduction.RuntimePacking.conversionInputIndex (prefixWidth width : ℕ) :
      Fin prefixWidth → Fin (prefixWidth + width)

      Feed only the current quotient block to repeated base conversion.

      Equations
      Instances For
        source
        def Algebraic.MassProduction.RuntimePacking.selectorInputIndex (prefixWidth width : ℕ) :
        Fin width → Fin (prefixWidth + width)

        Retain the first division's one-hot basis-coordinate remainder.

        Equations
        Instances For
          source
          noncomputable def Algebraic.MassProduction.RuntimePacking.conversionStageCircuit (prefixWidth dimension width : ℕ) (gridPositive : 0 < CanonicalPacking.gridWidth dimension width) :
          Circuit DeMorgan.signature (prefixWidth + width) (coreOutputCount prefixWidth dimension width)

          Repeated grid-base conversion alongside the retained selector. It has exactly BaseConversion.gateCount gates (conversionStageCircuit_size).

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            @[simp]
            theorem Algebraic.MassProduction.RuntimePacking.conversionStageCircuit_size (prefixWidth dimension width : ℕ) (gridPositive : 0 < CanonicalPacking.gridWidth dimension width) :
            (conversionStageCircuit prefixWidth dimension width gridPositive).size = BaseConversion.gateCount prefixWidth gridPositive dimension

            The conversion stage has exactly the gates of the repeated grid-base conversion; carrying the one-hot selector alongside it is pure wiring.

            source
            noncomputable def Algebraic.MassProduction.RuntimePacking.coreCircuit {width : ℕ} (prefixWidth dimension : ℕ) (widthPositive : 0 < width) (gridPositive : 0 < CanonicalPacking.gridWidth dimension width) :
            Circuit DeMorgan.signature prefixWidth (coreOutputCount prefixWidth dimension width)

            Divide by width, convert the quotient to base gridWidth, and retain the one-hot width remainder.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              @[simp]
              theorem Algebraic.MassProduction.RuntimePacking.coreCircuit_size {width : ℕ} (prefixWidth dimension : ℕ) (widthPositive : 0 < width) (gridPositive : 0 < CanonicalPacking.gridWidth dimension width) :
              (coreCircuit prefixWidth dimension widthPositive gridPositive).size = FixedDivision.prefixGateCount prefixWidth widthPositive prefixWidth + BaseConversion.gateCount prefixWidth gridPositive dimension
              source
              noncomputable def Algebraic.MassProduction.RuntimePacking.coreDigitIndex (prefixWidth dimension width : ℕ) (coordinate : Fin dimension) (candidate : Fin (CanonicalPacking.gridWidth dimension width)) :
              Fin (coreOutputCount prefixWidth dimension width)

              Core output index of one one-hot tensor-grid digit.

              Equations
              Instances For
                source
                noncomputable def Algebraic.MassProduction.RuntimePacking.coreSelectorIndex (prefixWidth dimension width : ℕ) (candidate : Fin width) :
                Fin (coreOutputCount prefixWidth dimension width)

                Core output index of one retained basis-coordinate selector bit.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  source
                  theorem Algebraic.MassProduction.RuntimePacking.coreCircuit_digit_oneHot {width dimension prefixWidth : ℕ} (widthPositive : 0 < width) (gridPositive : 0 < CanonicalPacking.gridWidth dimension width) (packingFits : 2 ^ prefixWidth ≤ CanonicalPacking.gridWidth dimension width ^ dimension * width) (input : Fin prefixWidth → Bool) (coordinate : Fin dimension) (candidate : Fin (CanonicalPacking.gridWidth dimension width)) :
                  (coreCircuit prefixWidth dimension widthPositive gridPositive).eval DeMorgan.interpretation input (coreDigitIndex prefixWidth dimension width coordinate candidate) = decide (candidate = CanonicalPacking.symbolDigits packingFits (source input) coordinate)
                  source
                  theorem Algebraic.MassProduction.RuntimePacking.coreCircuit_selector_oneHot {width dimension prefixWidth : ℕ} (widthPositive : 0 < width) (gridPositive : 0 < CanonicalPacking.gridWidth dimension width) (packingFits : 2 ^ prefixWidth ≤ CanonicalPacking.gridWidth dimension width ^ dimension * width) (input : Fin prefixWidth → Bool) (candidate : Fin width) :
                  (coreCircuit prefixWidth dimension widthPositive gridPositive).eval DeMorgan.interpretation input (coreSelectorIndex prefixWidth dimension width candidate) = decide (candidate = CanonicalPacking.bitIndex packingFits (source input))

                  Encoding one-hot grid digits as target-point bits #

                  source
                  noncomputable def Algebraic.MassProduction.RuntimePacking.digitInputIndex (prefixWidth dimension width : ℕ) (coordinate : Fin dimension) (candidate : Fin (CanonicalPacking.gridWidth dimension width)) :
                  Fin (coreOutputCount prefixWidth dimension width)

                  Input wire for one grid candidate in one coordinate block.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    source
                    noncomputable def Algebraic.MassProduction.RuntimePacking.targetBitExpression (prefixWidth dimension width : ℕ) (coordinate : Fin dimension) (bit : Fin width) :
                    DeMorgan.Expression (coreOutputCount prefixWidth dimension width)

                    One target-point bit, obtained by selecting the hardwired binary encoding of the active grid digit.

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      source
                      @[reducible]
                      noncomputable def Algebraic.MassProduction.RuntimePacking.targetEncoderGateCount (prefixWidth dimension width : ℕ) :
                      ℕ

                      Emitted gate count of all encoded target-point bits.

                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        source
                        noncomputable def Algebraic.MassProduction.RuntimePacking.targetEncoderCircuit (prefixWidth dimension width : ℕ) :
                        Circuit DeMorgan.signature (coreOutputCount prefixWidth dimension width) (dimension * width)

                        Encode all one-hot grid digits in row-major fixed-width binary form.

                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For
                          source
                          @[simp]
                          theorem Algebraic.MassProduction.RuntimePacking.targetEncoderCircuit_size (prefixWidth dimension width : ℕ) :
                          (targetEncoderCircuit prefixWidth dimension width).size = targetEncoderGateCount prefixWidth dimension width
                          source
                          theorem Algebraic.MassProduction.RuntimePacking.targetBitExpression_eval_oneHot {prefixWidth dimension width : ℕ} (input : Fin (coreOutputCount prefixWidth dimension width) → Bool) (coordinate : Fin dimension) (selected : Fin (CanonicalPacking.gridWidth dimension width)) (oneHot : ∀ (candidate : Fin (CanonicalPacking.gridWidth dimension width)), input (digitInputIndex prefixWidth dimension width coordinate candidate) = decide (candidate = selected)) (bit : Fin width) :
                          DeMorgan.Expression.eval input (targetBitExpression prefixWidth dimension width coordinate bit) = finiteIndexBits width selected bit
                          source
                          @[simp]
                          theorem Algebraic.MassProduction.RuntimePacking.targetEncoderCircuit_eval {prefixWidth dimension width : ℕ} (input : Fin (coreOutputCount prefixWidth dimension width) → Bool) (selected : Fin dimension → Fin (CanonicalPacking.gridWidth dimension width)) (oneHot : ∀ (coordinate : Fin dimension) (candidate : Fin (CanonicalPacking.gridWidth dimension width)), input (digitInputIndex prefixWidth dimension width coordinate candidate) = decide (candidate = selected coordinate)) (coordinate : Fin dimension) (bit : Fin width) :
                          (targetEncoderCircuit prefixWidth dimension width).eval DeMorgan.interpretation input (finProdFinEquiv (coordinate, bit)) = finiteIndexBits width (selected coordinate) bit
                          source
                          noncomputable def Algebraic.MassProduction.RuntimePacking.selectorCircuit (prefixWidth dimension width : ℕ) :
                          Circuit DeMorgan.signature (coreOutputCount prefixWidth dimension width) width

                          Retain the one-hot selected field coordinate after target encoding.

                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            source
                            @[simp]
                            theorem Algebraic.MassProduction.RuntimePacking.selectorCircuit_size (prefixWidth dimension width : ℕ) :
                            (selectorCircuit prefixWidth dimension width).size = 0

                            selectorCircuit is pure wiring: it has no gates.

                            source
                            @[reducible]
                            def Algebraic.MassProduction.RuntimePacking.outputCount (dimension width : ℕ) :
                            ℕ

                            Final output width: target point followed by one-hot basis selector.

                            Equations
                            Instances For
                              source
                              noncomputable def Algebraic.MassProduction.RuntimePacking.circuit {width : ℕ} (prefixWidth dimension : ℕ) (widthPositive : 0 < width) (gridPositive : 0 < CanonicalPacking.gridWidth dimension width) :
                              Circuit DeMorgan.signature prefixWidth (outputCount dimension width)

                              Runtime canonical packing circuit for one prefix.

                              Equations
                              • One or more equations did not get rendered due to their size.
                              Instances For
                                source
                                @[simp]
                                theorem Algebraic.MassProduction.RuntimePacking.circuit_size {width : ℕ} (prefixWidth dimension : ℕ) (widthPositive : 0 < width) (gridPositive : 0 < CanonicalPacking.gridWidth dimension width) :
                                (circuit prefixWidth dimension widthPositive gridPositive).size = FixedDivision.prefixGateCount prefixWidth widthPositive prefixWidth + BaseConversion.gateCount prefixWidth gridPositive dimension + targetEncoderGateCount prefixWidth dimension width
                                source
                                theorem Algebraic.MassProduction.RuntimePacking.circuit_eval_target {width dimension prefixWidth : ℕ} (widthPositive : 0 < width) (gridPositive : 0 < CanonicalPacking.gridWidth dimension width) (packingFits : 2 ^ prefixWidth ≤ CanonicalPacking.gridWidth dimension width ^ dimension * width) (input : Fin prefixWidth → Bool) (coordinate : Fin dimension) (bit : Fin width) :
                                (circuit prefixWidth dimension widthPositive gridPositive).eval DeMorgan.interpretation input (Fin.castAdd width (finProdFinEquiv (coordinate, bit))) = finiteIndexBits width (CanonicalPacking.symbolDigits packingFits (source input) coordinate) bit

                                Runtime target bits agree exactly with the canonical packed point.

                                source
                                theorem Algebraic.MassProduction.RuntimePacking.circuit_eval_selector {width dimension prefixWidth : ℕ} (widthPositive : 0 < width) (gridPositive : 0 < CanonicalPacking.gridWidth dimension width) (packingFits : 2 ^ prefixWidth ≤ CanonicalPacking.gridWidth dimension width ^ dimension * width) (input : Fin prefixWidth → Bool) (candidate : Fin width) :
                                (circuit prefixWidth dimension widthPositive gridPositive).eval DeMorgan.interpretation input (Fin.natAdd (dimension * width) candidate) = decide (candidate = CanonicalPacking.bitIndex packingFits (source input))

                                Runtime selector bits are one-hot at the canonical basis coordinate.

                                Cost #

                                source
                                theorem Algebraic.MassProduction.RuntimePacking.targetBitExpression_standardCost {dimension width prefixWidth : ℕ} (coordinate : Fin dimension) (bit : Fin width) :
                                (targetBitExpression prefixWidth dimension width coordinate bit).standardCost = 2 * CanonicalPacking.gridWidth dimension width
                                source
                                @[simp]
                                theorem Algebraic.MassProduction.RuntimePacking.targetEncoderCircuit_cost {prefixWidth dimension width : ℕ} :
                                (targetEncoderCircuit prefixWidth dimension width).cost DeMorgan.standardCost = dimension * width * (2 * CanonicalPacking.gridWidth dimension width)
                                source
                                @[simp]
                                theorem Algebraic.MassProduction.RuntimePacking.conversionStageCircuit_cost {dimension width prefixWidth : ℕ} (gridPositive : 0 < CanonicalPacking.gridWidth dimension width) :
                                (conversionStageCircuit prefixWidth dimension width gridPositive).cost DeMorgan.standardCost = (BaseConversion.circuit prefixWidth gridPositive dimension).cost DeMorgan.standardCost
                                source
                                @[simp]
                                theorem Algebraic.MassProduction.RuntimePacking.coreCircuit_cost {width dimension prefixWidth : ℕ} (widthPositive : 0 < width) (gridPositive : 0 < CanonicalPacking.gridWidth dimension width) :
                                (coreCircuit prefixWidth dimension widthPositive gridPositive).cost DeMorgan.standardCost = (FixedDivision.circuit prefixWidth widthPositive).cost DeMorgan.standardCost + (BaseConversion.circuit prefixWidth gridPositive dimension).cost DeMorgan.standardCost
                                source
                                theorem Algebraic.MassProduction.RuntimePacking.circuit_cost {width dimension prefixWidth : ℕ} (widthPositive : 0 < width) (gridPositive : 0 < CanonicalPacking.gridWidth dimension width) :
                                (circuit prefixWidth dimension widthPositive gridPositive).cost DeMorgan.standardCost = (FixedDivision.circuit prefixWidth widthPositive).cost DeMorgan.standardCost + (BaseConversion.circuit prefixWidth gridPositive dimension).cost DeMorgan.standardCost + dimension * width * (2 * CanonicalPacking.gridWidth dimension width)
                                source
                                theorem Algebraic.MassProduction.RuntimePacking.circuit_cost_le {width dimension prefixWidth : ℕ} (widthPositive : 0 < width) (gridPositive : 0 < CanonicalPacking.gridWidth dimension width) :
                                (circuit prefixWidth dimension widthPositive gridPositive).cost DeMorgan.standardCost ≤ prefixWidth * (8 * width) + dimension * (prefixWidth * (8 * CanonicalPacking.gridWidth dimension width)) + dimension * width * (2 * CanonicalPacking.gridWidth dimension width)

                                Explicit linear-in-grid packing cost.