Factored polynomial overhead bound

The concrete composition ledger contains several large expanded formulas. This module factors each of them into the number of live power-of-two records times a polynomial coefficient in bit widths and sorting depths. The result retains the manuscript's three meaningful volumes: grouped scheduler work, incidences, and resource slots. No asymptotic notation and no instances are introduced.

def Algebraic.MassProduction.OverheadBound.schedulerStandaloneCoefficient (dimension width : ℕ) : ℕ

Non-record-multiplied cost of projective unranking in one scheduler stage.

Equations

• Algebraic.MassProduction.OverheadBound.schedulerStandaloneCoefficient dimension width = dimension * width * (dimension * (2 * width + 2 + dimension * (2 * width + 1) + 2))

def Algebraic.MassProduction.OverheadBound.freshRankRecordedCoefficient (dimension width depth : ℕ) : ℕ

Coefficient of networkRecords depth in fresh-rank selection.

Equations

• One or more equations did not get rendered due to their size.

def Algebraic.MassProduction.OverheadBound.schedulerRecordedCoefficient (dimension width depth : ℕ) : ℕ

Complete coefficient of record-multiplied work in one scheduler stage.

Equations

• One or more equations did not get rendered due to their size.

def Algebraic.MassProduction.OverheadBound.schedulerCoefficient (dimension width depth : ℕ) : ℕ

Polynomial coefficient which absorbs both record-multiplied and the standalone work of one scheduler stage.

Equations

• One or more equations did not get rendered due to their size.

def Algebraic.MassProduction.OverheadBound.lineCoefficient (dimension width : ℕ) : ℕ

Per-field-element polynomial work of explicit line enumeration.

Equations

• Algebraic.MassProduction.OverheadBound.lineCoefficient dimension width = dimension * (width * (6 * (width * width)) + 4 * width)

theorem Algebraic.MassProduction.OverheadBound.schedulerStageCostBound_eq (dimension width depth : ℕ) : SchedulerStage.schedulerStageCostBound dimension width depth = Sorting.networkRecords depth * schedulerRecordedCoefficient dimension width depth + schedulerStandaloneCoefficient dimension width

theorem Algebraic.MassProduction.OverheadBound.schedulerStageCostBound_le (dimension width depth : ℕ) : SchedulerStage.schedulerStageCostBound dimension width depth ≤ Sorting.networkRecords depth * schedulerCoefficient dimension width depth

theorem Algebraic.MassProduction.OverheadBound.scheduledLineEnumerationCostBound_le (dimension width depth : ℕ) : LineEnumeration.scheduledLineEnumerationCostBound dimension width depth ≤ Sorting.networkRecords depth * schedulerCoefficient dimension width depth + 2 ^ width * lineCoefficient dimension width

def Algebraic.MassProduction.OverheadBound.scatterCoefficient (depth keyWidth payloadWidth : ℕ) : ℕ

Polynomial multiplier after factoring out the scatter record count.

Equations

• One or more equations did not get rendered due to their size.

theorem Algebraic.MassProduction.OverheadBound.scatterRoutingCostBound_eq (depth keyWidth payloadWidth : ℕ) : CompositionBound.scatterRoutingCostBound depth keyWidth payloadWidth = Sorting.networkRecords depth * scatterCoefficient depth keyWidth payloadWidth

def Algebraic.MassProduction.OverheadBound.gatherCoefficient (depth keyWidth metadataWidth valueWidth : ℕ) : ℕ

Polynomial multiplier after factoring out the gather record count.

Equations

• One or more equations did not get rendered due to their size.

theorem Algebraic.MassProduction.OverheadBound.gatherRoutingCostBound_eq (depth keyWidth metadataWidth valueWidth : ℕ) : CompositionBound.gatherRoutingCostBound depth keyWidth metadataWidth valueWidth = Sorting.networkRecords depth * gatherCoefficient depth keyWidth metadataWidth valueWidth

def Algebraic.MassProduction.OverheadBound.packingCoefficient (prefixWidth dimension width : ℕ) : ℕ

Polynomial multiplier for runtime prefix packing after factoring out one field cardinality.

Equations

• Algebraic.MassProduction.OverheadBound.packingCoefficient prefixWidth dimension width = prefixWidth * (8 * width) + dimension * (prefixWidth * 8) + dimension * width * 2

theorem Algebraic.MassProduction.OverheadBound.gridWidth_le_fieldCard (dimension width : ℕ) (widthPositive : 0 < width) : CanonicalPacking.gridWidth dimension width ≤ 2 ^ width

theorem Algebraic.MassProduction.OverheadBound.packingCostBound_le (prefixWidth dimension width : ℕ) (widthPositive : 0 < width) : CompositionBound.packingCostBound prefixWidth dimension width ≤ 2 ^ width * packingCoefficient prefixWidth dimension width

def Algebraic.MassProduction.OverheadBound.coefficientEnvelope (bound : ℕ) : ℕ

One polynomial envelope for every coefficient in the factored ledger.

Equations

• One or more equations did not get rendered due to their size.

theorem Algebraic.MassProduction.OverheadBound.coefficientEnvelope_le (bound : ℕ) : coefficientEnvelope bound ≤ 1000000 * (bound + 1) ^ 10

theorem Algebraic.MassProduction.OverheadBound.coefficients_le_envelope (dimension width schedulerDepth prefixWidth keyWidth suffixWidth orderWidth routingDepth bound : ℕ) (dimensionBound : dimension ≤ bound) (widthBound : width ≤ bound) (schedulerDepthBound : schedulerDepth ≤ bound) (prefixWidthBound : prefixWidth ≤ bound) (keyWidthBound : keyWidth ≤ bound) (suffixWidthBound : suffixWidth ≤ bound) (orderWidthBound : orderWidth + 1 ≤ bound) (routingDepthBound : routingDepth ≤ bound) : schedulerCoefficient dimension width schedulerDepth ≤ coefficientEnvelope bound ∧ lineCoefficient dimension width ≤ coefficientEnvelope bound ∧ packingCoefficient prefixWidth dimension width ≤ coefficientEnvelope bound ∧ scatterCoefficient routingDepth keyWidth suffixWidth ≤ coefficientEnvelope bound ∧ gatherCoefficient routingDepth keyWidth (orderWidth + 1) width ≤ coefficientEnvelope bound

Every ledger coefficient is monotone in its bit-width and depth parameters, and hence lies below the common envelope at any shared upper bound.

def Algebraic.MassProduction.OverheadBound.factoredOverhead (totalRequests groups prefixWidth dimension width suffixWidth schedulerDepth groupBitWidth orderWidth routingDepth : ℕ) : ℕ

Factored form of every non-resource contribution.

Equations

• One or more equations did not get rendered due to their size.

def Algebraic.MassProduction.OverheadBound.overheadVolume (totalRequests groups width schedulerDepth routingDepth : ℕ) : ℕ

Sum of the three live record volumes after the two identical totalRequests * fieldCardinality contributions are combined.

Equations

• One or more equations did not get rendered due to their size.

theorem Algebraic.MassProduction.OverheadBound.factoredOverhead_le_volume_mul_envelope (totalRequests groups prefixWidth dimension width suffixWidth schedulerDepth groupBitWidth orderWidth routingDepth bound : ℕ) (dimensionBound : dimension ≤ bound) (widthBound : width ≤ bound) (schedulerDepthBound : schedulerDepth ≤ bound) (prefixWidthBound : prefixWidth ≤ bound) (keyWidthBound : IncidenceRouting.incidenceKeyWidth groupBitWidth dimension width ≤ bound) (suffixWidthBound : suffixWidth ≤ bound) (orderWidthBound : orderWidth + 1 ≤ bound) (routingDepthBound : routingDepth ≤ bound) : factoredOverhead totalRequests groups prefixWidth dimension width suffixWidth schedulerDepth groupBitWidth orderWidth routingDepth ≤ overheadVolume totalRequests groups width schedulerDepth routingDepth * (coefficientEnvelope bound + 5 * bound)

Once all widths and depths share a bound, the complete factored ledger is the live record volume times one explicit degree-ten polynomial envelope.

theorem Algebraic.MassProduction.OverheadBound.overheadCostBound_le_factored (totalRequests groups prefixWidth dimension width suffixWidth schedulerDepth groupBitWidth orderWidth routingDepth : ℕ) (widthPositive : 0 < width) : CompositionBound.overheadCostBound totalRequests groups prefixWidth dimension width suffixWidth schedulerDepth groupBitWidth orderWidth routingDepth routingDepth ≤ factoredOverhead totalRequests groups prefixWidth dimension width suffixWidth schedulerDepth groupBitWidth orderWidth routingDepth

The canonical expanded overhead is bounded by the factored record-volume ledger.