H2 for Thakur's hypotheses on power sums

def ZetaH123.H2.qdigit (q x e : ℕ) : ℕ

The e-th base-q digit of x (returns 0 for positions beyond the representation, matching the convention x_e = 0 for large e).

Equations

• ZetaH123.H2.qdigit q x e = (q.digits x).getD e 0

def ZetaH123.H2.AddNoCarry (q : ℕ) (xs : List ℕ) : Prop

A finite list of nonnegative integers xs adds without carries in base q if at every digit position e the base-q digits sum to at most q - 1. This is exactly the carry-free condition of Definition 2.

Equations

• ZetaH123.H2.AddNoCarry q xs = ∀ (e : ℕ), (List.map (fun (x : ℕ) => ZetaH123.H2.qdigit q x e) xs).sum ≤ q - 1

def ZetaH123.H2.TSet (q d k1 : ℕ) : Set (Fin d → ℕ)

The set T_{d,k1} of d-tuples (encoded as m : Fin d → ℕ) such that each m i is positive, divisible by q - 1, and the list (k1, m_0, …, m_{d-1}) adds without carries in base q. Here k1 plays the role of k - 1.

Equations

• ZetaH123.H2.TSet q d k1 = {m : Fin d → ℕ | (∀ (i : Fin d), 0 < m i) ∧ (∀ (i : Fin d), q - 1 ∣ m i) ∧ ZetaH123.H2.AddNoCarry q (k1 :: List.ofFn m)}

noncomputable def ZetaH123.H2.s (q d k : ℕ) : ℕ

The function s_d(k) = d*k + min over T_{d,k-1}of∑ (i+1) * m i. The minimum over the nonempty set of objective values is realised as the infimum (sInf`) of that set of naturals.

Equations

• ZetaH123.H2.s q d k = d * k + sInf {v : ℕ | ∃ m ∈ ZetaH123.H2.TSet q d (k - 1), v = ∑ i : Fin d, (↑i + 1) * m i}

noncomputable def ZetaH123.H2.F (q d k j : ℕ) : ℕ

The objective F(j) = s_{d-1}(s_1(k) + j) + s_1(k) + j.

Equations

• ZetaH123.H2.F q d k j = ZetaH123.H2.s q (d - 1) (ZetaH123.H2.s q 1 k + j) + ZetaH123.H2.s q 1 k + j

def ZetaH123.H2.Jset (q k : ℕ) : Set ℕ

The admissible set J: nonnegative integers j with (q - 1) ∣ j and q ∤ C(s_1(k) + j - 1, k - 1).

Equations

• ZetaH123.H2.Jset q k = {j : ℕ | q - 1 ∣ j ∧ ¬q ∣ (ZetaH123.H2.s q 1 k + j - 1).choose (k - 1)}

theorem ZetaH123.H2.qdigit_eq (q x e : ℕ) (hq : 2 ≤ q) : qdigit q x e = x / q ^ e % q

The e-th base-q digit equals x / q ^ e % q.

theorem ZetaH123.H2.digit_mod (q a i : ℕ) : a % q ^ i = ∑ e ∈ Finset.range i, a / q ^ e % q * q ^ e

a % q ^ i is the base-q number formed by the first i digits.

theorem ZetaH123.H2.geom_pred (q i : ℕ) (hq : 1 ≤ q) : (q - 1) * ∑ e ∈ Finset.range i, q ^ e = q ^ i - 1

(q - 1) * ∑_{e<i} q ^ e = q ^ i - 1.

theorem ZetaH123.H2.noCarry_mod (q a b i : ℕ) (hq : 1 < q) (h : ∀ e < i, a / q ^ e % q + b / q ^ e % q ≤ q - 1) : a % q ^ i + b % q ^ i < q ^ i

If two numbers add without carry in the first i positions, then their truncations to i digits sum to less than q ^ i.

theorem ZetaH123.H2.not_dvd_choose (q n k : ℕ) (hq : Nat.Prime q) (hkn : k ≤ n) (hcarry : ∀ (i : ℕ), k % q ^ i + (n - k) % q ^ i < q ^ i) : ¬q ∣ n.choose k

Kummer's theorem (one direction): if adding k and n-k produces no carry in any base-q position, then q ∤ C(n,k).

theorem ZetaH123.H2.digit_special (q L e : ℕ) (hq : 2 ≤ q) : (q - 1) * q ^ L / q ^ e % q = if e = L then q - 1 else 0

The e-th digit of (q - 1) * q ^ L: equal to q-1 at position L, else 0.

theorem ZetaH123.H2.main_zero_mem (q : ℕ) (hq : Nat.Prime q) (d k : ℕ) (_hd : 1 < d) (hk : 0 < k) : 0 ∈ Jset q k

0 is admissible: 0 ∈ J. This nontrivial admissibility fact makes the uniqueness-of-minimizer statement meaningful.

theorem ZetaH123.H2.add_mod_eq (q a b i : ℕ) (hq : 1 < q) (h : ∀ e < i, a / q ^ e % q + b / q ^ e % q ≤ q - 1) : (a + b) % q ^ i = a % q ^ i + b % q ^ i

Carry-free addition is digit-additive (fact D2): if at every position the base-q digits of a and b sum to ≤ q-1, then the truncated sums agree.

theorem ZetaH123.H2.qdigit_add (q a b e : ℕ) (hq : 2 ≤ q) (h : ∀ (f : ℕ), a / q ^ f % q + b / q ^ f % q ≤ q - 1) : (a + b) / q ^ e % q = a / q ^ e % q + b / q ^ e % q

Digit additivity (fact D2): if a and b add without carry in every base-q position, then each digit of a + b is the sum of the corresponding digits.

theorem ZetaH123.H2.tset_value_nonempty (q d k : ℕ) (hq : 2 ≤ q) (hk : 0 < k) : {v : ℕ | ∃ m ∈ TSet q d (k - 1), v = ∑ i : Fin d, (↑i + 1) * m i}.Nonempty

The objective value set for TSet q d (k - 1) is nonempty: an explicit witness places each coordinate at a distinct high power (q - 1)·q ^ (k+i), which is positive, divisible by q-1, and carry-free with k-1 (the powers are distinct and exceed log_q (k - 1)). This generalises the Fin 1 nonemptiness in main_zero_mem.

theorem ZetaH123.H2.s_minimizer (q d k : ℕ) (hq : 2 ≤ q) (hk : 0 < k) : ∃ m ∈ TSet q d (k - 1), s q d k = d * k + ∑ i : Fin d, (↑i + 1) * m i

Minimizer extraction: since the objective value set is nonempty, its sInf is attained by some m ∈ TSet q d (k - 1), giving the value identity for s.

theorem ZetaH123.H2.comp_id_le (q : ℕ) (hq : Nat.Prime q) (d k : ℕ) (hd : 1 < d) (hk : 0 < k) : s q d k ≤ s q (d - 1) (s q 1 k) + s q 1 k

Easy direction of the composition identity: s_d(k) ≤ s_{d-1}(s_1(k)) + s_1(k). Constructive: combine a minimizer μ₁ for s_1 (placed at top weight d) with a minimizer of s_{d-1} at argument s_1(k); the combined tuple lies in TSet q d (k - 1).

def ZetaH123.H2.slotList (q k1 L : ℕ) : List ℕ

The list of available base-q digit slots of k1, truncated to positions < L, listed in INCREASING order of value: position e contributes (q - 1) - qdigit q k1 e copies of q ^ e. Sorted ascending since q ^ e is increasing in e.

Equations

• ZetaH123.H2.slotList q k1 L = List.flatMap (fun (e : ℕ) => List.replicate (q - 1 - ZetaH123.H2.qdigit q k1 e) (q ^ e)) (List.range L)

def ZetaH123.H2.blockSum (q k1 L r : ℕ) : ℕ

The sum of the r-th block of n = q-1 smallest slots (1-indexed block r): the slots at list positions [(r-1)*n, r*n).

Equations

• ZetaH123.H2.blockSum q k1 L r = (List.take (q - 1) (List.drop ((r - 1) * (q - 1)) (ZetaH123.H2.slotList q k1 L))).sum

def ZetaH123.H2.Phi (q k1 d L : ℕ) : ℕ

The block functional Φ_d(M) = d·β₁ + (d-1)·β₂ + ⋯ + 1·β_d (β_r = blockSum … r).

Equations

• ZetaH123.H2.Phi q k1 d L = ∑ r ∈ Finset.range d, (d - r) * ZetaH123.H2.blockSum q k1 L (r + 1)

def ZetaH123.H2.slotLen (q d k : ℕ) : ℕ

A truncation length large enough to contain every slot used by any tuple in TSet q d (k - 1) realizing the minimum.

Equations

• ZetaH123.H2.slotLen q d k = if q = q then k + d * (k + 1) + 1 else k + d * (k + 1) + 1

theorem ZetaH123.H2.slotList_prefix (q k1 L₁ L₂ : ℕ) (h : L₁ ≤ L₂) : ∃ (t : List ℕ), slotList q k1 L₂ = slotList q k1 L₁ ++ t

slotList is monotone in the truncation length: a larger L only appends more slots.

theorem ZetaH123.H2.qdigit_zero_of_ge (q k1 e : ℕ) (hq : 2 ≤ q) (he : k1 + 1 ≤ e) : qdigit q k1 e = 0

Digits of k1 beyond position k1 (in fact beyond log_q k1) vanish.

theorem ZetaH123.H2.slotList_length_ge (q k1 L : ℕ) (hq : 2 ≤ q) : (q - 1) * (L - (k1 + 1)) ≤ (slotList q k1 L).length

Lower bound on the length of slotList: positions e ∈ [k1+1, L) each contribute q-1 slots (since the digits of k1 vanish there).

theorem ZetaH123.H2.blockSum_Lindep (q k1 L₁ L₂ r : ℕ) (h : L₁ ≤ L₂) (hr : 1 ≤ r) (hlen : r * (q - 1) ≤ (slotList q k1 L₁).length) : blockSum q k1 L₂ r = blockSum q k1 L₁ r

blockSum is independent of the truncation length once L is large enough to contain the first r blocks.

theorem ZetaH123.H2.Phi_split (q k1 d L : ℕ) (hd : 1 ≤ d) : Phi q k1 d L = d * blockSum q k1 L 1 + ∑ r ∈ Finset.range (d - 1), (d - 1 - r) * blockSum q k1 L (r + 2)

(L3, pure reindexing) Split off the first block of Φ_d: Φ_d(M) = d·β₁ + ∑_{r<d-1} (d-1-r)·β_{r+2}.

theorem ZetaH123.H2.slotList_succ (q k1 Lx : ℕ) : slotList q k1 (Lx + 1) = slotList q k1 Lx ++ List.replicate (q - 1 - qdigit q k1 Lx) (q ^ Lx)

theorem ZetaH123.H2.slotList_length (q k1 Lx : ℕ) : (slotList q k1 Lx).length = ∑ e ∈ Finset.range Lx, (q - 1 - qdigit q k1 e)

theorem ZetaH123.H2.slotList_length_mono (q k1 : ℕ) {a b : ℕ} (h : a ≤ b) : (slotList q k1 a).length ≤ (slotList q k1 b).length

theorem ZetaH123.H2.slotList_sum (q k1 L : ℕ) : (slotList q k1 L).sum = ∑ e ∈ Finset.range L, (q - 1 - qdigit q k1 e) * q ^ e

theorem ZetaH123.H2.slotList_take (q k1 L n : ℕ) : n ≤ (slotList q k1 L).length → ∃ p ≤ L, ∃ (r : ℕ), List.take n (slotList q k1 L) = slotList q k1 p ++ List.replicate r (q ^ p) ∧ (slotList q k1 p).length + r = n ∧ r ≤ q - 1 - qdigit q k1 p

theorem ZetaH123.H2.take_blocks (q k1 L c : ℕ) : (List.take (c * (q - 1)) (slotList q k1 L)).sum = ∑ r ∈ Finset.range c, blockSum q k1 L (r + 1)

theorem ZetaH123.H2.abel_swap (d : ℕ) (b : ℕ → ℕ) : ∑ r ∈ Finset.range d, (d - r) * b (r + 1) = ∑ c ∈ Finset.range d, ∑ r ∈ Finset.range (c + 1), b (r + 1)

theorem ZetaH123.H2.Phi_eq_take_sum (q k1 d L : ℕ) : Phi q k1 d L = ∑ c ∈ Finset.range d, (List.take ((c + 1) * (q - 1)) (slotList q k1 L)).sum

Abel reformulation of Φ_d(M): the layer-cake identity Φ_d(M) = ∑_{c<d} (sum of the smallest (c + 1)·n slots).

theorem ZetaH123.H2.greedy_core (q p L : ℕ) (hq : 2 ≤ q) (hpL : p ≤ L) (b s : ℕ → ℕ) (r : ℕ) (hbs : ∀ e < L, b e ≤ s e) (hcount : ∑ e ∈ Finset.range p, s e + r ≤ ∑ e ∈ Finset.range L, b e) : ∑ e ∈ Finset.range p, s e * q ^ e + r * q ^ p ≤ ∑ e ∈ Finset.range L, b e * q ^ e

theorem ZetaH123.H2.slot_value_le (q d k : ℕ) (hq : 2 ≤ q) (N m : ℕ) (hcarry : ∀ (e : ℕ), qdigit q (k - 1) e + qdigit q N e ≤ q - 1) (hm_len : m ≤ (slotList q (k - 1) (slotLen q d k)).length) (hcount : m ≤ ∑ e ∈ Finset.range (slotLen q d k + N + 1), qdigit q N e) : (List.take m (slotList q (k - 1) (slotLen q d k))).sum ≤ N

Bridge: the value of the smallest m slots of M(k - 1) is at most any N that adds to k-1 without carry and whose total slot count (digit sum) is ≥ m. The greedy/exchange argument in closed arithmetic form.

theorem ZetaH123.H2.qdigit_sum {ι : Type u_1} (q : ℕ) (hq : 2 ≤ q) (I : Finset ι) (f : ι → ℕ) (h : ∀ (e : ℕ), ∑ i ∈ I, qdigit q (f i) e ≤ q - 1) (e : ℕ) : qdigit q (∑ i ∈ I, f i) e = ∑ i ∈ I, qdigit q (f i) e

theorem ZetaH123.H2.sum_pow_modEq (q L : ℕ) (hq : 2 ≤ q) (d : ℕ → ℕ) : ∑ e ∈ Finset.range L, d e * q ^ e ≡ ∑ e ∈ Finset.range L, d e [MOD q - 1]

theorem ZetaH123.H2.digitsum_ge (q x L : ℕ) (hq : 2 ≤ q) (hdvd : q - 1 ∣ x) (hpos : 0 < x) (hxL : x < q ^ L) : q - 1 ≤ ∑ e ∈ Finset.range L, qdigit q x e

theorem ZetaH123.H2.rhs_reindex (d : ℕ) (m : Fin d → ℕ) : ∑ i : Fin d, (↑i + 1) * m i = ∑ c ∈ Finset.range d, ∑ i : Fin d with d - 1 - c ≤ ↑i, m i

theorem ZetaH123.H2.slot_lower_bound (q d k : ℕ) (hq : 2 ≤ q) (hk : 0 < k) (m : Fin d → ℕ) (hm : m ∈ TSet q d (k - 1)) : Phi q (k - 1) d (slotLen q d k) ≤ ∑ i : Fin d, (↑i + 1) * m i

Optimality lower bound (the ≥ half of the slot formula): every tuple in TSet q d (k - 1) has objective at least Φ_d(M) (informal.tex Lem. H2-block-min). Proof idea: reindex the objective by weight levels and bound each level by the greedy bound slot_value_le.

theorem ZetaH123.H2.digit_of_sum_aux (q : ℕ) (hq : 2 ≤ q) (m : ℕ) (coeff : ℕ → ℕ) (hc : ∀ e < m, coeff e < q) (f : ℕ) (hf : f < m) : (∑ e ∈ Finset.range m, coeff e * q ^ e) / q ^ f % q = coeff f

The f-th base-q digit of a bounded expansion ∑_{e<m} coeff e · q ^ e is coeff f.

theorem ZetaH123.H2.sum_lt_pow_aux (q : ℕ) (hq : 2 ≤ q) (m : ℕ) (coeff : ℕ → ℕ) (hc : ∀ e < m, coeff e < q) : ∑ e ∈ Finset.range m, coeff e * q ^ e < q ^ m

theorem ZetaH123.H2.qdigit_le_aux (q k1 e : ℕ) (hq : 2 ≤ q) : qdigit q k1 e ≤ q - 1

theorem ZetaH123.H2.list_map_range_sum (n : ℕ) (g : ℕ → ℕ) : (List.map g (List.range n)).sum = ∑ i ∈ Finset.range n, g i

theorem ZetaH123.H2.wsum_eq (q L : ℕ) (hq : 2 ≤ q) (w : List ℕ) (hpow : ∀ x ∈ w, ∃ e < L, x = q ^ e) : w.sum = ∑ e ∈ Finset.range L, List.count (q ^ e) w * q ^ e

theorem ZetaH123.H2.qdigit_window (q L : ℕ) (hq : 2 ≤ q) (w : List ℕ) (hpow : ∀ x ∈ w, ∃ e < L, x = q ^ e) (hlt : ∀ (e : ℕ), List.count (q ^ e) w < q) (f : ℕ) : qdigit q w.sum f = if f < L then List.count (q ^ f) w else 0

theorem ZetaH123.H2.slotList_pow (q k1 L x : ℕ) : x ∈ slotList q k1 L → ∃ e < L, x = q ^ e

theorem ZetaH123.H2.slotList_count (q k1 L : ℕ) (hq : 2 ≤ q) (e : ℕ) (he : e < L) : List.count (q ^ e) (slotList q k1 L) = q - 1 - qdigit q k1 e

theorem ZetaH123.H2.take_blocks_count {α : Type u_1} [BEq α] (L : List α) (n c : ℕ) (x : α) : ∑ s ∈ Finset.range c, List.count x (List.take n (List.drop (s * n) L)) = List.count x (List.take (c * n) L)

theorem ZetaH123.H2.window_len {α : Type u_1} (L : List α) (a n : ℕ) (h : a + n ≤ L.length) : (List.take n (List.drop a L)).length = n

theorem ZetaH123.H2.pow_sum_modEq (q : ℕ) (hq : 2 ≤ q) (w : List ℕ) (hpow : ∀ x ∈ w, ∃ (e : ℕ), x = q ^ e) : w.sum ≡ w.length [MOD q - 1]

theorem ZetaH123.H2.slot_upper_bound (q d k : ℕ) (hq : 2 ≤ q) (hk : 0 < k) : sInf {v : ℕ | ∃ m ∈ TSet q d (k - 1), v = ∑ i : Fin d, (↑i + 1) * m i} ≤ Phi q (k - 1) d (slotLen q d k)

Optimality upper bound (the ≤ half of the slot formula): the tuple sending the r-th smallest block to the coordinate of weight d-r+1 lies in TSet q d (k - 1) and has objective exactly Φ_d(M).

theorem ZetaH123.H2.slot_formula (q d k : ℕ) (hq : 2 ≤ q) (hk : 0 < k) : s q d k = d * k + Phi q (k - 1) d (slotLen q d k)

The reciprocal slot formula s_d(k) = d·k + Φ_d(M). Assembled by antisymmetry from slot_lower_bound (every value ≥ Φ_d, hence sInf ≥ Φ_d) and slot_upper_bound (sInf ≤ Φ_d).

theorem ZetaH123.H2.s_one_eq (q k : ℕ) (hq : 2 ≤ q) (hk : 0 < k) : s q 1 k = k + blockSum q (k - 1) (slotLen q 1 k) 1

(L1) The d=1 corollary s_1(k) = k + β₁: the slot formula at d=1 gives Φ_1(M) = β₁ (the smallest block sum).

theorem ZetaH123.H2.slotList_drop (q k1 p r : ℕ) (hr : r ≤ q - 1 - qdigit q k1 p) (Lx : ℕ) : List.drop ((slotList q k1 p).length + r) (slotList q k1 Lx) = List.flatMap (fun (e : ℕ) => List.replicate (if e < p then 0 else if e = p then q - 1 - qdigit q k1 p - r else q - 1 - qdigit q k1 e) (q ^ e)) (List.range Lx)

Dropping the first (slotList q k1 p).length + r slots: the result is a flatMap with the slots at positions < p removed, r removed at position p, and all positions > p intact.

theorem ZetaH123.H2.digit_of_sum (q : ℕ) (hq : 2 ≤ q) (m : ℕ) (coeff : ℕ → ℕ) (hc : ∀ e < m, coeff e < q) (f : ℕ) (hf : f < m) : (∑ e ∈ Finset.range m, coeff e * q ^ e) / q ^ f % q = coeff f

theorem ZetaH123.H2.sum_lt_pow (q : ℕ) (hq : 2 ≤ q) (m : ℕ) (coeff : ℕ → ℕ) (hc : ∀ e < m, coeff e < q) : ∑ e ∈ Finset.range m, coeff e * q ^ e < q ^ m

theorem ZetaH123.H2.qdigit_le (q k1 e : ℕ) (hq : 2 ≤ q) : qdigit q k1 e ≤ q - 1

theorem ZetaH123.H2.beta_digit (q k1 p r : ℕ) (hq : 2 ≤ q) (hr : r ≤ q - 1 - qdigit q k1 p) (f : ℕ) : qdigit q ((slotList q k1 p).sum + r * q ^ p) f = if f < p then q - 1 - qdigit q k1 f else if f = p then r else 0

theorem ZetaH123.H2.newmult_eq (q k1 p r : ℕ) (hq : 2 ≤ q) (hr : r ≤ q - 1 - qdigit q k1 p) (e : ℕ) : q - 1 - qdigit q (k1 + ((slotList q k1 p).sum + r * q ^ p)) e = if e < p then 0 else if e = p then q - 1 - qdigit q k1 p - r else q - 1 - qdigit q k1 e

theorem ZetaH123.H2.slot_subtraction (q k1 L₀ : ℕ) (hq : 2 ≤ q) (hβ : q - 1 ≤ (slotList q k1 L₀).length) (Lx : ℕ) : slotList q (k1 + blockSum q k1 L₀ 1) Lx = List.drop (q - 1) (slotList q k1 Lx)

(L2, slot subtraction) The slot list of k1 + β₁, where β₁ is the sum of the q-1 smallest slots of k1, equals the slot list of k1 with its first block removed: M(k1 + β₁) = M(k1) \ B₁. Adding β₁ is carry-free and "spends" exactly the digit positions occupied by the q-1 smallest slots.

theorem ZetaH123.H2.layer_cake (q d k : ℕ) (hq : 2 ≤ q) (hd : 1 < d) (hk : 0 < k) : d * k + Phi q (k - 1) d (slotLen q d k) = (d - 1) * s q 1 k + Phi q (s q 1 k - 1) (d - 1) (slotLen q (d - 1) (s q 1 k)) + s q 1 k

(L2)+(L3) Layer-cake identity linking Φ_d(M) at argument k to Φ_{d-1} at argument s_1(k) (whose slot set is M \ B₁): d·k + Φ_d(M(k - 1)) = (d-1)·s_1(k) + Φ_{d-1}(M(s_1(k)-1)) + s_1(k). Combines (L1) s_1(k)=k+β₁, (L2) slot subtraction M(s_1(k)-1)=M\B₁, and (L3) Φ_d(M)=d·β₁+Φ_{d-1}(M\B₁); pure block-reindexing algebra.

theorem ZetaH123.H2.comp_id_ge (q : ℕ) (hq : Nat.Prime q) (d k : ℕ) (hd : 1 < d) (hk : 0 < k) : s q (d - 1) (s q 1 k) + s q 1 k ≤ s q d k

Hard direction of the composition identity: s_{d-1}(s_1(k)) + s_1(k) ≤ s_d(k). Assembled from the slot formula on s_d and s_{d-1} plus the layer_cake reindexing.

theorem ZetaH123.H2.composition_identity (q : ℕ) (hq : Nat.Prime q) (d k : ℕ) (hd : 1 < d) (hk : 0 < k) : s q (d - 1) (s q 1 k) + s q 1 k = s q d k

Pillar 1, the composition identity: s_{d-1}(s_1(k)) + s_1(k) = s_d(k), i.e. F(0) = s_d(k). Antisymmetry of comp_id_le and comp_id_ge.

theorem ZetaH123.H2.wlen_eq (q L : ℕ) (hq : 2 ≤ q) (w : List ℕ) (hpow : ∀ x ∈ w, ∃ e < L, x = q ^ e) : w.length = ∑ e ∈ Finset.range L, List.count (q ^ e) w

Length of a list of powers q ^ e (e < L) is the sum of its value-counts.

theorem ZetaH123.H2.qdigit_add2 (q k1 u e : ℕ) (hq : 2 ≤ q) (hcf : ∀ (f : ℕ), qdigit q k1 f + qdigit q u f ≤ q - 1) : qdigit q (k1 + u) e = qdigit q k1 e + qdigit q u e

Carry-free digit additivity for two numbers.

theorem ZetaH123.H2.newmult_gen (q k1 u e : ℕ) (hq : 2 ≤ q) (hcf : ∀ (f : ℕ), qdigit q k1 f + qdigit q u f ≤ q - 1) : q - 1 - qdigit q (k1 + u) e + qdigit q u e = q - 1 - qdigit q k1 e

Slot multiplicity of k1+u (carry-free): smaller than k1's by qdigit u e.

theorem ZetaH123.H2.digitsum_eq (q u L : ℕ) (hq : 2 ≤ q) (huL : u < q ^ L) : u = ∑ e ∈ Finset.range L, qdigit q u e * q ^ e

Digit sum of u over range L (with u < q ^ L) is the multiset size m.

theorem ZetaH123.H2.removal_bound (q k1 u Lbig : ℕ) (hq : 2 ≤ q) (hcf : ∀ (f : ℕ), qdigit q k1 f + qdigit q u f ≤ q - 1) (huL : u < q ^ Lbig) (m : ℕ) (hm : m = ∑ e ∈ Finset.range Lbig, qdigit q u e) (t : ℕ) (ht : t ≤ (slotList q (k1 + u) Lbig).length) : (List.take (t + m) (slotList q k1 Lbig)).sum ≤ (List.take t (slotList q (k1 + u) Lbig)).sum + u

Removal bound: with u adding to k1 carry-free (so M' = slotList q (k1+u) is M = slotList q k1 with a size-m submultiset U of total value u removed), the value of the smallest t+m slots of M is at most the value of the smallest t slots of M' plus u.

theorem ZetaH123.H2.dvd_choose_of_carry (q n k : ℕ) (hq : Nat.Prime q) (hkn : k ≤ n) (hcarry : ∃ (i : ℕ), q ^ i ≤ k % q ^ i + (n - k) % q ^ i) : q ∣ n.choose k

Converse Kummer/Lucas: if k+(n - k) has a carry in base q at some position (q ^ i ≤ k%q ^ i + (n - k)%q ^ i), then q ∣ C(n,k). Proved via Nat.factorization_choose.

theorem ZetaH123.H2.admissible_carryfree (q : ℕ) (hq : Nat.Prime q) (k : ℕ) (hk : 0 < k) (j : ℕ) (hj : j ∈ Jset q k) (e : ℕ) : qdigit q (k - 1) e + qdigit q (blockSum q (k - 1) (slotLen q 1 k) 1 + j) e ≤ q - 1

Carry-free correspondence from admissibility. For j ∈ Jset q k set β = blockSum q (k - 1) (slotLen q 1 k) 1 and u = β + j. Then u adds to k-1 carry-free in base q, i.e. per position the digit sum is ≤ q-1. Uses s_one_eq (so s q 1 k - 1 = (k - 1) + β, hence s q 1 k + j - 1 = (k - 1) + u), the admissibility ¬ q ∣ C((k - 1)+u, k-1), and dvd_choose_of_carry.

theorem ZetaH123.H2.take_sum_mono (w : List ℕ) {a b : ℕ} (h : a ≤ b) : (List.take a w).sum ≤ (List.take b w).sum

Prefix-sum monotonicity: taking more (nonneg ℕ) elements never decreases the sum.

theorem ZetaH123.H2.Phi_Lindep (q k1 d L₁ Lbig : ℕ) (h : L₁ ≤ Lbig) (hlen : d * (q - 1) ≤ (slotList q k1 L₁).length) : Phi q k1 d Lbig = Phi q k1 d L₁

Phi is independent of the truncation length once it contains the first d blocks.

theorem ZetaH123.H2.extraction_core (q : ℕ) (hq : 2 ≤ q) (k1 d : ℕ) (hd : 1 < d) (u : ℕ) (hudvd : q - 1 ∣ u) (hcf : ∀ (e : ℕ), qdigit q k1 e + qdigit q u e ≤ q - 1) (L₀ L₁ L₂ : ℕ) (hL₀ : q - 1 ≤ (slotList q k1 L₀).length) (hugt : blockSum q k1 L₀ 1 < u) (hL₁ : d * (q - 1) ≤ (slotList q k1 L₁).length) (hL₂ : (d - 1) * (q - 1) ≤ (slotList q (k1 + u) L₂).length) : Phi q k1 d L₁ < d * u + Phi q (k1 + u) (d - 1) L₂

The core extraction inequality. Let u add to k1 = k-1 carry-free with (q - 1) ∣ u and u > β₁ where β₁ = blockSum q k1 L₀ 1. Then for truncations L₁, L₂ large enough to contain the relevant blocks, Φ_d(M) < d·u + Φ_{d-1}(M\U), i.e. Phi q k1 d L₁ < d*u + Phi q (k1+u) (d-1) L₂. Proof idea: expand both Phis into prefix sums, bound each prefix sum of M\U below via removal_bound, and use u > β₁ for strictness.

theorem ZetaH123.H2.extraction_strict (q : ℕ) (hq : Nat.Prime q) (d k : ℕ) (hd : 1 < d) (hk : 0 < k) (j : ℕ) (hj : j ∈ Jset q k) (hjpos : 0 < j) : s q d k < F q d k j

Pillar 2, the extraction inequality in strict form: for admissible j > 0, s_d(k) < F(j) (informal.tex Lem. lem:H2-extraction). With u = β₁ + j, admissibility makes u carry-free with k-1; the slot formula reduces the goal to extraction_core, strict since j > 0 gives u > β₁.

theorem ZetaH123.H2.main (q : ℕ) (hq : Nat.Prime q) (d k : ℕ) (hd : 1 < d) (hk : 0 < k) (j : ℕ) : j ∈ Jset q k → 0 < j → F q d k 0 < F q d k j

F attains its minimum over J uniquely at j = 0: for every admissible j ∈ J with j > 0 we have F(0) < F(j).

Assembled from composition_identity (F(0) = s_d(k)) and extraction_strict (s_d(k) < F(j) for admissible j > 0).