MaxLeafFormal.RSXConst

Source file MaxLeafFormal/RSXConst.lean of the Lean project (how it is built).

import MaxLeafFormal.EncloseH

/-!
# RSX: numerical constants of an earlier version of the paper

These constants belonged to an appendix (algorithm RSX) that was removed from the paper on
2026-10-26. No statement of the current paper uses this module; it stays in the build unchanged.
-/

namespace MaxLeafFormal.RSXConst

open Enclose

/-- `b_k(p) = (1-p)² (1 - (1-p)^k)`. -/
noncomputable def bk (k : ℕ) (p : ℝ) : ℝ := (1 - p)^2 * (1 - (1 - p)^k)

/-- `ψ̃_k(p) = (1-p)(1 - (1-p)^(k+1) - (k+1) p (1-p)^k)`. -/
noncomputable def psik (k : ℕ) (p : ℝ) : ℝ := (1 - p) * (1 - (1 - p)^(k+1) - (k+1) * p * (1 - p)^k)

/-- `ω = log 1.7150 - 10⁻¹⁰`. -/
noncomputable def ωm : ℝ := Real.logb 2 (343/200) - 1/10^10

/-- The closed forms used by the program. -/
theorem psik_one (p : ℝ) : psik 1 p = (1 - p) * p^2 := by
  unfold psik
  push_cast
  ring

theorem psik_two (p : ℝ) : psik 2 p = (1 - p) * p^2 * (3 - 2 * p) := by
  unfold psik
  push_cast
  ring

lemma rat_le_real {q r : ℚ} (h : q ≤ r) : (q : ℝ) ≤ (r : ℝ) := by exact_mod_cast h

theorem rsx_C1 : ∀ p ∈ Set.Icc (0:ℝ) 1,
    bk 1 p ≤ 4/27 ∧ bk 2 p ≤ 1/4 ∧ bk 3 p ≤ 33/100 ∧ psik 1 p ≤ 4/27 ∧ psik 2 p ≤ 26/100 := by
  intro p hp
  obtain ⟨hp0, hp1⟩ := hp
  have hq : 0 ≤ 1 - p := by linarith
  refine ⟨?_, ?_, ?_, ?_, ?_⟩
  · -- 4/27 - p (1-p)^2 = (p - 1/3)^2 (4/3 - p)
    unfold bk
    nlinarith [mul_nonneg (sq_nonneg (p - 1/3)) (by linarith : (0:ℝ) ≤ 4/3 - p)]
  · -- u (1 - u) with u = (1-p)^2
    unfold bk
    nlinarith [sq_nonneg ((1 - p)^2 - 1/2)]
  · -- with q = 1 - p: 33/100 - q^2 + q^5 = (q - 737/1000)^2 Q(q) + L(q),
    -- Q(q) = q^3 + 1.474 q^2 + 1.6295 q + 0.6013 > 0, L linear and positive on [0,1]
    unfold bk
    nlinarith [mul_nonneg (pow_nonneg hq 3) (sq_nonneg ((1 - p) - 737/1000)),
      mul_nonneg (pow_nonneg hq 2) (sq_nonneg ((1 - p) - 737/1000)),
      mul_nonneg hq (sq_nonneg ((1 - p) - 737/1000)),
      sq_nonneg ((1 - p) - 737/1000)]
  · rw [psik_one]
    -- 4/27 - p^2 (1-p) = (p - 2/3)^2 (p + 1/3)
    nlinarith [mul_nonneg (sq_nonneg (p - 2/3)) (by linarith : (0:ℝ) ≤ p + 1/3)]
  · rw [psik_two]
    -- 26/100 - psik 2 = (p - r)^2 Q(p) + L(p) with r = 578465/10^6,
    -- Q(p) = γ(1-p) + δ p + 2 p (1-p) with γ, δ > 0, L linear and positive on [0,1]
    nlinarith [mul_nonneg (sq_nonneg (p - 578465/1000000)) hq,
      mul_nonneg (sq_nonneg (p - 578465/1000000)) hp0,
      mul_nonneg (mul_nonneg (sq_nonneg (p - 578465/1000000)) hp0) hq]

theorem rsx_C2 :
    (6 + 3*(4/27) + 1/8 + 33/100 : ℚ) ≤ 69/10 ∧ (3*(4/27) + 13/100 + 6 : ℚ) ≤ 658/100 ∧
    (3/8 + 5 : ℚ) = 5375/1000 ∧ (13/100 + 5 : ℚ) ≤ 513/100 ∧ (1/3 + 658/100 + 513/100 : ℚ) ≤ 1205/100 ∧
    (1/3 : ℝ) * (1 + Real.logb 2 (Real.exp 1) + Real.logb 2 (3 + 1/60)) ≤ 149/100 ∧
    (1 + 149/100 + 5375/1000 : ℚ) ≤ 787/100 ∧ (787/100 : ℚ) ≤ 1205/100 ∧
    ((4 - 3*(15/100)) / (15/100) : ℚ) ≤ 2367/100 ∧ (2 + 79/10 + 2367/100 : ℚ) ≤ 50 ∧
    (2 + 11 + 1205/100 + 2367/100 : ℚ) = 4872/100 := by
  have hlog : (1/3 : ℝ) * (1 + Real.logb 2 (Real.exp 1) + Real.logb 2 (3 + 1/60)) ≤ 149/100 := by
    have he : Real.logb 2 (Real.exp 1) = 1 / Real.log 2 := by
      rw [Real.logb, Real.log_exp]
    have hln2 : (0.6931471803 : ℝ) < Real.log 2 := Real.log_two_gt_d9
    have hinv : 1 / Real.log 2 ≤ 14427/10000 := by
      rw [div_le_iff₀ (by linarith)]
      nlinarith
    have hL : Real.logb 2 (3 + 1/60) ≤ 16/10 := by
      obtain ⟨_, h2⟩ := log2Q_sound (q := 181/60) (by norm_num) 60 80
      have hb : (log2Q (181/60) 60 80).hi ≤ 16/10 := by decide +kernel
      have hb' := rat_le_real hb; push_cast at hb'
      have e : ((181/60 : ℚ) : ℝ) = 3 + 1/60 := by norm_num
      rw [e] at h2
      linarith
    rw [he]
    linarith
  refine ⟨by norm_num, by norm_num, by norm_num, by norm_num, by norm_num, hlog,
    by norm_num, by norm_num, by norm_num, by norm_num, by norm_num⟩

theorem rsx_C3 : MLS.H2 (1501/10000) < ωm ∧ MLS.H2 (4/5) < ωm ∧ (1 - ωm) * 59 + 1 ≤ 50 := by
  have hW : (76/100 : ℝ) ≤ ωm := by
    obtain ⟨h1, _⟩ := log2Q_sound (q := 343/200) (by norm_num) 60 80
    have e : ((343/200 : ℚ) : ℝ) = 343/200 := by norm_num
    rw [e] at h1
    have hlo : (77/100 : ℚ) ≤ (log2Q (343/200) 60 80).lo := by decide +kernel
    have hlo' := rat_le_real hlo; push_cast at hlo'
    unfold ωm
    norm_num at h1 ⊢
    linarith
  have hH1 : MLS.H2 (1501/10000) < ωm := by
    obtain ⟨_, h2⟩ := H2Q_sound (x := 1501/10000) (by norm_num) (by norm_num) 60 80
    have e : ((1501/10000 : ℚ) : ℝ) = 1501/10000 := by norm_num
    rw [e] at h2
    have hb : (H2Q (1501/10000) 60 80).hi ≤ 7/10 := by decide +kernel
    have hb' := rat_le_real hb; push_cast at hb'
    linarith
  have hH2 : MLS.H2 (4/5) < ωm := by
    obtain ⟨_, h2⟩ := H2Q_sound (x := 4/5) (by norm_num) (by norm_num) 60 80
    have e : ((4/5 : ℚ) : ℝ) = 4/5 := by norm_num
    rw [e] at h2
    have hb : (H2Q (4/5) 60 80).hi ≤ 75/100 := by decide +kernel
    have hb' := rat_le_real hb; push_cast at hb'
    linarith
  refine ⟨hH1, hH2, ?_⟩
  linarith

end MaxLeafFormal.RSXConst
Back to top