Exhaustive decomposition of the original short sum

The large-prefix rough-remainder majorant includes the small-total-mass case. For larger total mass, the first crossing prime gives either that majorant, the small-prime exceptional contribution, or a large prefix. The latter is covered by bounded smoothness or the intermediate logarithmic bands.

theorem NairTenenbaum.le_sum_four_indicators {p q r s : Prop} [Decidable p] [Decidable q] [Decidable r] [Decidable s] {v : ℝ} (hv : 0 ≤ v) (h : p ∨ q ∨ r ∨ s) : v ≤ (((if p then v else 0) + if q then v else 0) + if r then v else 0) + if s then v else 0

A nonnegative weight is bounded by the indicators of four covering predicates.

theorem NairTenenbaum.primeSelect_range_eq_self {r : ℕ} (n : Tuple r) {q : ℕ} (hq : mass n < q) : primeSelect n (Finset.range q) = n

A cutoff past the total mass includes every whole prime power.

theorem NairTenenbaum.PolynomialSystem.hasSmallRoughPrefixReal_of_total_mass {k r : ℕ} (P : PolynomialSystem k r) {t : ℤ} {n : Tuple r} (hn : ∀ (i : Fin r), ↑(n i) = (Polynomial.eval t (P.R i)).natAbs) {T : ℝ} (hT : ↑(weightedMass P.exponent n) ≤ T) (z : ℝ) : P.HasSmallRoughPrefixReal T z t

When the full value is below the divisor bound, an arbitrarily large cutoff supplies a rough prefix with empty remainder.

theorem NairTenenbaum.PolynomialSystem.value_weight_eq_zero {k r : ℕ} (P : PolynomialSystem k r) (F : ArithmeticMap k) {t : ℤ} (ht : Polynomial.eval t P.total = 0) : (extendArithmeticMap F fun (j : Fin k) => (Polynomial.eval t (P.Q j)).natAbs) = 0

Vanishing total polynomial values have zero arithmetic weight under the explicit zero-extension convention.

theorem NairTenenbaum.PolynomialSystem.prefix_classes_exhaustive {k r : ℕ} (P : PolynomialSystem k r) {ε x w₀ : ℝ} (hε : 0 ≤ ε) (hx : 1 ≤ x) (hw₀ : 1 ≤ w₀) (t : ℤ) (ht : Polynomial.eval t P.total ≠ 0) : P.HasSmallRoughPrefixReal (x ^ (3 * ↑P.total.natDegree ^ 2 * ε)) (x ^ (↑P.total.natDegree * ε / 16)) t ∨ P.HasSmallCrossingPrime ε x t ∨ P.HasLargeSmoothDivisorTuple (Finset.Icc 0 ⌊w₀⌋₊) ε x t ∨ P.HasIntermediatePrefixReal (x ^ (3 * ↑P.total.natDegree ^ 2 * ε)) (x ^ (3 * ↑P.total.natDegree ^ 2 * ε / 2)) w₀ x (↑P.total.natDegree * ε / 16) t

Every nonzero polynomial value belongs to at least one of the four proved majorants. The classes may overlap; disjointness is unnecessary for nonnegative arithmetic weights.