Kernel-friendly base-39 column construction.

def SumDifferenceExponent.ColumnConstruction.V : Finset ℕ

The twelve base-39 digits whose sums cover a full digit range, with fewer differences.

Equations

• SumDifferenceExponent.ColumnConstruction.V = {0, 1, 3, 4, 8, 9, 10, 11, 14, 17, 18, 19}

def SumDifferenceExponent.ColumnConstruction.VInt : Finset ℤ

The selected base-39 digits viewed as integers.

Equations

• SumDifferenceExponent.ColumnConstruction.VInt = Finset.image (fun (n : ℕ) => ↑n) SumDifferenceExponent.ColumnConstruction.V

def SumDifferenceExponent.ColumnConstruction.VDiff : Finset ℤ

The integer digit differences used to cover differences of columns.

Equations

• SumDifferenceExponent.ColumnConstruction.VDiff = SumDifferenceExponent.ColumnConstruction.VInt - SumDifferenceExponent.ColumnConstruction.VInt

theorem SumDifferenceExponent.ColumnConstruction.V_card_certificate : V.card = 12

theorem SumDifferenceExponent.ColumnConstruction.V_sum_certificate : V + V = Finset.range 39

theorem SumDifferenceExponent.ColumnConstruction.VDiff_card_certificate : VDiff.card = 37

def SumDifferenceExponent.ColumnConstruction.baseValue (b m : ℕ) (w : Fin m → ℕ) : ℕ

Evaluate a fixed-length digit vector in base b, with the least significant digit first.

Equations

• SumDifferenceExponent.ColumnConstruction.baseValue b m w = ∑ i : Fin m, w i * b ^ ↑i

def SumDifferenceExponent.ColumnConstruction.digitSet (b : ℕ) (D : Finset ℕ) (m : ℕ) : Finset ℕ

All base-b values of length m with digits in D.

Equations

• SumDifferenceExponent.ColumnConstruction.digitSet b D m = Finset.image (SumDifferenceExponent.ColumnConstruction.baseValue b m) (Fintype.piFinset fun (x : Fin m) => D)

theorem SumDifferenceExponent.ColumnConstruction.baseValue_eq_ofDigits (b m : ℕ) (w : Fin m → ℕ) : baseValue b m w = Nat.ofDigits b (List.ofFn w)

theorem SumDifferenceExponent.ColumnConstruction.baseValue_injOn {b : ℕ} (hb : 1 < b) {D : Finset ℕ} (hD : ∀ x ∈ D, x < b) (m : ℕ) : Set.InjOn (baseValue b m) ↑(Fintype.piFinset fun (x : Fin m) => D)

theorem SumDifferenceExponent.ColumnConstruction.digitSet_card {b : ℕ} (hb : 1 < b) {D : Finset ℕ} (hD : ∀ x ∈ D, x < b) (m : ℕ) : (digitSet b D m).card = D.card ^ m

theorem SumDifferenceExponent.ColumnConstruction.baseValue_lt_pow {b : ℕ} (hb : 1 < b) {m : ℕ} {w : Fin m → ℕ} (hw : ∀ (i : Fin m), w i < b) : baseValue b m w < b ^ m

def SumDifferenceExponent.ColumnConstruction.allValues (m : ℕ) : Finset ℕ

All length-m base-39 expansions, including leading zeros.

Equations

• SumDifferenceExponent.ColumnConstruction.allValues m = SumDifferenceExponent.ColumnConstruction.digitSet 39 (Finset.range 39) m

theorem SumDifferenceExponent.ColumnConstruction.allValues_eq_range (m : ℕ) : allValues m = Finset.range (39 ^ m)

def SumDifferenceExponent.ColumnConstruction.ZNat (m : ℕ) : Finset ℕ

The sparse columns obtained by restricting base-39 digits to V.

Equations

• SumDifferenceExponent.ColumnConstruction.ZNat m = SumDifferenceExponent.ColumnConstruction.digitSet 39 SumDifferenceExponent.ColumnConstruction.V m

def SumDifferenceExponent.ColumnConstruction.Z (m : ℕ) : Finset ℤ

The sparse column set viewed as integers.

Equations

• SumDifferenceExponent.ColumnConstruction.Z m = Finset.image (fun (n : ℕ) => ↑n) (SumDifferenceExponent.ColumnConstruction.ZNat m)

theorem SumDifferenceExponent.ColumnConstruction.ZNat_card (m : ℕ) : (ZNat m).card = 12 ^ m

theorem SumDifferenceExponent.ColumnConstruction.Z_card (m : ℕ) : (Z m).card = 12 ^ m

theorem SumDifferenceExponent.ColumnConstruction.range_pow_subset_ZNat_add (m : ℕ) : Finset.range (39 ^ m) ⊆ ZNat m + ZNat m

theorem SumDifferenceExponent.ColumnConstruction.cast_range_pow_subset_Z_add (m : ℕ) : Finset.image (fun (n : ℕ) => ↑n) (Finset.range (39 ^ m)) ⊆ Z m + Z m

def SumDifferenceExponent.ColumnConstruction.differenceValue (m : ℕ) (w : Fin m → ℤ) : ℤ

Evaluate an integer digit vector, allowing negative digits, in base 39.

Equations

• SumDifferenceExponent.ColumnConstruction.differenceValue m w = ∑ i : Fin m, w i * 39 ^ ↑i

def SumDifferenceExponent.ColumnConstruction.differenceRepresentations (m : ℕ) : Finset ℤ

A finite cover of column differences by independent digit differences.

Equations

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

theorem SumDifferenceExponent.ColumnConstruction.Z_sub_Z_subset_representations (m : ℕ) : Z m - Z m ⊆ differenceRepresentations m

theorem SumDifferenceExponent.ColumnConstruction.differenceRepresentations_card_le (m : ℕ) : (differenceRepresentations m).card ≤ 37 ^ m

theorem SumDifferenceExponent.ColumnConstruction.Z_sub_Z_card_le (m : ℕ) : (Z m - Z m).card ≤ 37 ^ m

theorem SumDifferenceExponent.ColumnConstruction.mem_ZNat_lt_pow {m z : ℕ} (hz : z ∈ ZNat m) : z < 39 ^ m