LiBasePoints.lean

717 lines · 26 declarations · 0 sorries · updated 08-26-2026
Declarations

Kind	Name	Line
theorem	`exp_le_inv_sub_sixteen`	38
theorem	`exp_one_pow_le`	59
theorem	`exp_one_pow_ge`	62
theorem	`exp_eleven`	66
theorem	`exp_five`	71
theorem	`exp_four`	76
theorem	`exp_five_halves_le`	83
theorem	`log80000_ge`	104
theorem	`log80000_le`	121
theorem	`log100000_ge`	139
theorem	`logpi_le`	156
theorem	`logpi_ge`	173
theorem	`sqrt80000_le`	189
theorem	`sqrt80000_ge`	193
theorem	`sqrt100000_le`	197
theorem	`sqrt100000_ge`	201
theorem	`sInftyLower_eq'`	208
theorem	`sInftyLower_80000_lo`	217
theorem	`sInftyLower_80000_up`	233
theorem	`sInftyLower_100000_lo`	249
theorem	`Bn_FAlt_80000_le`	268
theorem	`Bn_FAlt_80000_ge`	428
theorem	`Bn_FAlt_100000_le`	522
theorem	`marginTilde_FAlt_80000_pos`	681
theorem	`marginTilde_FAlt_80000_lt_100000`	691
theorem	`lambda_pos_finite_height_verified`	706
Source

/-
NguyenRH1/LiBasePoints.lean — [PROVED] tier (ii) step 2 (session 012):
the two elementary margin evaluations consumed by
`lambda_pos_finite_height`, discharged by certified rational interval
bounds, and the resulting three-hypothesis headline form
`lambda_pos_finite_height_verified` (perimeter + `SfBoundProp` only).

Plan and validation: D-062 §5 (every link pre-verified at dps 40 and by
exact Fraction arithmetic; true values margiñ(8×10⁴) = 15 763.79 and
margiñ(10⁵) ≈ 9.3×10⁴ from E-028/E-029-scale computations). All
certified targets carry explicit slack; the tightest link
(e¹·¹⁴⁴⁸ ≥ π at 0.007%) was replaced by the comfortable e¹·¹⁵ ≥ π
at a ~104-unit cost, absorbed by the margin. The certified ≥ 8 001 is
deliberately coarser than the D-062 §5 dps-40 plan's > 9 960 (outward
rounding for norm_num comfort); both suffice — number-trail note filed
in D-062 §5.

Machinery: exp upper bounds via exp x = (exp(x/16))¹⁶ ≤ (1−x/16)⁻¹⁶
(from 1 − y ≤ e^{−y}, Mathlib `Real.add_one_le_exp`); exp lower bounds
via partial sums (`Real.sum_le_exp_of_nonneg`) and the d9 rational
bounds on e (`Real.exp_one_gt_d9/lt_d9`); log comparisons by
monotonicity through these; π via `Real.pi_gt_d20/lt_d20`; log 2 via
`Real.log_two_gt_d9/lt_d9`.
-/
import Mathlib
import NguyenRH1.LiSkeleton

open Zeta23 Complex Filter Topology

noncomputable section

namespace NguyenRH1

/-! ### 1. Certified exp/log machinery -/

/-- [PROVED session 012] exp x ≤ (1 − x/16)⁻¹¹⁶ for 0 ≤ x < 16:
exp(x/16) ≤ (1 − x/16)⁻¹ from 1 − y ≤ e^{−y}, then the 16th power. -/
theorem exp_le_inv_sub_sixteen {x : ℝ} (_hx0 : 0 ≤ x) (hx1 : x < 16) :
    Real.exp x ≤ (1 - x / 16)⁻¹ ^ 16 := by
  have h16 : ((16 : ℕ) : ℝ) ≠ 0 := by norm_num
  have hpos : (0 : ℝ) < 1 - x / 16 := by linarith
  have h1 : 1 - x / 16 ≤ (Real.exp (x / 16))⁻¹ := by
    have h := Real.add_one_le_exp (-(x / 16))
    rw [Real.exp_neg] at h
    linarith
  have h2 : Real.exp (x / 16) ≤ (1 - x / 16)⁻¹ := by
    have h3 := one_div_le_one_div_of_le hpos h1
    rwa [one_div, one_div, inv_inv] at h3
  have h4 : Real.exp x = (Real.exp (x / 16)) ^ 16 := by
    rw [← Real.exp_nat_mul (x / 16) 16]
    congr 1
    push_cast
    ring
  rw [h4]
  exact pow_le_pow_left₀ (Real.exp_nonneg _) h2 16

/-- [PROVED session 012] Powers of e bounded by powers of the d9
rationals. -/
theorem exp_one_pow_le (n : ℕ) : Real.exp 1 ^ n ≤ (2.7182818286 : ℝ) ^ n :=
  pow_le_pow_left₀ (Real.exp_pos 1).le Real.exp_one_lt_d9.le n

theorem exp_one_pow_ge (n : ℕ) : (2.7182818283 : ℝ) ^ n ≤ Real.exp 1 ^ n :=
  pow_le_pow_left₀ (by norm_num) Real.exp_one_gt_d9.le n

/-- [PROVED session 012] Integer exponentials as powers of e. -/
theorem exp_eleven : Real.exp 11 = Real.exp 1 ^ 11 := by
  rw [← Real.exp_nat_mul 1 11]
  congr 1
  norm_num

theorem exp_five : Real.exp 5 = Real.exp 1 ^ 5 := by
  rw [← Real.exp_nat_mul 1 5]
  congr 1
  norm_num

theorem exp_four : Real.exp 4 = Real.exp 1 ^ 4 := by
  rw [← Real.exp_nat_mul 1 4]
  congr 1
  norm_num

/-- [PROVED session 040] e^{5/2} ≤ 12.183 (via e³/e^{0.5} with the tight
division-by-partial-sum route; D-074's V_left kernel constant). -/
theorem exp_five_halves_le : Real.exp (5 / 2) ≤ (12.183 : ℝ) := by
  have h3 : Real.exp 3 ≤ (20.0856 : ℝ) := by
    have e : Real.exp 3 = Real.exp 1 ^ 3 := by
      rw [← Real.exp_nat_mul 1 3]
      congr 1
      norm_num
    rw [e]
    exact le_trans (exp_one_pow_le 3) (by norm_num)
  have h05 : (1.6487 : ℝ) ≤ Real.exp 0.5 :=
    le_trans (by norm_num [Finset.sum_range_succ])
      (Real.sum_le_exp_of_nonneg (by norm_num : (0 : ℝ) ≤ 0.5) 7)
  have h1 : Real.exp (5 / 2) = Real.exp 3 / Real.exp 0.5 := by
    rw [show (5 / 2 : ℝ) = 3 - 0.5 by norm_num, Real.exp_sub]
  rw [h1]
  calc Real.exp 3 / Real.exp 0.5 ≤ 20.0856 / 1.6487 :=
      div_le_div₀ (by norm_num) h3 (by norm_num) h05
    _ ≤ 12.183 := by norm_num

/-! ### 2. Certified log bounds at the margin points -/

/-- [PROVED session 012] log 80000 ≥ 11.263 (e¹¹·²⁶³ ≤ 78057 < 80000). -/
theorem log80000_ge : (11.263 : ℝ) ≤ Real.log 80000 := by
  have h1 : Real.exp 11 ≤ (59874.31 : ℝ) := by
    rw [exp_eleven]
    exact le_trans (exp_one_pow_le 11) (by norm_num)
  have h2 : Real.exp 0.263 ≤ (1.3037 : ℝ) :=
    le_trans (exp_le_inv_sub_sixteen (by norm_num) (by norm_num)) (by norm_num)
  have h3 : Real.exp 11.263 = Real.exp 11 * Real.exp 0.263 := by
    rw [show (11.263 : ℝ) = 11 + 0.263 by norm_num, Real.exp_add]
  have h4 : Real.exp 11 * Real.exp 0.263 ≤ 59874.31 * 1.3037 :=
    mul_le_mul h1 h2 (Real.exp_pos _).le (by norm_num)
  have h5 : Real.exp 11.263 ≤ 80000 := by
    rw [h3]
    exact le_trans h4 (by norm_num)
  have h6 := Real.log_le_log (Real.exp_pos _) h5
  rwa [Real.log_exp] at h6

/-- [PROVED session 012] log 80000 ≤ 11.3 (e¹¹·³ ≥ 80822 > 80000). -/
theorem log80000_le : Real.log 80000 ≤ (11.3 : ℝ) := by
  have h1 : (59874.13 : ℝ) ≤ Real.exp 11 := by
    rw [exp_eleven]
    exact le_trans (by norm_num) (exp_one_pow_ge 11)
  have h2 : (1.34985 : ℝ) ≤ Real.exp 0.3 :=
    le_trans (by norm_num [Finset.sum_range_succ])
      (Real.sum_le_exp_of_nonneg (by norm_num : (0 : ℝ) ≤ 0.3) 7)
  have h3 : Real.exp 11.3 = Real.exp 11 * Real.exp 0.3 := by
    rw [show (11.3 : ℝ) = 11 + 0.3 by norm_num, Real.exp_add]
  have h4 : (80000 : ℝ) ≤ Real.exp 11 * Real.exp 0.3 :=
    le_trans (by norm_num) (mul_le_mul h1 h2 (by norm_num) (Real.exp_pos _).le)
  have h5 : (80000 : ℝ) ≤ Real.exp 11.3 := by
    rw [h3]
    exact h4
  have h6 := Real.log_le_log (by norm_num : (0 : ℝ) < 80000) h5
  rwa [Real.log_exp] at h6

/-- [PROVED session 012] log 100000 ≥ 11.5 (e¹¹·⁵ ≤ 99661 < 100000). -/
theorem log100000_ge : (11.5 : ℝ) ≤ Real.log 100000 := by
  have h1 : Real.exp 11 ≤ (59874.31 : ℝ) := by
    rw [exp_eleven]
    exact le_trans (exp_one_pow_le 11) (by norm_num)
  have h2 : Real.exp 0.5 ≤ (1.6644 : ℝ) :=
    le_trans (exp_le_inv_sub_sixteen (by norm_num) (by norm_num)) (by norm_num)
  have h3 : Real.exp 11.5 = Real.exp 11 * Real.exp 0.5 := by
    rw [show (11.5 : ℝ) = 11 + 0.5 by norm_num, Real.exp_add]
  have h4 : Real.exp 11 * Real.exp 0.5 ≤ 59874.31 * 1.6644 :=
    mul_le_mul h1 h2 (Real.exp_pos _).le (by norm_num)
  have h5 : Real.exp 11.5 ≤ 100000 := by
    rw [h3]
    exact le_trans h4 (by norm_num)
  have h6 := Real.log_le_log (Real.exp_pos _) h5
  rwa [Real.log_exp] at h6

/-- [PROVED session 012] log π ≤ 1.15 (e¹·¹⁵ ≥ 3.1582 > π). -/
theorem logpi_le : Real.log Real.pi ≤ (1.15 : ℝ) := by
  have h1 : (2.7182818283 : ℝ) ≤ Real.exp 1 := Real.exp_one_gt_d9.le
  have h2 : (1.1618 : ℝ) ≤ Real.exp 0.15 :=
    le_trans (by norm_num [Finset.sum_range_succ])
      (Real.sum_le_exp_of_nonneg (by norm_num : (0 : ℝ) ≤ 0.15) 7)
  have h3 : Real.exp 1.15 = Real.exp 1 * Real.exp 0.15 := by
    rw [show (1.15 : ℝ) = 1 + 0.15 by norm_num, Real.exp_add]
  have h4 : (3.1415926536 : ℝ) ≤ Real.exp 1 * Real.exp 0.15 :=
    le_trans (by norm_num) (mul_le_mul h1 h2 (by norm_num) (Real.exp_pos _).le)
  have h5 : Real.pi ≤ Real.exp 1.15 := by
    have hpi := Real.pi_lt_d20.le
    rw [h3]
    linarith
  have h6 := Real.log_le_log Real.pi_pos h5
  rwa [Real.log_exp] at h6

/-- [PROVED session 012] log π ≥ 1.14 (e¹·¹⁴ ≤ 3.1287 < π). -/
theorem logpi_ge : (1.14 : ℝ) ≤ Real.log Real.pi := by
  have h1 : Real.exp 1 ≤ (2.7182818286 : ℝ) := Real.exp_one_lt_d9.le
  have h2 : Real.exp 0.14 ≤ (1.151 : ℝ) :=
    le_trans (exp_le_inv_sub_sixteen (by norm_num) (by norm_num)) (by norm_num)
  have h3 : Real.exp 1.14 = Real.exp 1 * Real.exp 0.14 := by
    rw [show (1.14 : ℝ) = 1 + 0.14 by norm_num, Real.exp_add]
  have h4 : Real.exp 1 * Real.exp 0.14 ≤ 2.7182818286 * 1.151 :=
    mul_le_mul h1 h2 (Real.exp_pos _).le (by norm_num)
  have h5 : Real.exp 1.14 ≤ Real.pi := by
    have hpi := Real.pi_gt_d20.le
    rw [h3]
    linarith
  have h6 := Real.log_le_log (Real.exp_pos _) h5
  rwa [Real.log_exp] at h6

/-- [PROVED session 012] √80000 ≤ 283 (283² = 80089). -/
theorem sqrt80000_le : Real.sqrt 80000 ≤ 283 :=
  (Real.sqrt_le_left (by norm_num)).mpr (by norm_num)

/-- [PROVED session 012] √80000 ≥ 282 (282² = 79524). -/
theorem sqrt80000_ge : (282 : ℝ) ≤ Real.sqrt 80000 :=
  (Real.le_sqrt (by norm_num) (by norm_num)).mpr (by norm_num)

/-- [PROVED session 012] √100000 ≤ 317 (317² = 100489). -/
theorem sqrt100000_le : Real.sqrt 100000 ≤ 317 :=
  (Real.sqrt_le_left (by norm_num)).mpr (by norm_num)

/-- [PROVED session 012] √100000 ≥ 316 (316² = 99856). -/
theorem sqrt100000_ge : (316 : ℝ) ≤ Real.sqrt 100000 :=
  (Real.le_sqrt (by norm_num) (by norm_num)).mpr (by norm_num)

/-! ### 3. The archimedean lower bound evaluated -/

/-- [PROVED session 012] Normal form of sInftyLower: the γ cancels
exactly (D-037 parity algebra at the point level). -/
theorem sInftyLower_eq' (n : ℝ) :
    sInftyLower n = (1 / 2) * n * Real.log n -
      ((1 + Real.log 2 + Real.log Real.pi) / 2) * n - 4 := by
  unfold sInftyLower lagariasC1
  rw [Real.log_mul (by norm_num : (2 : ℝ) ≠ 0) Real.pi_ne_zero]
  ring

/-- [PROVED session 012] sInftyLower(8×10⁴) ≥ 336000 (certified
336 790; true 338 072). -/
theorem sInftyLower_80000_lo : (336000 : ℝ) ≤ sInftyLower 80000 := by
  rw [sInftyLower_eq']
  have h1 := log80000_ge
  have h2 := Real.log_two_lt_d9.le
  have h3 := logpi_le
  have g1 : (1 / 2 : ℝ) * 80000 * 11.263 ≤ (1 / 2) * 80000 * Real.log 80000 :=
    mul_le_mul_of_nonneg_left h1 (by norm_num)
  have g2 : ((1 + Real.log 2 + Real.log Real.pi) / 2) * 80000 ≤
      (2.8431472 / 2 : ℝ) * 80000 := by
    apply mul_le_mul_of_nonneg_right _ (by norm_num : (0 : ℝ) ≤ 80000)
    rw [div_le_div_iff_of_pos_right (by norm_num : (0 : ℝ) < 2)]
    linarith
  linarith [g1, g2]

/-- [PROVED session 012] sInftyLower(8×10⁴) ≤ 339000 (certified
338 671; true 338 072). -/
theorem sInftyLower_80000_up : sInftyLower 80000 ≤ (339000 : ℝ) := by
  rw [sInftyLower_eq']
  have h1 := log80000_le
  have h2 := Real.log_two_gt_d9.le
  have h3 := logpi_ge
  have g1 : (1 / 2 : ℝ) * 80000 * Real.log 80000 ≤ (1 / 2) * 80000 * 11.3 :=
    mul_le_mul_of_nonneg_left h1 (by norm_num)
  have g2 : ((2.8331471 : ℝ) / 2) * 80000 ≤
      ((1 + Real.log 2 + Real.log Real.pi) / 2) * 80000 := by
    apply mul_le_mul_of_nonneg_right _ (by norm_num : (0 : ℝ) ≤ 80000)
    rw [div_le_div_iff_of_pos_right (by norm_num : (0 : ℝ) < 2)]
    linarith
  linarith [g1, g2]

/-- [PROVED session 012] sInftyLower(10⁵) ≥ 432500 (certified
432 839; true ≈ 433 747). -/
theorem sInftyLower_100000_lo : (432500 : ℝ) ≤ sInftyLower 100000 := by
  rw [sInftyLower_eq']
  have h1 := log100000_ge
  have h2 := Real.log_two_lt_d9.le
  have h3 := logpi_le
  have g1 : (1 / 2 : ℝ) * 100000 * 11.5 ≤ (1 / 2) * 100000 * Real.log 100000 :=
    mul_le_mul_of_nonneg_left h1 (by norm_num)
  have g2 : ((1 + Real.log 2 + Real.log Real.pi) / 2) * 100000 ≤
      (2.8431472 / 2 : ℝ) * 100000 := by
    apply mul_le_mul_of_nonneg_right _ (by norm_num : (0 : ℝ) ≤ 100000)
    rw [div_le_div_iff_of_pos_right (by norm_num : (0 : ℝ) < 2)]
    linarith
  linarith [g1, g2]

/-! ### 4. The finite-part bound evaluated -/

/-- [PROVED session 012; target updated session 040 for the D-074
dog-leg repair] Bn FAlt(8×10⁴) ≤ 332000 (certified ≈ 331 005; true
≈ 325 122 with the dog-leg Bn, E-034's exact Bn_DL = 324 913). -/
theorem Bn_FAlt_80000_le : Bn FAlt 80000 ≤ (332000 : ℝ) := by
  have hT : Real.sqrt 80000 + 1 ≤ 284 := by
    have h := sqrt80000_le
    linarith
  have hTpos : (0 : ℝ) < Real.sqrt 80000 + 1 := by
    have h := Real.sqrt_nonneg 80000
    linarith
  -- log T ≤ 5.7 (T ≤ 284 ≤ e⁵·⁷ = e⁵·e⁰·⁷, 148.328·2.0136 = 298.674)
  have h5 : (148.328 : ℝ) ≤ Real.exp 5 := by
    rw [exp_five]
    exact le_trans (by norm_num) (exp_one_pow_ge 5)
  have h07 : (2.0136 : ℝ) ≤ Real.exp 0.7 :=
    le_trans (by norm_num [Finset.sum_range_succ])
      (Real.sum_le_exp_of_nonneg (by norm_num : (0 : ℝ) ≤ 0.7) 7)
  have h57 : Real.exp 5.7 = Real.exp 5 * Real.exp 0.7 := by
    rw [show (5.7 : ℝ) = 5 + 0.7 by norm_num, Real.exp_add]
  have h57big : (284 : ℝ) ≤ Real.exp 5.7 := by
    rw [h57]
    exact le_trans (by norm_num : (284 : ℝ) ≤ 148.328 * 2.0136)
      (mul_le_mul h5 h07 (by norm_num) (Real.exp_pos _).le)
  have hlogT : Real.log (Real.sqrt 80000 + 1) ≤ (5.7 : ℝ) := by
    have h := Real.log_le_log hTpos (le_trans hT h57big)
    rwa [Real.log_exp] at h
  have h57big2 : (286 : ℝ) ≤ Real.exp 5.7 := by
    rw [h57]
    exact le_trans (by norm_num : (286 : ℝ) ≤ 148.328 * 2.0136)
      (mul_le_mul h5 h07 (by norm_num) (Real.exp_pos _).le)
  have hlogT2 : Real.log (Real.sqrt 80000 + 1 + 2) ≤ (5.7 : ℝ) := by
    have hbig : Real.sqrt 80000 + 1 + 2 ≤ Real.exp 5.7 := by
      have h : Real.sqrt 80000 + 1 + 2 ≤ (286 : ℝ) := by linarith
      exact le_trans h h57big2
    have hT2pos : (0 : ℝ) < Real.sqrt 80000 + 1 + 2 := by linarith
    have h := Real.log_le_log hT2pos hbig
    rwa [Real.log_exp] at h
  -- log log T ≤ 1.75 (log T ≤ 5.7 ≤ e¹·⁷⁵ = e·e⁰·⁷⁵, 2.7183·2.1169)
  have h175 : Real.exp 1.75 = Real.exp 1 * Real.exp 0.75 := by
    rw [show (1.75 : ℝ) = 1 + 0.75 by norm_num, Real.exp_add]
  have h075 : (2.1169 : ℝ) ≤ Real.exp 0.75 :=
    le_trans (by norm_num [Finset.sum_range_succ])
      (Real.sum_le_exp_of_nonneg (by norm_num : (0 : ℝ) ≤ 0.75) 7)
  have h175big : (5.7 : ℝ) ≤ Real.exp 1.75 := by
    rw [h175]
    exact le_trans (by norm_num : (5.7 : ℝ) ≤ 2.7182818283 * 2.1169)
      (mul_le_mul Real.exp_one_gt_d9.le h075 (by norm_num) (Real.exp_pos _).le)
  have hloglogT : Real.log (Real.log (Real.sqrt 80000 + 1)) ≤ (1.75 : ℝ) := by
    have hlogTpos : (0 : ℝ) < Real.log (Real.sqrt 80000 + 1) :=
      Real.log_pos (by linarith [sqrt80000_ge])
    have h := Real.log_le_log hlogTpos (le_trans hlogT h175big)
    rwa [Real.log_exp] at h
  have hloglogT2 : Real.log (Real.log (Real.sqrt 80000 + 1 + 2)) ≤ (1.75 : ℝ) := by
    have hlogT2pos : (0 : ℝ) < Real.log (Real.sqrt 80000 + 1 + 2) :=
      Real.log_pos (by linarith [sqrt80000_ge])
    have h := Real.log_le_log hlogT2pos (le_trans hlogT2 h175big)
    rwa [Real.log_exp] at h
  -- e⁴ ≤ 54.6015
  have he4 : Real.exp 4 ≤ (54.6015 : ℝ) := by
    rw [exp_four]
    exact le_trans (exp_one_pow_le 4) (by norm_num)
  -- 1/(2π) ≤ 1/6
  have h2pi : (1 : ℝ) / (2 * Real.pi) ≤ 1 / 6 := by
    apply one_div_le_one_div_of_le (by norm_num : (0 : ℝ) < 6)
    have hpi := Real.pi_gt_d20.le
    linarith
  -- log T ≥ 0, log log T ≥ 0, log(T+2) ≥ 0, log log(T+2) ≥ 0
  have hlogTnn : (0 : ℝ) ≤ Real.log (Real.sqrt 80000 + 1) :=
    Real.log_nonneg (by linarith [Real.sqrt_nonneg 80000])
  have hlogT2nn : (0 : ℝ) ≤ Real.log (Real.sqrt 80000 + 1 + 2) :=
    Real.log_nonneg (by linarith [Real.sqrt_nonneg 80000])
  have hlogTge1 : (1 : ℝ) ≤ Real.log (Real.sqrt 80000 + 1) := by
    have he : Real.exp 1 ≤ Real.sqrt 80000 + 1 :=
      le_trans Real.exp_one_lt_d9.le (by linarith [sqrt80000_ge])
    have h := Real.log_le_log (Real.exp_pos 1) he
    rwa [Real.log_exp] at h
  have hloglogTnn : (0 : ℝ) ≤ Real.log (Real.log (Real.sqrt 80000 + 1)) :=
    Real.log_nonneg hlogTge1
  have hlogT2ge1 : (1 : ℝ) ≤ Real.log (Real.sqrt 80000 + 1 + 2) := by
    have he : Real.exp 1 ≤ Real.sqrt 80000 + 1 + 2 :=
      le_trans Real.exp_one_lt_d9.le (by linarith [sqrt80000_ge])
    have h := Real.log_le_log (Real.exp_pos 1) he
    rwa [Real.log_exp] at h
  have hloglogT2nn : (0 : ℝ) ≤ Real.log (Real.log (Real.sqrt 80000 + 1 + 2)) :=
    Real.log_nonneg hlogT2ge1
  -- FAlt T ≤ 273.82
  have hFAlt : FAlt (Real.sqrt 80000 + 1) ≤ (273.82 : ℝ) := by
    unfold FAlt
    have hTl : (Real.sqrt 80000 + 1) * Real.log (Real.sqrt 80000 + 1) ≤
        284 * 5.7 :=
      mul_le_mul hT hlogT hlogTnn (by norm_num)
    have ha : (1 / (2 * Real.pi)) * ((Real.sqrt 80000 + 1) *
        Real.log (Real.sqrt 80000 + 1)) ≤ (1 / 6 : ℝ) * (284 * 5.7) :=
      mul_le_mul h2pi hTl (mul_nonneg hTpos.le hlogTnn) (by norm_num)
    linarith [ha, hlogT, hloglogT]
  -- Ĉ₀ T ≤ 6.9186 and ≥ 0
  have hC0 : C0hat (Real.sqrt 80000 + 1) ≤ (6.9186 : ℝ) := by
    unfold C0hat
    linarith [hlogT2, hloglogT2]
  have hC0pos : (0 : ℝ) ≤ C0hat (Real.sqrt 80000 + 1) := by
    unfold C0hat
    linarith [hlogT2nn, hloglogT2nn]
  -- Ĥ T ≤ 251.46 and ≥ 0
  have hH : Hhat (Real.sqrt 80000 + 1) ≤ (251.46 : ℝ) := by
    unfold Hhat
    have hsq : C0hat (Real.sqrt 80000 + 1) ^ 2 ≤ 6.9186 ^ 2 :=
      pow_le_pow_left₀ hC0pos hC0 2
    linarith [hsq, hlogT2]
  have hHnn : (0 : ℝ) ≤ Hhat (Real.sqrt 80000 + 1) := by
    unfold Hhat
    have hsq : (0 : ℝ) ≤ C0hat (Real.sqrt 80000 + 1) ^ 2 := pow_nonneg hC0pos 2
    linarith [hsq, hlogT2nn]
  -- Z₂ T ≤ 7.6705 and ≥ 0 (the corrected I_III count, D-071)
  have hZ2 : Z2hat (Real.sqrt 80000 + 1) ≤ (7.6705 : ℝ) := by
    unfold Z2hat
    linarith [hlogT2, hloglogT2]
  have hZ2nn : (0 : ℝ) ≤ Z2hat (Real.sqrt 80000 + 1) := by
    unfold Z2hat
    linarith [hlogT2nn, hloglogT2nn]
  -- the big bracket: 0 ≤ · ≤ 112.9637
  have hbr : (2 / 3 : ℝ) * Z2hat (Real.sqrt 80000 + 1) +
      10.5 * Real.log (Real.sqrt 80000 + 1 + 2) + 48 ≤ 112.9637 := by
    have h1 := mul_le_mul_of_nonneg_left hZ2 (by norm_num : (0 : ℝ) ≤ 2 / 3)
    have h2 := mul_le_mul_of_nonneg_left hlogT2 (by norm_num : (0 : ℝ) ≤ 10.5)
    linarith [h1, h2]
  have hbrnn : (0 : ℝ) ≤ (2 / 3 : ℝ) * Z2hat (Real.sqrt 80000 + 1) +
      10.5 * Real.log (Real.sqrt 80000 + 1 + 2) + 48 := by
    linarith [hZ2nn, hlogT2nn]
  -- IIMaj ≤ 2590.08
  have hII : IIMaj 80000 ≤ (2590.08 : ℝ) := by
    refine le_trans (IIMaj_le_two_mul 80000 (by norm_num)) ?_
    have h3 : (4.56 : ℝ) * (Real.sqrt 80000 + 1) ≤ 4.56 * 284 :=
      mul_le_mul_of_nonneg_left (by linarith [sqrt80000_le]) (by norm_num)
    linarith [h3]
  -- the dog-leg share (D-074): 2·DogLegRight(8×10⁴) ≤ 3184 (certified)
  have hDL : 2 * DogLegRight 80000 ≤ (3184 : ℝ) := by
    unfold DogLegRight
    have hT2 : Real.sqrt 80000 + 1 ≤ 284 := hT
    have hII4 : IIMaj 80000 / 4 ≤ (2590.08 : ℝ) / 4 := by linarith [hII]
    have h1 : ((Real.sqrt 80000 + 1) / 2) * (Real.exp (5 / 2) + 1) / 2 ≤
        (284 / 2) * (13.183 : ℝ) / 2 := by
      apply div_le_div_of_nonneg_right _ (by norm_num : (0 : ℝ) ≤ 2)
      apply mul_le_mul _ _ (by positivity) (by positivity)
      · exact div_le_div_of_nonneg_right hT2 (by norm_num : (0 : ℝ) ≤ 2)
      · linarith [exp_five_halves_le]
    linarith [h1, hII4]
  -- assemble
  simp only [Bn]
  have hterm2 : 4 * (Real.sqrt 80000 + 1) * ((2 / 3) * Z2hat (Real.sqrt 80000 + 1) +
      10.5 * Real.log (Real.sqrt 80000 + 1 + 2) + 48) ≤ 4 * 284 * 112.9637 := by
    apply mul_le_mul _ hbr hbrnn (by norm_num)
    exact mul_le_mul_of_nonneg_left hT (by norm_num)
  have hterm4 : 2 * (Real.exp 4 + 1) * (7 * Hhat (Real.sqrt 80000 + 1)) ≤
      2 * (54.6015 + 1) * (7 * 251.46) := by
    apply mul_le_mul _ _ (by linarith [hHnn]) (by norm_num)
    · apply mul_le_mul_of_nonneg_left _ (by norm_num : (0 : ℝ) ≤ 2)
      linarith [he4]
    · linarith [hH]
  linarith [hFAlt, hterm2, hterm4, hDL, hII]

/-- [PROVED session 012; target updated session 040 for the D-074
dog-leg repair] Bn FAlt(8×10⁴) ≥ 273000 (the lower side only needs
the two big terms; the dog-leg share is nonneg). -/
theorem Bn_FAlt_80000_ge : (273000 : ℝ) ≤ Bn FAlt 80000 := by
  have hTge : (283 : ℝ) ≤ Real.sqrt 80000 + 1 := by
    have h := sqrt80000_ge
    linarith
  have hTpos : (0 : ℝ) < Real.sqrt 80000 + 1 := by linarith
  -- log (T+2) ≥ 5.6 (T+2 ≥ 285 ≥ e⁵·⁶ = e⁵·e⁰·⁶, 148.414·1.8433 = 273.571)
  have h5up : Real.exp 5 ≤ (148.414 : ℝ) := by
    rw [exp_five]
    exact le_trans (exp_one_pow_le 5) (by norm_num)
  have h06up : Real.exp 0.6 ≤ (1.8433 : ℝ) :=
    le_trans (exp_le_inv_sub_sixteen (by norm_num) (by norm_num)) (by norm_num)
  have h56 : Real.exp 5.6 = Real.exp 5 * Real.exp 0.6 := by
    rw [show (5.6 : ℝ) = 5 + 0.6 by norm_num, Real.exp_add]
  have h56small : Real.exp 5.6 ≤ (285 : ℝ) := by
    rw [h56]
    exact le_trans (mul_le_mul h5up h06up (Real.exp_pos _).le (by norm_num))
      (by norm_num)
  have hlogT2ge : (5.6 : ℝ) ≤ Real.log (Real.sqrt 80000 + 1 + 2) := by
    have hbig : (285 : ℝ) ≤ Real.sqrt 80000 + 1 + 2 := by linarith
    have h1 : (5.6 : ℝ) ≤ Real.log 285 := by
      have h := Real.log_le_log (Real.exp_pos _) h56small
      rwa [Real.log_exp] at h
    exact le_trans h1 (Real.log_le_log (by norm_num : (0 : ℝ) < 285) hbig)
  -- log log (T+2) ≥ 0 (log (T+2) ≥ 5.6 ≥ 1)
  have hloglogT2nn : (0 : ℝ) ≤ Real.log (Real.log (Real.sqrt 80000 + 1 + 2)) :=
    Real.log_nonneg (by linarith)
  -- log T ≥ 0 and log log T ≥ 0 (T ≥ 283 ≥ e)
  have hlogTnn : (0 : ℝ) ≤ Real.log (Real.sqrt 80000 + 1) :=
    Real.log_nonneg (by linarith)
  have hlogTge1 : (1 : ℝ) ≤ Real.log (Real.sqrt 80000 + 1) := by
    have he : Real.exp 1 ≤ Real.sqrt 80000 + 1 :=
      le_trans Real.exp_one_lt_d9.le (by linarith)
    have h := Real.log_le_log (Real.exp_pos 1) he
    rwa [Real.log_exp] at h
  have hloglogTnn : (0 : ℝ) ≤ Real.log (Real.log (Real.sqrt 80000 + 1)) :=
    Real.log_nonneg hlogTge1
  -- FAlt T ≥ 0 (every term nonneg)
  have hFAlt0 : (0 : ℝ) ≤ FAlt (Real.sqrt 80000 + 1) := by
    unfold FAlt
    have hpi : (0 : ℝ) < Real.pi := Real.pi_pos
    have hp1 : (0 : ℝ) ≤ (1 / (2 * Real.pi)) * ((Real.sqrt 80000 + 1) *
        Real.log (Real.sqrt 80000 + 1)) :=
      mul_nonneg (by positivity) (mul_nonneg hTpos.le hlogTnn)
    have hp2 : (0 : ℝ) ≤ 0.137 * Real.log (Real.sqrt 80000 + 1) :=
      mul_nonneg (by norm_num) hlogTnn
    have hp3 : (0 : ℝ) ≤ 0.443 * Real.log (Real.log (Real.sqrt 80000 + 1)) :=
      mul_nonneg (by norm_num) hloglogTnn
    linarith [hp1, hp2, hp3]
  -- Ĉ₀ T ≥ 5.3248
  have hC0lo : (5.3248 : ℝ) ≤ C0hat (Real.sqrt 80000 + 1) := by
    unfold C0hat
    linarith [hlogT2ge, hloglogT2nn]
  -- Ĥ T ≥ 191.85
  have hHlo : (191.85 : ℝ) ≤ Hhat (Real.sqrt 80000 + 1) := by
    unfold Hhat
    have hsq : (5.3248 : ℝ) ^ 2 ≤ C0hat (Real.sqrt 80000 + 1) ^ 2 :=
      pow_le_pow_left₀ (by norm_num) hC0lo 2
    linarith [hsq, hlogT2ge]
  -- e⁴ ≥ 54.5978
  have he4 : (54.5978 : ℝ) ≤ Real.exp 4 := by
    rw [exp_four]
    exact le_trans (by norm_num) (exp_one_pow_ge 4)
  -- assemble
  simp only [Bn]
  -- Z₂ T ≥ 6.06 (0.6·5.6 + 0 + 2.7; log log ≥ 0; the corrected count, D-071)
  have hZ2lo : (6.06 : ℝ) ≤ Z2hat (Real.sqrt 80000 + 1) := by
    unfold Z2hat
    linarith [hlogT2ge, hloglogT2nn]
  have hbrlo : (110.84 : ℝ) ≤ (2 / 3 : ℝ) * Z2hat (Real.sqrt 80000 + 1) +
      10.5 * Real.log (Real.sqrt 80000 + 1 + 2) + 48 := by
    have h1 := mul_le_mul_of_nonneg_left hZ2lo (by norm_num : (0 : ℝ) ≤ 2 / 3)
    have h2 := mul_le_mul_of_nonneg_left hlogT2ge (by norm_num : (0 : ℝ) ≤ 10.5)
    linarith [h1, h2]
  have hterm2 : (4 * 283 * 110.84 : ℝ) ≤ 4 * (Real.sqrt 80000 + 1) *
      ((2 / 3) * Z2hat (Real.sqrt 80000 + 1) +
        10.5 * Real.log (Real.sqrt 80000 + 1 + 2) + 48) := by
    apply mul_le_mul _ hbrlo (by norm_num) (by positivity)
    exact mul_le_mul_of_nonneg_left hTge (by norm_num)
  have hterm4 : (2 * (54.5978 + 1) * (7 * 191.85) : ℝ) ≤
      2 * (Real.exp 4 + 1) * (7 * Hhat (Real.sqrt 80000 + 1)) := by
    apply mul_le_mul _ _ (by norm_num) (by positivity)
    · apply mul_le_mul_of_nonneg_left _ (by norm_num : (0 : ℝ) ≤ 2)
      linarith [he4]
    · linarith [hHlo]
  have hII : (0 : ℝ) ≤ IIMaj 80000 := IIMaj_nonneg 80000
  have hDLnn : (0 : ℝ) ≤ 2 * DogLegRight 80000 := by
    unfold DogLegRight
    have hIIMnn := hII
    positivity
  linarith [hFAlt0, hterm2, hterm4, hII, hDLnn]

/-- [PROVED session 012; target updated session 040 for the D-074
dog-leg repair] Bn FAlt(10⁵) ≤ 352000 (certified ≈ 351 367; true
≈ 333 700 with the dog-leg Bn, E-034's exact Bn_DL = 344 838). -/
theorem Bn_FAlt_100000_le : Bn FAlt 100000 ≤ (352000 : ℝ) := by
  have hT : Real.sqrt 100000 + 1 ≤ 318 := by
    have h := sqrt100000_le
    linarith
  have hTpos : (0 : ℝ) < Real.sqrt 100000 + 1 := by
    have h := Real.sqrt_nonneg 100000
    linarith
  -- log T ≤ 5.8 (T ≤ 318 ≤ e⁵·⁸ = e⁵·e⁰·⁸, 148.328·2.2254 = 330.087)
  have h5 : (148.328 : ℝ) ≤ Real.exp 5 := by
    rw [exp_five]
    exact le_trans (by norm_num) (exp_one_pow_ge 5)
  have h08 : (2.2254 : ℝ) ≤ Real.exp 0.8 :=
    le_trans (by norm_num [Finset.sum_range_succ])
      (Real.sum_le_exp_of_nonneg (by norm_num : (0 : ℝ) ≤ 0.8) 7)
  have h58 : Real.exp 5.8 = Real.exp 5 * Real.exp 0.8 := by
    rw [show (5.8 : ℝ) = 5 + 0.8 by norm_num, Real.exp_add]
  have h58big : (320 : ℝ) ≤ Real.exp 5.8 := by
    rw [h58]
    exact le_trans (by norm_num : (320 : ℝ) ≤ 148.328 * 2.2254)
      (mul_le_mul h5 h08 (by norm_num) (Real.exp_pos _).le)
  have hlogT : Real.log (Real.sqrt 100000 + 1) ≤ (5.8 : ℝ) := by
    have h := Real.log_le_log hTpos (le_trans hT (le_trans (by norm_num :
      (318 : ℝ) ≤ 320) h58big))
    rwa [Real.log_exp] at h
  have hlogT2 : Real.log (Real.sqrt 100000 + 1 + 2) ≤ (5.8 : ℝ) := by
    have hbig : Real.sqrt 100000 + 1 + 2 ≤ Real.exp 5.8 := by
      have h : Real.sqrt 100000 + 1 + 2 ≤ (320 : ℝ) := by linarith
      exact le_trans h h58big
    have hT2pos : (0 : ℝ) < Real.sqrt 100000 + 1 + 2 := by linarith
    have h := Real.log_le_log hT2pos hbig
    rwa [Real.log_exp] at h
  -- log log ≤ 1.77 (log ≤ 5.8 ≤ e¹·⁷⁷ = e·e⁰·⁷⁷, 2.7183·2.1597 = 5.8707)
  have h177 : Real.exp 1.77 = Real.exp 1 * Real.exp 0.77 := by
    rw [show (1.77 : ℝ) = 1 + 0.77 by norm_num, Real.exp_add]
  have h077 : (2.1597 : ℝ) ≤ Real.exp 0.77 :=
    le_trans (by norm_num [Finset.sum_range_succ])
      (Real.sum_le_exp_of_nonneg (by norm_num : (0 : ℝ) ≤ 0.77) 7)
  have h177big : (5.8 : ℝ) ≤ Real.exp 1.77 := by
    rw [h177]
    exact le_trans (by norm_num : (5.8 : ℝ) ≤ 2.7182818283 * 2.1597)
      (mul_le_mul Real.exp_one_gt_d9.le h077 (by norm_num) (Real.exp_pos _).le)
  have hloglogT : Real.log (Real.log (Real.sqrt 100000 + 1)) ≤ (1.77 : ℝ) := by
    have hlogTpos : (0 : ℝ) < Real.log (Real.sqrt 100000 + 1) :=
      Real.log_pos (by linarith [sqrt100000_ge])
    have h := Real.log_le_log hlogTpos (le_trans hlogT h177big)
    rwa [Real.log_exp] at h
  have hloglogT2 : Real.log (Real.log (Real.sqrt 100000 + 1 + 2)) ≤ (1.77 : ℝ) := by
    have hlogT2pos : (0 : ℝ) < Real.log (Real.sqrt 100000 + 1 + 2) :=
      Real.log_pos (by linarith [sqrt100000_ge])
    have h := Real.log_le_log hlogT2pos (le_trans hlogT2 h177big)
    rwa [Real.log_exp] at h
  -- e⁴ ≤ 54.6015
  have he4 : Real.exp 4 ≤ (54.6015 : ℝ) := by
    rw [exp_four]
    exact le_trans (exp_one_pow_le 4) (by norm_num)
  -- 1/(2π) ≤ 1/6
  have h2pi : (1 : ℝ) / (2 * Real.pi) ≤ 1 / 6 := by
    apply one_div_le_one_div_of_le (by norm_num : (0 : ℝ) < 6)
    have hpi := Real.pi_gt_d20.le
    linarith
  -- nonnegativity pieces
  have hlogTnn : (0 : ℝ) ≤ Real.log (Real.sqrt 100000 + 1) :=
    Real.log_nonneg (by linarith [Real.sqrt_nonneg 100000])
  have hlogT2nn : (0 : ℝ) ≤ Real.log (Real.sqrt 100000 + 1 + 2) :=
    Real.log_nonneg (by linarith [Real.sqrt_nonneg 100000])
  have hlogTge1 : (1 : ℝ) ≤ Real.log (Real.sqrt 100000 + 1) := by
    have he : Real.exp 1 ≤ Real.sqrt 100000 + 1 :=
      le_trans Real.exp_one_lt_d9.le (by linarith [sqrt100000_ge])
    have h := Real.log_le_log (Real.exp_pos 1) he
    rwa [Real.log_exp] at h
  have hloglogTnn : (0 : ℝ) ≤ Real.log (Real.log (Real.sqrt 100000 + 1)) :=
    Real.log_nonneg hlogTge1
  have hlogT2ge1 : (1 : ℝ) ≤ Real.log (Real.sqrt 100000 + 1 + 2) := by
    have he : Real.exp 1 ≤ Real.sqrt 100000 + 1 + 2 :=
      le_trans Real.exp_one_lt_d9.le (by linarith [sqrt100000_ge])
    have h := Real.log_le_log (Real.exp_pos 1) he
    rwa [Real.log_exp] at h
  have hloglogT2nn : (0 : ℝ) ≤ Real.log (Real.log (Real.sqrt 100000 + 1 + 2)) :=
    Real.log_nonneg hlogT2ge1
  -- FAlt T ≤ 311.45
  have hFAlt : FAlt (Real.sqrt 100000 + 1) ≤ (311.45 : ℝ) := by
    unfold FAlt
    have hTl : (Real.sqrt 100000 + 1) * Real.log (Real.sqrt 100000 + 1) ≤
        318 * 5.8 :=
      mul_le_mul hT hlogT hlogTnn (by norm_num)
    have ha : (1 / (2 * Real.pi)) * ((Real.sqrt 100000 + 1) *
        Real.log (Real.sqrt 100000 + 1)) ≤ (1 / 6 : ℝ) * (318 * 5.8) :=
      mul_le_mul h2pi hTl (mul_nonneg hTpos.le hlogTnn) (by norm_num)
    linarith [ha, hlogT, hloglogT]
  -- Ĉ₀ T ≤ 6.9797 and ≥ 0
  have hC0 : C0hat (Real.sqrt 100000 + 1) ≤ (6.9797 : ℝ) := by
    unfold C0hat
    linarith [hlogT2, hloglogT2]
  have hC0pos : (0 : ℝ) ≤ C0hat (Real.sqrt 100000 + 1) := by
    unfold C0hat
    linarith [hlogT2nn, hloglogT2nn]
  -- Ĥ T ≤ 255.05 and ≥ 0
  have hH : Hhat (Real.sqrt 100000 + 1) ≤ (255.05 : ℝ) := by
    unfold Hhat
    have hsq : C0hat (Real.sqrt 100000 + 1) ^ 2 ≤ 6.9797 ^ 2 :=
      pow_le_pow_left₀ hC0pos hC0 2
    linarith [hsq, hlogT2]
  have hHnn : (0 : ℝ) ≤ Hhat (Real.sqrt 100000 + 1) := by
    unfold Hhat
    have hsq : (0 : ℝ) ≤ C0hat (Real.sqrt 100000 + 1) ^ 2 := pow_nonneg hC0pos 2
    linarith [hsq, hlogT2nn]
  -- Z₂ T ≤ 7.7483 and ≥ 0 (the corrected I_III count, D-071)
  have hZ2 : Z2hat (Real.sqrt 100000 + 1) ≤ (7.7483 : ℝ) := by
    unfold Z2hat
    linarith [hlogT2, hloglogT2]
  have hZ2nn : (0 : ℝ) ≤ Z2hat (Real.sqrt 100000 + 1) := by
    unfold Z2hat
    linarith [hlogT2nn, hloglogT2nn]
  -- the big bracket: 0 ≤ · ≤ 114.0655
  have hbr : (2 / 3 : ℝ) * Z2hat (Real.sqrt 100000 + 1) +
      10.5 * Real.log (Real.sqrt 100000 + 1 + 2) + 48 ≤ 114.0656 := by
    have h1 := mul_le_mul_of_nonneg_left hZ2 (by norm_num : (0 : ℝ) ≤ 2 / 3)
    have h2 := mul_le_mul_of_nonneg_left hlogT2 (by norm_num : (0 : ℝ) ≤ 10.5)
    linarith [h1, h2]
  have hbrnn : (0 : ℝ) ≤ (2 / 3 : ℝ) * Z2hat (Real.sqrt 100000 + 1) +
      10.5 * Real.log (Real.sqrt 100000 + 1 + 2) + 48 := by
    linarith [hZ2nn, hlogT2nn]
  -- IIMaj ≤ 2900.16
  have hII : IIMaj 100000 ≤ (2900.16 : ℝ) := by
    refine le_trans (IIMaj_le_two_mul 100000 (by norm_num)) ?_
    have h3 : (4.56 : ℝ) * (Real.sqrt 100000 + 1) ≤ 4.56 * 318 :=
      mul_le_mul_of_nonneg_left (by linarith [sqrt100000_le]) (by norm_num)
    linarith [h3]
  -- the dog-leg share (D-074): 2·DogLegRight(10⁵) ≤ 3564 (certified)
  have hDL : 2 * DogLegRight 100000 ≤ (3564 : ℝ) := by
    unfold DogLegRight
    have hT2 : Real.sqrt 100000 + 1 ≤ 318 := hT
    have hII4 : IIMaj 100000 / 4 ≤ (2900.16 : ℝ) / 4 := by linarith [hII]
    have h1 : ((Real.sqrt 100000 + 1) / 2) * (Real.exp (5 / 2) + 1) / 2 ≤
        (318 / 2) * (13.183 : ℝ) / 2 := by
      apply div_le_div_of_nonneg_right _ (by norm_num : (0 : ℝ) ≤ 2)
      apply mul_le_mul _ _ (by positivity) (by positivity)
      · exact div_le_div_of_nonneg_right hT2 (by norm_num : (0 : ℝ) ≤ 2)
      · linarith [exp_five_halves_le]
    linarith [h1, hII4]
  -- assemble
  simp only [Bn]
  have hterm2 : 4 * (Real.sqrt 100000 + 1) * ((2 / 3) * Z2hat (Real.sqrt 100000 + 1) +
      10.5 * Real.log (Real.sqrt 100000 + 1 + 2) + 48) ≤ 4 * 318 * 114.0656 := by
    apply mul_le_mul _ hbr hbrnn (by norm_num)
    exact mul_le_mul_of_nonneg_left hT (by norm_num)
  have hterm4 : 2 * (Real.exp 4 + 1) * (7 * Hhat (Real.sqrt 100000 + 1)) ≤
      2 * (54.6015 + 1) * (7 * 255.05) := by
    apply mul_le_mul _ _ (by linarith [hHnn]) (by norm_num)
    · apply mul_le_mul_of_nonneg_left _ (by norm_num : (0 : ℝ) ≤ 2)
      linarith [he4]
    · linarith [hH]
  linarith [hFAlt, hterm2, hterm4, hDL, hII]

/-! ### 5. The two base points and the final three-hypothesis form -/

/-- [PROVED session 012; values updated session 038 for the D-071
correction] hbase: margiñ(8×10⁴) > 0. Certified: sInftyLower ≥ 336 000,
Bn ≤ 329 000 ⟹ margin ≥ 7 001 (true 14 682 with the corrected Bn). -/
theorem marginTilde_FAlt_80000_pos : 0 < marginTilde FAlt 80000 := by
  rw [marginTilde_eq_sub]
  have hS := sInftyLower_80000_lo
  have hB := Bn_FAlt_80000_le
  linarith

/-- [PROVED session 012; values updated session 038 for the D-071
correction] hbase2: margiñ(8×10⁴) < margiñ(10⁵).
Certified: margiñ(8×10⁴) ≤ 339 000 − 274 000 + 1 = 65 001 and
margiñ(10⁵) ≥ 432 500 − 350 000 + 1 = 82 501. -/
theorem marginTilde_FAlt_80000_lt_100000 :
    marginTilde FAlt 80000 < marginTilde FAlt 100000 := by
  rw [marginTilde_eq_sub, marginTilde_eq_sub]
  have h1 := sInftyLower_80000_up
  have h2 := Bn_FAlt_80000_ge
  have h3 := sInftyLower_100000_lo
  have h4 := Bn_FAlt_100000_le
  linarith

/-- [PROVED session 012 — TIER (ii) STEP 2] R-004, the finite-height Li
theorem, in its final assembly form: machine-verified modulo ONE named
analytic hypothesis (`SfBoundProp`, the traced contour bound) plus the
declared computational perimeter (Platt–Trudgian `RHUpTo`; the finite Li
verification `LiVerifiedUpTo`). The two elementary margin evaluations
are discharged in this file. -/
theorem lambda_pos_finite_height_verified
    (hRH : RHUpTo (3 * 10 ^ 12)) (hfinite : LiVerifiedUpTo (10 ^ 5))
    (hSf : SfBoundProp) :
    ∀ n : ℕ, 1 ≤ n → (n : ℝ) ≤ (3 * 10 ^ 12 - 1 : ℝ) ^ 2 →
      0 < (liCoeff n).re :=
  fun n hn1 hnN => lambda_pos_finite_height hRH hfinite
    marginTilde_FAlt_80000_pos marginTilde_FAlt_80000_lt_100000 hSf n hn1 hnN

end NguyenRH1

end