Documentation

Complexitylib.Algebraic.MassProduction.Nonuniform.BufferedPhase

A universal compacted halving step #

For fixed buffer sizes and field parameters, one concrete circuit accepts half the pending requests and produces the next encoded buffer. The circuit works for every original request dataset with distinct identities and the stated target projection. All menu choices precede the input and state.

source
def Algebraic.MassProduction.Nonuniform.BufferedPhase.menuDepth (total requestDepth dimension width : ℕ) :
ℕ

Sorting depth of the fixed universal menu for this pending count.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def Algebraic.MassProduction.Nonuniform.BufferedPhase.routingRecords (total completed requestDepth dimension width : ℕ) :
    ℕ

    Source records plus all generated candidate points.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def Algebraic.MassProduction.Nonuniform.BufferedPhase.routingDepth (total completed requestDepth dimension width : ℕ) :
      ℕ

      Canonical routing depth for shared occupancy lookup.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        theorem Algebraic.MassProduction.Nonuniform.BufferedPhase.recordCount (total completed requestDepth dimension width : ℕ) :
        completed * 2 ^ width + Sorting.networkRecords (menuDepth total requestDepth dimension width + requestDepth + width) + FiniteParameters.paddingCount (routingRecords total completed requestDepth dimension width) = Sorting.networkRecords (routingDepth total completed requestDepth dimension width)

        Canonical padding gives the exact required occupancy-router capacity.

        source
        def Algebraic.MassProduction.Nonuniform.BufferedPhase.costBound (total completed requestDepth dimension width requestWidth : ℕ) :
        ℕ

        The explicit cost bound for one complete compacted buffer step.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          theorem Algebraic.MassProduction.Nonuniform.BufferedPhase.existsCircuit {width dimension completed requestDepth total requestWidth : ℕ} (positive : 0 < width) (dimensionPositive : 0 < dimension) (counts : completed + Sorting.networkRecords requestDepth = total) (budget : 512 * total * Nat.card (BinaryExtension width) ≤ Nat.card (Projectivization (BinaryExtension width) (Fin dimension → BinaryExtension width))) (targetProjection : Fin (dimension * width) → Fin requestWidth) :
          ∃ (step : Circuit DeMorgan.signature (BufferInput.inputWidth completed (Sorting.networkRecords requestDepth) requestWidth (2 ^ width) (dimension * width)) (BufferInput.inputWidth (completed + acceptedCount requestDepth) (pendingCount requestDepth) requestWidth (2 ^ width) (dimension * width))), step.cost DeMorgan.standardCost ≤ costBound total completed requestDepth dimension width requestWidth ∧ BufferModel.Transforms positive targetProjection step total

          A fixed circuit advances every valid encoded buffer and preserves its geometric and request-identity invariants. Compaction adds no charged cost.