Finite composition bound

This module packages the exact runtime pipeline as the finite counterpart of the manuscript's composition proposition. If every shorter resource circuit has cost at most resourceBound, then the resource term is

resourceBitCount dimension width * resourceBound,

the literal q^ell * b * L_C(d) term. Every remaining contribution is an explicit natural-number expression. No asymptotic notation and no new type-class instances are used here.

@[reducible]

noncomputable def Algebraic.MassProduction.CompositionBound.packingCostBound (prefixWidth dimension width : ℕ) : ℕ

Explicit upper bound for runtime canonical prefix packing per request.

Equations

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

@[reducible]

def Algebraic.MassProduction.CompositionBound.scatterRoutingCostBound (depth keyWidth payloadWidth : ℕ) : ℕ

The polynomial bound proved for the two-sort scatter router.

Equations

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

@[reducible]

def Algebraic.MassProduction.CompositionBound.gatherRoutingCostBound (depth keyWidth metadataWidth valueWidth : ℕ) : ℕ

The polynomial bound proved for the metadata-preserving gather router.

Equations

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

@[reducible]

noncomputable def Algebraic.MassProduction.CompositionBound.overheadCostBound (totalRequests groups prefixWidth dimension width suffixWidth schedulerDepth groupBitWidth orderWidth scatterDepth gatherDepth : ℕ) : ℕ

Every non-resource contribution in the concrete finite construction.

Equations

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

@[reducible]

noncomputable def Algebraic.MassProduction.CompositionBound.costBound (totalRequests groups prefixWidth dimension width suffixWidth schedulerDepth groupBitWidth orderWidth scatterDepth gatherDepth resourceBound : ℕ) : ℕ

Finite form of the master ledger: resource count times a uniform shorter resource bound, plus the fully explicit overhead.

Equations

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

theorem Algebraic.MassProduction.CompositionBound.circuit_cost_le {width dimension groups totalRequests scatterPaddingCount scatterDepth gatherPaddingCount gatherDepth prefixWidth : ℕ} (widthPositive : 0 < width) (gridPositive : 0 < CanonicalPacking.gridWidth dimension width) (groupsPositive : 0 < groups) (schedulerDepth suffixWidth groupBitWidth orderWidth : ℕ) (allFit : GroupedScheduler.requestGroupSize totalRequests groups * LineEnumeration.nonzeroScalarCount width ≤ Sorting.networkRecords schedulerDepth) (incidenceFits : totalRequests * LineEnumeration.nonzeroScalarCount width ≤ 2 ^ orderWidth) (dummyTarget : Fin dimension → BinaryExtension width) (scatterRecordCount : totalRequests * LineEnumeration.nonzeroScalarCount width + 2 ^ (groupBitWidth + dimension * width) + scatterPaddingCount = Sorting.networkRecords scatterDepth) (resourceCircuits : Fin (ResourceEvaluation.resourceBitCount dimension width) → Circuit DeMorgan.signature (groups * suffixWidth) groups) (resourceBound : ℕ) (resourcesBounded : ∀ (member : Fin (ResourceEvaluation.resourceBitCount dimension width)), (resourceCircuits member).cost DeMorgan.standardCost ≤ resourceBound) (gatherRecordCount : 2 ^ (groupBitWidth + dimension * width) + totalRequests * LineEnumeration.nonzeroScalarCount width + gatherPaddingCount = Sorting.networkRecords gatherDepth) : (RuntimePipeline.circuit prefixWidth widthPositive gridPositive groupsPositive schedulerDepth suffixWidth groupBitWidth orderWidth allFit incidenceFits dummyTarget scatterRecordCount resourceCircuits gatherRecordCount).cost DeMorgan.standardCost ≤ costBound totalRequests groups prefixWidth dimension width suffixWidth schedulerDepth groupBitWidth orderWidth scatterDepth gatherDepth resourceBound

Concrete natural-number composition bound for the runtime circuit.

theorem Algebraic.MassProduction.CompositionBound.booleanMassComplexity_le {width dimension groups prefixWidth totalRequests scatterPaddingCount scatterDepth gatherPaddingCount gatherDepth : ℕ} (widthPositive : 0 < width) (widthAtLeastTwo : 2 ≤ width) (dimensionPositive : 0 < dimension) (gridPositive : 0 < CanonicalPacking.gridWidth dimension width) (groupsPositive : 0 < groups) (packingFits : 2 ^ prefixWidth ≤ CanonicalPacking.gridWidth dimension width ^ dimension * width) (schedulerDepth suffixWidth groupBitWidth orderWidth : ℕ) (groupFits : groups ≤ 2 ^ groupBitWidth) (allFit : GroupedScheduler.requestGroupSize totalRequests groups * LineEnumeration.nonzeroScalarCount width ≤ Sorting.networkRecords schedulerDepth) (directionCapacity : GroupedScheduler.requestGroupSize totalRequests groups * LineEnumeration.nonzeroScalarCount width < Nat.card (Projectivization (BinaryExtension width) (Fin dimension → BinaryExtension width))) (incidenceFits : totalRequests * LineEnumeration.nonzeroScalarCount width ≤ 2 ^ orderWidth) (function : Fin (2 ^ prefixWidth) → (Fin suffixWidth → Bool) → Bool) (dummyTarget : Fin dimension → BinaryExtension width) (scatterRecordCount : totalRequests * LineEnumeration.nonzeroScalarCount width + 2 ^ (groupBitWidth + dimension * width) + scatterPaddingCount = Sorting.networkRecords scatterDepth) (resourceCircuits : Fin (ResourceEvaluation.resourceBitCount dimension width) → Circuit DeMorgan.signature (groups * suffixWidth) groups) (resourcesCompute : ∀ (point : Fin (ResourceEvaluation.pointCount dimension width)) (bit : Fin width), (resourceCircuits (ResourceEvaluation.resourceMemberIndex point bit)).ComputesWith DeMorgan.interpretation (directProduct (ResourceEvaluation.packedResourceFunction widthPositive (CanonicalPacking.packedPlacement widthPositive packingFits) function point bit) groups)) (resourceBound : ℕ) (resourcesBounded : ∀ (member : Fin (ResourceEvaluation.resourceBitCount dimension width)), (resourceCircuits member).cost DeMorgan.standardCost ≤ resourceBound) (gatherRecordCount : 2 ^ (groupBitWidth + dimension * width) + totalRequests * LineEnumeration.nonzeroScalarCount width + gatherPaddingCount = Sorting.networkRecords gatherDepth) : booleanMassComplexity (RuntimePipeline.requestFunction function) totalRequests ≤ ↑(costBound totalRequests groups prefixWidth dimension width suffixWidth schedulerDepth groupBitWidth orderWidth scatterDepth gatherDepth resourceBound)

Complexity-theoretic form of the finite composition proposition. The left side is the minimum circuit cost of the ordinary runtime direct product; the right side is resource count times the supplied shorter bound plus the explicit overhead.

noncomputable def Algebraic.MassProduction.CompositionBound.canonicalResourceFunction {width prefixWidth dimension suffixWidth : ℕ} (widthPositive : 0 < width) (packingFits : 2 ^ prefixWidth ≤ CanonicalPacking.gridWidth dimension width ^ dimension * width) (function : Fin (2 ^ prefixWidth) → (Fin suffixWidth → Bool) → Bool) (member : Fin (ResourceEvaluation.resourceBitCount dimension width)) : ScalarFunction Bool suffixWidth

Canonically indexed shorter resource function used by the runtime composition.

Equations

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

@[simp]

theorem Algebraic.MassProduction.CompositionBound.canonicalResourceFunction_index {width prefixWidth dimension suffixWidth : ℕ} (widthPositive : 0 < width) (packingFits : 2 ^ prefixWidth ≤ CanonicalPacking.gridWidth dimension width ^ dimension * width) (function : Fin (2 ^ prefixWidth) → (Fin suffixWidth → Bool) → Bool) (point : Fin (ResourceEvaluation.pointCount dimension width)) (bit : Fin width) : canonicalResourceFunction widthPositive packingFits function (ResourceEvaluation.resourceMemberIndex point bit) = ResourceEvaluation.packedResourceFunction widthPositive (CanonicalPacking.packedPlacement widthPositive packingFits) function point bit

theorem Algebraic.MassProduction.CompositionBound.booleanMassComplexity_le_of_resource_complexity {width dimension groups prefixWidth totalRequests scatterPaddingCount scatterDepth gatherPaddingCount gatherDepth : ℕ} (widthPositive : 0 < width) (widthAtLeastTwo : 2 ≤ width) (dimensionPositive : 0 < dimension) (gridPositive : 0 < CanonicalPacking.gridWidth dimension width) (groupsPositive : 0 < groups) (packingFits : 2 ^ prefixWidth ≤ CanonicalPacking.gridWidth dimension width ^ dimension * width) (schedulerDepth suffixWidth groupBitWidth orderWidth : ℕ) (suffixLarge : 16 ≤ suffixWidth) (groupFits : groups ≤ 2 ^ groupBitWidth) (allFit : GroupedScheduler.requestGroupSize totalRequests groups * LineEnumeration.nonzeroScalarCount width ≤ Sorting.networkRecords schedulerDepth) (directionCapacity : GroupedScheduler.requestGroupSize totalRequests groups * LineEnumeration.nonzeroScalarCount width < Nat.card (Projectivization (BinaryExtension width) (Fin dimension → BinaryExtension width))) (incidenceFits : totalRequests * LineEnumeration.nonzeroScalarCount width ≤ 2 ^ orderWidth) (function : Fin (2 ^ prefixWidth) → (Fin suffixWidth → Bool) → Bool) (dummyTarget : Fin dimension → BinaryExtension width) (scatterRecordCount : totalRequests * LineEnumeration.nonzeroScalarCount width + 2 ^ (groupBitWidth + dimension * width) + scatterPaddingCount = Sorting.networkRecords scatterDepth) (resourceBound : ℕ) (resourceComplexity : ∀ (member : Fin (ResourceEvaluation.resourceBitCount dimension width)), booleanMassComplexity (canonicalResourceFunction widthPositive packingFits function member) groups ≤ ↑resourceBound) (gatherRecordCount : 2 ^ (groupBitWidth + dimension * width) + totalRequests * LineEnumeration.nonzeroScalarCount width + gatherPaddingCount = Sorting.networkRecords gatherDepth) : booleanMassComplexity (RuntimePipeline.requestFunction function) totalRequests ≤ ↑(costBound totalRequests groups prefixWidth dimension width suffixWidth schedulerDepth groupBitWidth orderWidth scatterDepth gatherDepth resourceBound)

Complexity-only interface to the finite composition theorem. Shannon replication witnesses that every shorter direct product is realizable; a minimum circuit is then selected for each resource. Consequently callers only need to supply a uniform complexity bound, rather than a dependent family of concrete circuits.