Size bounds for the initialized-input magnitude convention

Native parameter computation uses (n+2)^κ, including at lengths zero and one. The existing finite instances retain their actual input-length parameter n; only their quantitative upper bounds are compared with the existing estimates at n+2.

Main results

• mPar_mono_input: candidate bounds are monotone in input length.
• mPar_shifted_pow_le: square-root times squared-logarithm bound for the actual native modulus.
• length_instances_shifted_pow_le: degree-seven logarithmic instance count at every length.
• packed_length_shifted_pow_le: linear times fourth-logarithm common packed length.

These elementary parameter bridges are original and reuse the existing finite Chan–He bounds. They do not change the finite instances or replace the actual input length by a padded input.

theorem Cslib.Algorithms.ThreeSum.ChanHe.mPar_mono_input {n n' : ℕ} (hn : n ≤ n') (U : ℕ) : mPar n U ≤ mPar n' U

Increasing the length parameter increases the candidate window without changing magnitude.

theorem Cslib.Algorithms.ThreeSum.ChanHe.mPar_shifted_pow_le (n κ : ℕ) : mPar n (2 * (n + 2) ^ κ) ≤ (5 * κ + 16) * (10 * κ + 40) * ((n + 2).sqrt + 1) * (Nat.log 2 (n + 2) + 1) ^ 2

The actual native parameter keeps length n and uses shifted polynomial magnitude.

theorem Cslib.Algorithms.ThreeSum.ChanHe.length_instances_shifted_pow_le (n κ : ℕ) (x : Fin n → ℤ) : (instances n ((n + 2) ^ κ) x).length ≤ numBound κ (n + 2)

The unchanged actual finite instance list has a logarithmic count even at lengths zero/one.

theorem Cslib.Algorithms.ThreeSum.ChanHe.packed_length_shifted_pow_le (κ n : ℕ) : 8 * mPar n (2 * (n + 2) ^ κ) ^ 2 ≤ 32 * ((5 * κ + 16) * (10 * κ + 40)) ^ 2 * (n + 2) * (Nat.log 2 (n + 2) + 1) ^ 4

The unchanged common packed length is bounded by the old estimate evaluated at n+2.