H1 for Thakur's hypotheses on power sums #
Carry-free condition (Definition 2): in every digit position n, the sum of the
n-th base-q digits of the entries is at most q - 1.
Equations
- ZetaH123.H1.CarryFree q d kk = ∀ (n : ℕ), ∑ i : Fin (d + 1), ZetaH123.H1.digit q (kk i) n ≤ q - 1
Instances For
The objective function F (Definition 4).
Equations
- ZetaH123.H1.F q d kk = ZetaH123.H1.bCoeff q 0 d + ∑ i : Fin (d + 1), ↑(kk i) * ZetaH123.H1.bCoeff q (↑i) d
Instances For
Supporting lemmas #
Elementary structural facts: every component of an admissible tuple is ≤ k,
base-q digits are ≤ q-1, the "all in slot 0" tuple is admissible, and the
admissible set is finite.
The crux: uniqueness of the maximizer #
Maximizing F is equivalent to minimizing the linear functional
Φ(kk) = q ^ {d+1}·∑ᵢ kkᵢ + (q - 1)·∑ᵢ i·qⁱ·kkᵢ, in which each "stone" in cell
(i,n) (one unit of the digit a_{i,n}) carries weight q ^ {n+i}·g_i with
g_i = q ^ {d+1-i} + (q - 1)·i strictly decreasing in i (informal.tex
eq:Phi-H1, eq:g-decreasing-H1). Two pillars: carry elimination
(carry_elimination: a maximizer's column sums are exactly the base-q
digits of k) and uniqueness of the greedy allocation via exchange arguments
(move_down, move_parallelogram).
Digit bookkeeping for the single-column exchange #
The strict Φ-decrease arithmetic. The key identity
q·g_{j+1} + (q - 1) ^ 2·(d-j) = g_j + (q - 1)·g_d, i.e.
g_j + (q - 1)·g_d - q·g_{j+1} = (q - 1) ^ 2·(d-j) > 0 for j < d, q ≥ 2
(informal.tex lem:H1-carry-elimination).
The F ↔ Φ reduction. Comparing F of two admissible tuples with the
same k reduces to comparing their Φ, where
Φ(kk) = q ^ {d+1}·∑ᵢ kkᵢ + (q - 1)·∑ᵢ i·qⁱ·kkᵢ: a strict Φ-decrease (from kk to kk')
gives a strict F-increase. (Identity (q - 1)·(-(∑ᵢ kkᵢ·b(i,d))) + q·k = Φ(kk).)
Row selection (take-from-top). Given nonnegative row-counts a on Fin (d + 1)
and a target c with 1 ≤ c ≤ ∑ a, there is a removal function r ≤ a removing
exactly c stones, taken greedily from the top rows: there is a maximal removed row
J (r J > 0) above which nothing is removed (r i = 0 for i > J).
Representation preservation for the single-column exchange. Removing r i
stones at cell (i, m-i) (r i ≤ a_{i,m-i}, r i = 0 for i > m, ∑ r = q) and
adding one stone at cell (j+1, m-j) (jj = j+1, j ≤ m) leaves ∑ kk_i q ^ i
unchanged.
Maximal removed non-top row. From a removal r with ∑ r = q whose top-row
value is ≤ q-1, there is a maximal row j < d that loses a stone, with no removed
rows strictly between j and d.
Carry-free preservation for the single-column exchange. The exchanged tuple
kk' (remove r i stones at cell (i,m-i), add one at (jj,m-jv), jj = jv+1)
stays carry-free. jrow is the maximal removed non-top row, jv = jrow.
Strict F-increase for the single-column exchange. The exchanged tuple kk'
has strictly larger F, since Φ drops by q ^ m·(q - 1) ^ 2·(d-jv) > 0.
Carry-exchange improvement. If an admissible kk has a shifted carry at
some column m (shifted column sum ∑_i a_{i,m-i} ≥ q), there is an admissible
kk' with strictly larger F: remove q stones from Col_m, add one at
(j+1, m-j) for j < d the maximal occupied non-top row
(informal.tex lem:H1-carry-elimination).
Carry elimination. An admissible F-maximizer has no shifted carries: for
every m, ∑_i a_{i,m-i} ≤ q-1. Otherwise carry_exchange_improves would give an
admissible tuple with strictly larger F (informal.tex lem:H1-carry-elimination).
The potential Φ(kk) = q ^ {d+1}·∑ᵢ kkᵢ + (q - 1)·∑ᵢ i·qⁱ·kkᵢ (matches the form used by
F_lt_of_Phi_lt). Minimizing Φ over equal-representation admissible tuples is equivalent
to maximizing F.
Equations
Instances For
Single downward move within a column. Move one stone from cell (i, m-i) down
to cell (j, m-j) (same column, rows i < j ≤ d), when the source cell is occupied
and the target diagonal m-j has slack (≤ q-2 stones). The result is admissible
and has strictly smaller Φ (by q ^ m (g_j - g_i) < 0).
Parallelogram double move. When the target diagonal m-j is full, swap two
stones around a parallelogram with corners P=(i,m-i), S=(j+t,m-j), Q=(i+t,m-i),
R=(j,m-j) (rows i<j, shift t ≥ 1, all rows ≤ d): remove one from P and S,
add one to Q and R. This preserves every column and diagonal sum (so admissibility
needs no slack hypothesis) and strictly lowers Φ by (q - 1)(j-i)(q ^ m - q ^ {m+t}) < 0.
No two distinct maximizers #
A maximizer minimizes Φ. For an admissible F-maximizer kk, every
admissible tuple kk' with the same k has Φ kk ≤ Φ kk' (via F_lt_of_Phi_lt).
Exact column sums. A maximizer kk has exactly digit q k m stones in
column m (∑_{i ≤ m} digit q (kk i) (m-i) = digit q k m): by carry_elimination
the column sums are ≤ q-1, so they form the unique base-q digit string of k.
Extremal differing-cell selection. Given admissible a ≠ b with equal column
sums in every column, there are a column m₀ and rows i₀ < j₀ (i₀, j₀ ≤ m₀,
j₀ ≤ d) such that a and b agree on every cell in columns < m₀, and either
a has a surplus at (i₀, m₀-i₀) and a deficit at (j₀, m₀-j₀), or the mirror
image with a and b swapped. In both cases the surplus row lies strictly above
the deficit row, so a downward move on the surplus array is possible.
Surplus row exists in the full-diagonal case. In the configuration produced by
differing_cell_select (rows i₀ < j₀ ≤ m₀, a,b agree below column m₀, a
deficit at (j₀, m₀-j₀)), if the target diagonal m₀-j₀ is full in a
(∑_r digit q (a r) (m₀-j₀) = q-1), then there is a shift t ≥ 1 with
j₀ + t ≤ d and a stone at (j₀+t, m₀-j₀).
No two distinct admissible maximizers. Two admissible F-maximizers agree in
every base-q digit of every row: both have column sums digit q k m
(column_sum_eq), so if they differed, differing_cell_select plus an improving
step (move_down or, via parallelogram_exists, move_parallelogram) on the
surplus array would strictly lower Φ, contradicting maximizer_min_Phi.
Greedy uniqueness. Any two admissible tuples that both maximize F over the
admissible set are equal: by digit_ext it suffices that all base-q digits agree,
which is no_two_distinct_maximizers (informal.tex alg:H1-greedy).
Theorem (Unique maximizer). Let q be a prime and d, k ≥ 0. Among all
admissible (d + 1)-tuples, the value F attains its maximum at exactly one admissible
tuple: there exists an admissible kstar that maximizes F, and any admissible tuple
that itself maximizes F over all admissible tuples must equal kstar.