PrimeNumberTheoremAnd

Given coefficient upper bounds and the two endpoint values of the majorant under 291.60, the exact Lemma-8 supremum for any row [b,b'] (k=5, 20 ≤ b) is ≤ T.

Given coefficient upper bounds and the two endpoint values of the majorant under 291.60, the exact Lemma-8 supremum for any row [b,b'] (k=5, 20 ≤ b) is ≤ T. -/ theorem row_bound_k5 (b b' A₁ A₂ E T : ℝ) (hbb' : b ≤ b') (hb20 : 20 ≤ b) (hA1 : 0 ≤ A₁) (hA2 : 0 ≤ A₂) (hE : 0 ≤ E) (ha1 : Inputs.default.a₁ b ≤ A₁) (ha2 : Inputs.default.a₂ b ≤ A₂) (heps : Inputs.default.ε b ≤ E) (hGb : Gp A₁ A₂ E b ≤ T) (hGb' : Gp A₁ A₂ E b' ≤ T) : B_8_exact 5 b b' ≤ T := by unfold B_8_exact refine B_le_of_forall_log _ _ _ _ hbb' ?_ intro y hy have hy0 : (0 : ℝ) ≤ y := by have := hy.1; linarith have hy5 : (0 : ℝ) ≤ y ^ 5 := pow_nonneg hy0 5 have hconv : Gp A₁ A₂ E y ≤ T := le_trans ((Gp_convexOn b b' hbb' hb20 hA1 hA2 hE).le_max_of_mem_Icc (left_mem_Icc.mpr hbb') (right_mem_Icc.mpr hbb') hy) (max_le hGb hGb') rw [show Finset.Icc 1 2 = {1, 2} from by decide, Finset.sum_insert (by decide), Finset.sum_singleton] have hif1 : (if (1 : ℕ) = 1 then Inputs.default.a₁ b else if (1 : ℕ) = 2 then Inputs.default.a₂ b else 0) = Inputs.default.a₁ b := by norm_num have hif2 : (if (2 : ℕ) = 1 then Inputs.default.a₁ b else if (2 : ℕ) = 2 then Inputs.default.a₂ b else 0) = Inputs.default.a₂ b := by norm_num have ce1 : Real.exp (-(((1 : ℕ) : ℝ) / (((1 : ℕ) : ℝ) + 1) * y)) = Real.exp (-(1 / 2 * y)) := by congr 1; push_cast; ring have ce2 : Real.exp (-(((2 : ℕ) : ℝ) / (((2 : ℕ) : ℝ) + 1) * y)) = Real.exp (-(2 / 3 * y)) := by congr 1; push_cast; ring rw [hif1, hif2, ce1, ce2] have e1 : (0 : ℝ) ≤ y ^ 5 * Real.exp (-(1 / 2 * y)) := mul_nonneg hy5 (Real.exp_pos _).le have e2 : (0 : ℝ) ≤ y ^ 5 * Real.exp (-(2 / 3 * y)) := mul_nonneg hy5 (Real.exp_pos _).le have h1 : Inputs.default.a₁ b * y ^ 5 * Real.exp (-(1 / 2 * y)) ≤ A₁ * (y ^ 5 * Real.exp (-(1 / 2 * y))) := by rw [mul_assoc]; exact mul_le_mul_of_nonneg_right ha1 e1 have h2 : Inputs.default.a₂ b * y ^ 5 * Real.exp (-(2 / 3 * y)) ≤ A₂ * (y ^ 5 * Real.exp (-(2 / 3 * y))) := by rw [mul_assoc]; exact mul_le_mul_of_nonneg_right ha2 e2 have h3 : Inputs.default.ε b * y ^ 5 ≤ E * y ^ 5 := mul_le_mul_of_nonneg_right heps hy5 have hGpy : Gp A₁ A₂ E y = A₁ * (y ^ 5 * Real.exp (-(1 / 2 * y))) + A₂ * (y ^ 5 * Real.exp (-(2 / 3 * y))) + E * y ^ 5 := by unfold Gp expT; ring rw [hGpy] at hconv linarith [h1, h2, h3, hconv]

/-! Cert-free crude a₂ bound + regime-2 row 60 (b'=65, crude a₂, convexity template).

The second max argument of a₂ is dominated by the same exp-sum with one more term.

Mid-tier cert-free a₂ bound: explicit head (k = 3..12) plus tail count times the k = 13 term. Valid for any b > 0 with ⌊b / log 2⌋₊ = K ≥ 12.

k = 1 row template (majorant y·e^{-cy}, no pow machinery): given coefficient upper bounds and the two endpoint majorant values under T, the exact Lemma-8 supremum for any row [b,b'] (20 ≤ b) is ≤ T.

General-k (k = m+2, m ≤ 3) row template: given coefficient upper bounds and the two endpoint majorant values under T, the exact Lemma-8 supremum for any row [b,b'] (20 ≤ b) is ≤ T. Proven ONCE; rows 20-... for every column k ∈ {2,3,4,5} instantiate it.

General a₁ bound on the constant branch: valid for every b ≤ 86.

General a₁ bound on the constant branch: valid for every b ≤ 86. -/ lemma a1_le_small {b : ℝ} (hb : b ≤ 86) : Inputs.default.a₁ b ≤ (1.00000002 : ℝ) := by have hlog : (43 : ℝ) < log Inputs.default.x₁ ∧ log Inputs.default.x₁ < 44 := by change (43 : ℝ) < log (1e19 : ℝ) ∧ log (1e19 : ℝ) < 44 have h1e19 : (1e19 : ℝ) = (10 : ℝ) ^ 19 := by norm_num rw [h1e19, Real.log_pow]; push_cast constructor <;> nlinarith [LogTables.log_10_gt, LogTables.log_10_lt] have hε19 : Inputs.default.ε (log Inputs.default.x₁) ≤ 1.93378e-8 * BKLNW_app.table_8_margin := by change BKLNW_app.table_8_ε (log Inputs.default.x₁) ≤ 1.93378e-8 * BKLNW_app.table_8_margin grw [BKLNW_app.table_8_ε.le_simp (log Inputs.default.x₁) (by linarith [hlog.1])] grind [BKLNW_app.table_8_ε'] unfold Inputs.a₁ rw [if_pos (by linarith [hlog.1] : b ≤ 2 * log Inputs.default.x₁)] have hb' : (1.93378e-8 * BKLNW_app.table_8_margin : ℝ) ≤ 1.00000002 - 1 := by norm_num [BKLNW_app.table_8_margin] linarith [hε19, hb']

/-! ## Regime-3 pointwise template (b ≳ 80): no convexity, no derivative machinery, uniform in every column k. Per-term endpoint bounds reduce the supremum to ONE constant inequality, dischargeable by interval_decide per row. Ported from the compiled row100_pointwise.lean exemplar, parameterized over k + coefficients.

C_bk_S is antitone in b (for nonnegative c, C): each exp term decreases.