Explicit row-column sets and their cardinality estimates.

def SumDifferenceExponent.ColumnConstruction.rowScale (l : ℕ) : ℕ

Scale separating the linear and quadratic parts of a row label.

Equations

• SumDifferenceExponent.ColumnConstruction.rowScale l = 4 * l

def SumDifferenceExponent.ColumnConstruction.rowLabel (l i : ℕ) : ℕ

Quadratic row labels whose cross-row sums identify both contributing rows.

Equations

• SumDifferenceExponent.ColumnConstruction.rowLabel l i = i + SumDifferenceExponent.ColumnConstruction.rowScale l * i ^ 2

def SumDifferenceExponent.ColumnConstruction.rowBase (l : ℕ) : ℕ

A modulus large enough that sums of the relevant row labels do not carry.

Equations

• SumDifferenceExponent.ColumnConstruction.rowBase l = 40 * l ^ 3 + 1

theorem SumDifferenceExponent.ColumnConstruction.index_sum_lt_scale {l i j : ℕ} (hi : i < 2 * l) (hj : j < 2 * l) : i + j < rowScale l

theorem SumDifferenceExponent.ColumnConstruction.rowLabel_mod {l i : ℕ} (hi : i < rowScale l) : rowLabel l i % rowScale l = i

theorem SumDifferenceExponent.ColumnConstruction.rowLabel_sum_mod {l i j : ℕ} (hl : 0 < l) (hi : i < 2 * l) (hj : j < 2 * l) : (rowLabel l i + rowLabel l j) % rowScale l = i + j

theorem SumDifferenceExponent.ColumnConstruction.rowLabel_sum_injective {l i j p q : ℕ} (hl : 0 < l) (hi : i < 2 * l) (hj : j < 2 * l) (hp : p < 2 * l) (hq : q < 2 * l) (hij : i < j) (hpq : p < q) (h : rowLabel l i + rowLabel l j = rowLabel l p + rowLabel l q) : i = p ∧ j = q

theorem SumDifferenceExponent.ColumnConstruction.cross_row_sum_injective (l : ℕ) (hl : 0 < l) : Function.Injective fun (p : Fin l × Fin l) => rowLabel l ↑p.1 + rowLabel l (l + ↑p.2)

theorem SumDifferenceExponent.ColumnConstruction.rowLabel_lt_base {l i : ℕ} (hl : 0 < l) (hi : i < 2 * l) : rowLabel l i < rowBase l

theorem SumDifferenceExponent.ColumnConstruction.rowLabel_sum_lt_base {l i j : ℕ} (hl : 0 < l) (hi : i < 2 * l) (hj : j < 2 * l) : rowLabel l i + rowLabel l j < rowBase l

def SumDifferenceExponent.ColumnConstruction.depth (l : ℕ) : ℕ

The number of base-39 digits needed to make the sparse contributions negligible.

Equations

• SumDifferenceExponent.ColumnConstruction.depth l = 28 * l

def SumDifferenceExponent.ColumnConstruction.columnModulus (l : ℕ) : ℕ

The range length of the full column at the chosen digit depth.

Equations

• SumDifferenceExponent.ColumnConstruction.columnModulus l = 39 ^ SumDifferenceExponent.ColumnConstruction.depth l

theorem SumDifferenceExponent.ColumnConstruction.sparse_difference_negligible (l : ℕ) : 2 * l * 37 ^ depth l ≤ columnModulus l

theorem SumDifferenceExponent.ColumnConstruction.sparse_size_negligible (l : ℕ) : 2 * l * 12 ^ depth l ≤ columnModulus l

def SumDifferenceExponent.ColumnConstruction.fullNat (l : ℕ) : Finset ℕ

The full zero row, containing every column below columnModulus l.

Equations

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

def SumDifferenceExponent.ColumnConstruction.sparseNat (l : ℕ) : Finset ℕ

The 2 * l sparse rows, with columns restricted to the digit set.

Equations

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

def SumDifferenceExponent.ColumnConstruction.ANat (l : ℕ) : Finset ℕ

The union of the full zero row and the sparse rows in the natural numbers.

Equations

• SumDifferenceExponent.ColumnConstruction.ANat l = SumDifferenceExponent.ColumnConstruction.fullNat l ∪ SumDifferenceExponent.ColumnConstruction.sparseNat l

def SumDifferenceExponent.ColumnConstruction.A (l : ℕ) : Finset ℤ

The explicit finite integer set used to approach the optimal exponent.

Equations

• SumDifferenceExponent.ColumnConstruction.A l = Finset.image (fun (n : ℕ) => ↑n) (SumDifferenceExponent.ColumnConstruction.ANat l)

theorem SumDifferenceExponent.ColumnConstruction.fullNat_card (l : ℕ) : (fullNat l).card = columnModulus l

theorem SumDifferenceExponent.ColumnConstruction.sparseNat_card_le (l : ℕ) : (sparseNat l).card ≤ 2 * l * 12 ^ depth l

theorem SumDifferenceExponent.ColumnConstruction.A_card_eq_ANat_card (l : ℕ) : (A l).card = (ANat l).card

theorem SumDifferenceExponent.ColumnConstruction.columnModulus_le_A_card (l : ℕ) : columnModulus l ≤ (A l).card

theorem SumDifferenceExponent.ColumnConstruction.A_card_le_two_mul_modulus (l : ℕ) : (A l).card ≤ 2 * columnModulus l

def SumDifferenceExponent.ColumnConstruction.sumWitnessValue (l : ℕ) (p : (Fin l × Fin l) × Fin (columnModulus l)) : ℕ

Encode two row indices and a column as a sumset witness.

Equations

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

theorem SumDifferenceExponent.ColumnConstruction.sumWitnessValue_injective (l : ℕ) (hl : 0 < l) : Function.Injective (sumWitnessValue l)

def SumDifferenceExponent.ColumnConstruction.sumWitnessSet (l : ℕ) : Finset ℤ

Distinct sums supplied by one row in each half of the row index range.

Equations

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

theorem SumDifferenceExponent.ColumnConstruction.sumWitnessSet_card (l : ℕ) (hl : 0 < l) : (sumWitnessSet l).card = l ^ 2 * columnModulus l

theorem SumDifferenceExponent.ColumnConstruction.sumWitnessSet_subset_add (l : ℕ) : sumWitnessSet l ⊆ A l + A l

theorem SumDifferenceExponent.ColumnConstruction.A_add_A_card_lower (l : ℕ) (hl : 0 < l) : l ^ 2 * columnModulus l ≤ (A l + A l).card

def SumDifferenceExponent.ColumnConstruction.columnInterval (l : ℕ) : Finset ℤ

The symmetric integer interval containing all differences of column indices.

Equations

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

theorem SumDifferenceExponent.ColumnConstruction.columnInterval_card (l : ℕ) : (columnInterval l).card = 2 * columnModulus l - 1

def SumDifferenceExponent.ColumnConstruction.zeroDiffCover (l : ℕ) : Finset ℤ

A cover of differences between two elements of the full zero row.

Equations

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

def SumDifferenceExponent.ColumnConstruction.rightDiffCover (l : ℕ) : Finset ℤ

A cover of differences from a sparse row to the full zero row.

Equations

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

def SumDifferenceExponent.ColumnConstruction.leftDiffCover (l : ℕ) : Finset ℤ

A cover of differences from the full zero row to a sparse row.

Equations

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

def SumDifferenceExponent.ColumnConstruction.sparseDiffCover (l : ℕ) : Finset ℤ

A cover of differences between two sparse rows.

Equations

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

def SumDifferenceExponent.ColumnConstruction.differenceCover (l : ℕ) : Finset ℤ

The four covers for the full/sparse row cases of a difference.

Equations

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

theorem SumDifferenceExponent.ColumnConstruction.nat_difference_mem_columnInterval {l a b : ℕ} (ha : a < columnModulus l) (hb : b < columnModulus l) : ↑a - ↑b ∈ columnInterval l

theorem SumDifferenceExponent.ColumnConstruction.A_sub_A_subset_differenceCover (l : ℕ) : A l - A l ⊆ differenceCover l

theorem SumDifferenceExponent.ColumnConstruction.zeroDiffCover_card_le (l : ℕ) : (zeroDiffCover l).card ≤ 2 * columnModulus l

theorem SumDifferenceExponent.ColumnConstruction.rightDiffCover_card_le (l : ℕ) : (rightDiffCover l).card ≤ 4 * l * columnModulus l

theorem SumDifferenceExponent.ColumnConstruction.leftDiffCover_card_le (l : ℕ) : (leftDiffCover l).card ≤ 4 * l * columnModulus l

theorem SumDifferenceExponent.ColumnConstruction.sparseDiffCover_card_le (l : ℕ) : (sparseDiffCover l).card ≤ 4 * l ^ 2 * 37 ^ depth l

theorem SumDifferenceExponent.ColumnConstruction.A_sub_A_card_upper (l : ℕ) (hl : 0 < l) : (A l - A l).card ≤ 12 * l * columnModulus l