Parameters for fine mass production

Fix a rational copy exponent γ = num / den < 1 and a slack X. Inputs of length n are split into a prefix of prefixWidth n ≈ (γ + (1 - γ) / (X + 1)) n bits and a suffix of the remaining suffixWidth n ≥ (X / (X + 1)) (1 - γ) n bits (mul_le_suffixWidth). The prefix is encoded in line-parity codes on K ^ dimension over a field of 2 ^ fieldWidth n elements, where fieldWidth n is a multiple of blockWidth and dimension ≤ 2 ^ blockWidth. Batches have 2 ^ depth n requests, where depth n = ⌊γ n⌋ + 1.

The dimension is large enough that (dimension - 2) * fieldWidth n eventually exceeds depth n by any fixed amount (eventually_add_depth_le): this is the projective-direction budget of the scheduler. The field width leaves 3 log₂ (n + 2) prefix bits unused (dimension_mul_fieldWidth_le), so a single code copy is negligible against 2 ^ prefixWidth n.

Main definitions

• Cslib.Circuits.Boolean.MassProduction.Fine.prefixWidth, Cslib.Circuits.Boolean.MassProduction.Fine.suffixWidth: the input split.
• Cslib.Circuits.Boolean.MassProduction.Fine.dimension, Cslib.Circuits.Boolean.MassProduction.Fine.blockWidth, Cslib.Circuits.Boolean.MassProduction.Fine.blocks, Cslib.Circuits.Boolean.MassProduction.Fine.fieldWidth: the code geometry.
• Cslib.Circuits.Boolean.MassProduction.Fine.depth: the batch exponent.

References

• Simplifies MassProduction/Nonuniform/{GeometricSlopes,BlockParameters, CoefficientParameters}.lean in S. Schlesinger, Boolean circuit mass production formalization.

def Cslib.Circuits.Boolean.MassProduction.Fine.prefixWidth (num den X n : ℕ) : ℕ

The prefix width ⌊n (den + num X) / ((X + 1) den)⌋.

def Cslib.Circuits.Boolean.MassProduction.Fine.suffixWidth (num den X n : ℕ) : ℕ

The suffix width, the rest of the input.

def Cslib.Circuits.Boolean.MassProduction.Fine.dimension (num den X : ℕ) : ℕ

The dimension of the code geometry.

def Cslib.Circuits.Boolean.MassProduction.Fine.blockWidth (num den X : ℕ) : ℕ

The block width of the field exponent: dimension ≤ 2 ^ blockWidth.

def Cslib.Circuits.Boolean.MassProduction.Fine.blocks (num den X n : ℕ) : ℕ

The number of blocks of the field exponent.

def Cslib.Circuits.Boolean.MassProduction.Fine.fieldWidth (num den X n : ℕ) : ℕ

The field has 2 ^ fieldWidth n elements.

def Cslib.Circuits.Boolean.MassProduction.Fine.depth (num den n : ℕ) : ℕ

Batches have 2 ^ depth n requests.

theorem Cslib.Circuits.Boolean.MassProduction.Fine.prefixWidth_le {num den X : ℕ} (hnd : num ≤ den) (n : ℕ) : prefixWidth num den X n ≤ n

theorem Cslib.Circuits.Boolean.MassProduction.Fine.prefixWidth_add_suffixWidth {num den X : ℕ} (hnd : num ≤ den) (n : ℕ) : prefixWidth num den X n + suffixWidth num den X n = n

theorem Cslib.Circuits.Boolean.MassProduction.Fine.mul_le_suffixWidth {num den X : ℕ} (hnd : num ≤ den) (n : ℕ) : X * (den - num) * n ≤ (X + 1) * den * suffixWidth num den X n

The suffix keeps at least a X / (X + 1) fraction of (1 - γ) n bits.

theorem Cslib.Circuits.Boolean.MassProduction.Fine.three_le_dimension {num den X : ℕ} : 3 ≤ dimension num den X

theorem Cslib.Circuits.Boolean.MassProduction.Fine.dimension_le_two_pow_blockWidth {num den X : ℕ} : dimension num den X ≤ 2 ^ blockWidth num den X

theorem Cslib.Circuits.Boolean.MassProduction.Fine.blockWidth_pos {num den X : ℕ} : 0 < blockWidth num den X

theorem Cslib.Circuits.Boolean.MassProduction.Fine.dimension_mul_fieldWidth_le {num den X : ℕ} (n : ℕ) : dimension num den X * fieldWidth num den X n + 3 * Nat.log 2 (n + 2) ≤ prefixWidth num den X n ∨ fieldWidth num den X n = 0

The code points use all but 3 log₂ (n + 2) of the prefix bits.

theorem Cslib.Circuits.Boolean.MassProduction.Fine.eventually_add_mul_log_le (A B : ℕ) : ∀ᶠ (n : ℕ) in Filter.atTop, A + B * Nat.log 2 (n + 2) ≤ n

Linear growth eventually dominates any affine function of log₂ (n + 2).

theorem Cslib.Circuits.Boolean.MassProduction.Fine.eventually_add_depth_le {num den X : ℕ} (hnd : num < den) (c : ℕ) : ∀ᶠ (n : ℕ) in Filter.atTop, c + depth num den n ≤ (dimension num den X - 2) * fieldWidth num den X n

The scheduler budget: (dimension - 2) * fieldWidth n eventually exceeds depth n by any fixed amount.

theorem Cslib.Circuits.Boolean.MassProduction.Fine.lt_mul_prefixWidth_add_one {num den X : ℕ} (hden : 0 < den) (n : ℕ) : n < (X + 1) * (prefixWidth num den X n + 1)

The prefix grows at least linearly: n < (X + 1) * (prefixWidth n + 1).

theorem Cslib.Circuits.Boolean.MassProduction.Fine.eventually_le_blocks {num den X : ℕ} (hden : 0 < den) (c : ℕ) : ∀ᶠ (n : ℕ) in Filter.atTop, c ≤ blocks num den X n

Eventually the field exponent has at least c blocks.

theorem Cslib.Circuits.Boolean.MassProduction.Fine.eventually_le_suffixWidth {num den X : ℕ} (hnd : num < den) (hX : 0 < X) (c : ℕ) : ∀ᶠ (n : ℕ) in Filter.atTop, c ≤ suffixWidth num den X n

Eventually the suffix has at least c bits, when the slack is positive.

theorem Cslib.Circuits.Boolean.MassProduction.Fine.two_mul_slack_le (P : ℕ) : 2 * P * ((16 * (P + 1) + 1) ^ 2 * (16 * (P + 1) + 2)) ≤ (2 * P + 1) * (16 * (P + 1)) ^ 3

Slack X = 16 (P + 1) in three factors costs less than 1 / (2 P).

theorem Cslib.Circuits.Boolean.MassProduction.Fine.mul_add_le_of_slack {P n w p den num R L O : ℕ} (hsuffix : 16 * (P + 1) * (den - num) * n ≤ (16 * (P + 1) + 1) * den * w) (hsplit : n = p + w) (hR : 16 * (P + 1) * R ≤ (16 * (P + 1) + 2) * 2 ^ p) (hL : 16 * (P + 1) * w * L ≤ (16 * (P + 1) + 1) * 2 ^ w) (hO : 2 * P * (den - num) * n * O ≤ den * 2 ^ n) : P * (den - num) * n * (R * L + O) ≤ (P + 1) * den * 2 ^ n

The leading-coefficient arithmetic of fine mass production.

theorem Cslib.Circuits.Boolean.MassProduction.Fine.eventually_mul_pow_le_two_pow_div (A E c : ℕ) (hc : 0 < c) : ∀ᶠ (n : ℕ) in Filter.atTop, A * (n + 1) ^ E ≤ 2 ^ (n / c)

Any polynomial is eventually below 2 ^ (n / c).

theorem Cslib.Circuits.Boolean.MassProduction.Fine.eventually_mul_two_pow_dimension_le {num den X : ℕ} (hnd : num ≤ den) (X' : ℕ) : ∀ᶠ (n : ℕ) in Filter.atTop, X' * fieldWidth num den X n * 2 ^ (dimension num den X * fieldWidth num den X n) ≤ 2 ^ prefixWidth num den X n

The last, partly filled code copy is negligible: eventually X' * fieldWidth n * 2 ^ (dimension * fieldWidth n) ≤ 2 ^ prefixWidth n.

theorem Cslib.Circuits.Boolean.MassProduction.Fine.div_le_suffixWidth {num den X : ℕ} (hnd : num < den) (hX : 0 < X) (n : ℕ) : n / ((X + 1) * den) ≤ suffixWidth num den X n

The prefix leaves a linear number of suffix bits: n / ((X + 1) den) ≤ suffixWidth n.

theorem Cslib.Circuits.Boolean.MassProduction.Fine.div_le_sub_depth_add_fieldWidth {num den X : ℕ} (hnd : num < den) (n : ℕ) : n / dimension num den X + depth num den n + fieldWidth num den X n ≤ n + 1

The scheduler exponent leaves a linear number of bits: n / dimension + depth n + fieldWidth n ≤ n + 1.

theorem Cslib.Circuits.Boolean.MassProduction.Fine.eventually_overhead_le {num den X : ℕ} (hnd : num < den) (hX : 0 < X) (P A E : ℕ) : ∀ᶠ (n : ℕ) in Filter.atTop, 2 * P * (den - num) * n * (A * (2 ^ prefixWidth num den X n + 2 ^ (depth num den n + fieldWidth num den X n)) * (n + 1) ^ E) ≤ den * 2 ^ n

The overhead is negligible. For any polynomial factor A (n + 1) ^ E, eventually 2 P (den - num) n · A (2 ^ prefixWidth n + 2 ^ (depth n + fieldWidth n)) (n + 1) ^ E is at most den 2 ^ n.