Canonical finite parameters for mass-production composition

The raw composition theorem exposes every routing width, sorting-network depth, and padding count. This module chooses each of those bookkeeping parameters canonically by ceiling binary logarithms. The only hypotheses left to later asymptotic work are the mathematical ones: packing into the evaluation-code grid and availability of enough projective directions.

No instances are declared here.

def Algebraic.MassProduction.FiniteParameters.binaryDepth (records : ℕ) : ℕ

Depth of the least power-of-two layout large enough for records.

Equations

• Algebraic.MassProduction.FiniteParameters.binaryDepth records = Nat.clog 2 records

theorem Algebraic.MassProduction.FiniteParameters.records_le_networkRecords (records : ℕ) : records ≤ Sorting.networkRecords (binaryDepth records)

def Algebraic.MassProduction.FiniteParameters.paddingCount (records : ℕ) : ℕ

Canonical padding from a live prefix to the next power-of-two layout.

Equations

• Algebraic.MassProduction.FiniteParameters.paddingCount records = Algebraic.MassProduction.Sorting.networkRecords (Algebraic.MassProduction.FiniteParameters.binaryDepth records) - records

theorem Algebraic.MassProduction.FiniteParameters.records_add_paddingCount (records : ℕ) : records + paddingCount records = Sorting.networkRecords (binaryDepth records)

theorem Algebraic.MassProduction.FiniteParameters.networkRecords_binaryDepth_lt_two_mul (records : ℕ) (recordsPositive : 0 < records) : Sorting.networkRecords (binaryDepth records) < 2 * records

The least power-of-two layout wastes less than a factor of two when the live record count is positive.

theorem Algebraic.MassProduction.FiniteParameters.binaryDepth_le (records bound : ℕ) (fits : records ≤ 2 ^ bound) : binaryDepth records ≤ bound

def Algebraic.MassProduction.FiniteParameters.groupBitWidth (groups : ℕ) : ℕ

Bit width used for a group index.

Equations

• Algebraic.MassProduction.FiniteParameters.groupBitWidth groups = Algebraic.MassProduction.FiniteParameters.binaryDepth groups

theorem Algebraic.MassProduction.FiniteParameters.groups_fit (groups : ℕ) : groups ≤ 2 ^ groupBitWidth groups

noncomputable def Algebraic.MassProduction.FiniteParameters.incidenceCount (totalRequests width : ℕ) : ℕ

Number of scheduled non-target incidences.

Equations

• Algebraic.MassProduction.FiniteParameters.incidenceCount totalRequests width = totalRequests * Algebraic.MassProduction.LineEnumeration.nonzeroScalarCount width

noncomputable def Algebraic.MassProduction.FiniteParameters.schedulerDepth (totalRequests groups width : ℕ) : ℕ

Sorting depth sufficient for one group's greedy scheduler state.

Equations

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

theorem Algebraic.MassProduction.FiniteParameters.scheduler_fits (totalRequests groups width : ℕ) : GroupedScheduler.requestGroupSize totalRequests groups * LineEnumeration.nonzeroScalarCount width ≤ Sorting.networkRecords (schedulerDepth totalRequests groups width)

noncomputable def Algebraic.MassProduction.FiniteParameters.orderWidth (totalRequests width : ℕ) : ℕ

Bit width sufficient to retain the original incidence order.

Equations

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

theorem Algebraic.MassProduction.FiniteParameters.incidences_fit (totalRequests width : ℕ) : incidenceCount totalRequests width ≤ 2 ^ orderWidth totalRequests width

def Algebraic.MassProduction.FiniteParameters.resourceSlotCount (groups dimension width : ℕ) : ℕ

Number of canonical (group, affine point) resource slots.

Equations

• Algebraic.MassProduction.FiniteParameters.resourceSlotCount groups dimension width = 2 ^ (Algebraic.MassProduction.FiniteParameters.groupBitWidth groups + dimension * width)

noncomputable def Algebraic.MassProduction.FiniteParameters.routingRecords (totalRequests groups dimension width : ℕ) : ℕ

Live record count shared by scatter and gather.

Equations

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

noncomputable def Algebraic.MassProduction.FiniteParameters.routingDepth (totalRequests groups dimension width : ℕ) : ℕ

Common power-of-two sorting depth for scatter and gather.

Equations

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

noncomputable def Algebraic.MassProduction.FiniteParameters.routingPadding (totalRequests groups dimension width : ℕ) : ℕ

Padding count for either routing pass.

Equations

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

theorem Algebraic.MassProduction.FiniteParameters.scatter_record_count (totalRequests groups dimension width : ℕ) : incidenceCount totalRequests width + resourceSlotCount groups dimension width + routingPadding totalRequests groups dimension width = Sorting.networkRecords (routingDepth totalRequests groups dimension width)

theorem Algebraic.MassProduction.FiniteParameters.gather_record_count (totalRequests groups dimension width : ℕ) : resourceSlotCount groups dimension width + incidenceCount totalRequests width + routingPadding totalRequests groups dimension width = Sorting.networkRecords (routingDepth totalRequests groups dimension width)

@[reducible]

noncomputable def Algebraic.MassProduction.FiniteParameters.canonicalCostBound (totalRequests groups prefixWidth dimension width suffixWidth resourceBound : ℕ) : ℕ

The fully instantiated finite bound.

Equations

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

theorem Algebraic.MassProduction.FiniteParameters.booleanMassComplexity_le (totalRequests groups prefixWidth dimension width suffixWidth : ℕ) (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) (suffixLarge : 16 ≤ suffixWidth) (directionCapacity : GroupedScheduler.requestGroupSize totalRequests groups * LineEnumeration.nonzeroScalarCount width < Nat.card (Projectivization (BinaryExtension width) (Fin dimension → BinaryExtension width))) (function : Fin (2 ^ prefixWidth) → (Fin suffixWidth → Bool) → Bool) (resourceBound : ℕ) (resourceComplexity : ∀ (member : Fin (ResourceEvaluation.resourceBitCount dimension width)), booleanMassComplexity (CompositionBound.canonicalResourceFunction widthPositive packingFits function member) groups ≤ ↑resourceBound) : booleanMassComplexity (RuntimePipeline.requestFunction function) totalRequests ≤ ↑(canonicalCostBound totalRequests groups prefixWidth dimension width suffixWidth resourceBound)

Canonically parameterized complexity-only composition theorem.