Quantitative storage and key widths for the chosen high-rate code

These inequalities retain the rate-one factor and charge at most one whole codeword for rounding. They concern exact integer counts and are ready for eventual parameter estimates.

theorem Algebraic.MassProduction.Nonuniform.FiniteBound.alphabetPower_eq (dimension blockWidth blocks : ℕ) : (2 ^ (blockWidth * dimension)) ^ blocks = 2 ^ (dimension * (blockWidth * blocks))

The digit alphabet table is exactly the affine point space.

theorem Algebraic.MassProduction.Nonuniform.FiniteBound.resourceCount_le_rate {blocks precision blockWidth dimension prefixWidth : ℕ} (blocksPositive : 0 < blocks) (blocksLarge : precision * (2 ^ (blockWidth * dimension) - 1) ≤ blocks) : precision * HighRate.ResourceLayout.count (copies prefixWidth dimension blockWidth blocks) dimension (blockWidth * blocks) ≤ (precision + 1) * 2 ^ prefixWidth + precision * (2 ^ (dimension * (blockWidth * blocks)) * (blockWidth * blocks))

Rate-one storage bound including the one-codeword rounding term.

theorem Algebraic.MassProduction.Nonuniform.FiniteBound.resourceCount_le_nearOne {blocks precision blockWidth dimension prefixWidth : ℕ} (blocksPositive : 0 < blocks) (blocksLarge : precision * (2 ^ (blockWidth * dimension) - 1) ≤ blocks) (roundingSmall : precision * (2 ^ (dimension * (blockWidth * blocks)) * (blockWidth * blocks)) ≤ 2 ^ prefixWidth) : precision * HighRate.ResourceLayout.count (copies prefixWidth dimension blockWidth blocks) dimension (blockWidth * blocks) ≤ (precision + 2) * 2 ^ prefixWidth

If one codeword is negligible at the selected precision, the complete bank has expansion at most (precision+2)/precision.

theorem Algebraic.MassProduction.Nonuniform.FiniteBound.copies_bitWidth_le (prefixWidth dimension blockWidth blocks : ℕ) : FiniteParameters.binaryDepth (copies prefixWidth dimension blockWidth blocks) ≤ prefixWidth + 1

Copy-index keys use at most one bit more than the source prefix.

theorem Algebraic.MassProduction.Nonuniform.FiniteBound.selector_bitWidth_le (width : ℕ) : FiniteParameters.binaryDepth width ≤ width

A field-basis selector fits in at most the field symbol's bit width.