Finite evaluation-code parameter selection

The field width must satisfy two competing requirements. Its interpolation grid must hold all 2^prefixWidth prefix bits, while the number of resource bits must remain within a dimension-dependent constant factor of that same quantity. Choosing a merely convenient large field would lose a factor of prefixWidth and therefore destroy the final 2^n / n bound.

We consequently choose the least field width above a fixed safe floor which satisfies the exact packing inequality. This is nonuniform parameter selection, not a run-time computation, and introduces no instances.

def Algebraic.MassProduction.CodeParameters.baseWidth (dimension : ℕ) : ℕ

A safe dimension-dependent floor for the binary-extension width.

Equations

• Algebraic.MassProduction.CodeParameters.baseWidth dimension = 2 * dimension + 2

def Algebraic.MassProduction.CodeParameters.candidateWidth (prefixWidth dimension : ℕ) : ℕ

A coarse explicit candidate used only to prove that minimal parameter selection is nonempty.

Equations

• Algebraic.MassProduction.CodeParameters.candidateWidth prefixWidth dimension = prefixWidth ⌈/⌉ dimension + 4 * dimension + 2

def Algebraic.MassProduction.CodeParameters.Admissible (prefixWidth dimension width : ℕ) : Prop

Exact admissibility predicate for a binary-extension width.

Equations

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

theorem Algebraic.MassProduction.CodeParameters.candidate_admissible (prefixWidth dimension : ℕ) (dimensionPositive : 0 < dimension) : Admissible prefixWidth dimension (candidateWidth prefixWidth dimension)

noncomputable def Algebraic.MassProduction.CodeParameters.fieldWidth (prefixWidth dimension : ℕ) (dimensionPositive : 0 < dimension) : ℕ

Least admissible binary-extension width above baseWidth.

Equations

• Algebraic.MassProduction.CodeParameters.fieldWidth prefixWidth dimension dimensionPositive = Nat.find ⋯

theorem Algebraic.MassProduction.CodeParameters.fieldWidth_admissible (prefixWidth dimension : ℕ) (dimensionPositive : 0 < dimension) : Admissible prefixWidth dimension (fieldWidth prefixWidth dimension dimensionPositive)

theorem Algebraic.MassProduction.CodeParameters.baseWidth_le_fieldWidth (prefixWidth dimension : ℕ) (dimensionPositive : 0 < dimension) : baseWidth dimension ≤ fieldWidth prefixWidth dimension dimensionPositive

theorem Algebraic.MassProduction.CodeParameters.fieldWidth_packingFits (prefixWidth dimension : ℕ) (dimensionPositive : 0 < dimension) : 2 ^ prefixWidth ≤ CanonicalPacking.gridWidth dimension (fieldWidth prefixWidth dimension dimensionPositive) ^ dimension * fieldWidth prefixWidth dimension dimensionPositive

theorem Algebraic.MassProduction.CodeParameters.fieldWidth_le_candidate (prefixWidth dimension : ℕ) (dimensionPositive : 0 < dimension) : fieldWidth prefixWidth dimension dimensionPositive ≤ candidateWidth prefixWidth dimension

theorem Algebraic.MassProduction.CodeParameters.ceilDiv_le_div_add_one (value divisor : ℕ) (divisorPositive : 0 < divisor) : value ⌈/⌉ divisor ≤ value / divisor + 1

Ceiling division differs from ordinary natural division by at most one.

theorem Algebraic.MassProduction.CodeParameters.fieldWidth_le_quotient_add (prefixWidth dimension : ℕ) (dimensionPositive : 0 < dimension) : fieldWidth prefixWidth dimension dimensionPositive ≤ prefixWidth / dimension + (4 * dimension + 3)

A division-based upper bound on the least admissible field width.

theorem Algebraic.MassProduction.CodeParameters.fieldCard_le (prefixWidth dimension : ℕ) (dimensionPositive : 0 < dimension) : 2 ^ fieldWidth prefixWidth dimension dimensionPositive ≤ 2 ^ (4 * dimension + 3) * 2 ^ (prefixWidth / dimension)

The selected field cardinality is a fixed dimension-dependent factor times the ideal 2^(prefixWidth / dimension) rate.

theorem Algebraic.MassProduction.CodeParameters.fieldCard_pow_dimension_le (prefixWidth dimension : ℕ) (dimensionPositive : 0 < dimension) : 2 ^ (dimension * fieldWidth prefixWidth dimension dimensionPositive) ≤ 2 ^ (dimension * (4 * dimension + 3)) * 2 ^ prefixWidth

Raising the selected field cardinality to the fixed code dimension costs only a fixed factor beyond the prefix truth-table size.

theorem Algebraic.MassProduction.CodeParameters.fieldWidth_minimal (prefixWidth dimension : ℕ) (dimensionPositive : 0 < dimension) {width : ℕ} (smaller : width < fieldWidth prefixWidth dimension dimensionPositive) : ¬Admissible prefixWidth dimension width

theorem Algebraic.MassProduction.CodeParameters.fieldWidth_atLeastTwo (prefixWidth dimension : ℕ) (dimensionPositive : 0 < dimension) : 2 ≤ fieldWidth prefixWidth dimension dimensionPositive

theorem Algebraic.MassProduction.CodeParameters.fieldWidth_positive (prefixWidth dimension : ℕ) (dimensionPositive : 0 < dimension) : 0 < fieldWidth prefixWidth dimension dimensionPositive

theorem Algebraic.MassProduction.CodeParameters.fieldWidth_gridPositive (prefixWidth dimension : ℕ) (dimensionPositive : 0 < dimension) : 0 < CanonicalPacking.gridWidth dimension (fieldWidth prefixWidth dimension dimensionPositive)

theorem Algebraic.MassProduction.CodeParameters.prefixWidth_le_succ_dimension_mul_fieldWidth (prefixWidth dimension : ℕ) (dimensionPositive : 0 < dimension) : prefixWidth ≤ (dimension + 1) * fieldWidth prefixWidth dimension dimensionPositive

Packing forces the selected field width to carry at least the prefix information rate. The extra + 1 accounts for the basis-bit coordinate in the packed grid.

Minimality preserves the code rate

def Algebraic.MassProduction.CodeParameters.resourceConstant (dimension : ℕ) : ℕ

Dimension-dependent constant in the resource-count estimate.

Equations

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

theorem Algebraic.MassProduction.CodeParameters.resourceBitCount_le (prefixWidth dimension : ℕ) (dimensionPositive : 0 < dimension) : ResourceEvaluation.resourceBitCount dimension (fieldWidth prefixWidth dimension dimensionPositive) ≤ resourceConstant dimension * 2 ^ prefixWidth

Minimal field selection keeps the exact number of (point, bit) resources within a fixed dimension-dependent factor of 2^prefixWidth.

Projective-direction capacity and finite composition

theorem Algebraic.MassProduction.CodeParameters.projectiveDirections_lower (dimension width : ℕ) (dimensionPositive : 0 < dimension) (widthPositive : 0 < width) : 2 ^ (width * (dimension - 1)) ≤ Nat.card (Projectivization (BinaryExtension width) (Fin dimension → BinaryExtension width))

The projective direction space contains at least the top term of its geometric cardinality sum.

theorem Algebraic.MassProduction.CodeParameters.directionCapacity_of_load (totalRequests groups dimension width : ℕ) (dimensionPositive : 0 < dimension) (widthPositive : 0 < width) (loadBound : GroupedScheduler.requestGroupSize totalRequests groups * 2 ^ width < 2 ^ (width * (dimension - 1))) : GroupedScheduler.requestGroupSize totalRequests groups * LineEnumeration.nonzeroScalarCount width < Nat.card (Projectivization (BinaryExtension width) (Fin dimension → BinaryExtension width))

A simple exponential load inequality implies the exact scheduler direction-capacity hypothesis.

theorem Algebraic.MassProduction.CodeParameters.booleanMassComplexity_le (totalRequests groups prefixWidth dimension suffixWidth : ℕ) (dimensionAtLeastTwo : 2 ≤ dimension) (groupsPositive : 0 < groups) (suffixLarge : 16 ≤ suffixWidth) (loadBound : GroupedScheduler.requestGroupSize totalRequests groups * 2 ^ fieldWidth prefixWidth dimension ⋯ < 2 ^ (fieldWidth prefixWidth dimension ⋯ * (dimension - 1))) (function : Fin (2 ^ prefixWidth) → (Fin suffixWidth → Bool) → Bool) (resourceBound : ℕ) (resourceComplexity : ∀ (member : Fin (ResourceEvaluation.resourceBitCount dimension (fieldWidth prefixWidth dimension ⋯))), booleanMassComplexity (CompositionBound.canonicalResourceFunction ⋯ ⋯ function member) groups ≤ ↑resourceBound) : booleanMassComplexity (RuntimePipeline.requestFunction function) totalRequests ≤ ↑(FiniteParameters.canonicalCostBound totalRequests groups prefixWidth dimension (fieldWidth prefixWidth dimension ⋯) suffixWidth resourceBound)

Composition with the least admissible field width and canonical routing bookkeeping.