← Session 17 — Lean tier (i): elementary proofs (after crash)
thinking (168 chars)
`oddHarm_lower` compiles. Piece 5: the main assembly. I'll replace the `sorry` in `sInfty_lower_bound` with the hmain reduction + log identities + both parity branches.
Piece 5: the main assembly — replacing the `sorry` in `sInfty_lower_bound`.
tool: Edit
input
{
"file_path": "D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiSkeleton.lean",
"old_string": "/-- [SKELETON] Archimedean lower bound (draft \u00a73.1 Step 1):\nS_\u221e(n) \u2265 \u00bd n log n + (C\u2081 \u2212 \u03b3/2) n \u2212 4 for n \u2265 20.\nElementary (Bernoulli + explicit harmonic bounds); machine-validated\nagainst exact values for 20 \u2264 n \u2264 5000 (E-021/E-023 V1, min slack 9.52). -/\ntheorem sInfty_lower_bound (n : \u2115) (hn : 20 \u2264 n) :\n (1 / 2) * n * Real.log n +\n (lagariasC1 - Real.eulerMascheroniConstant / 2) * n - 4 \u2264\n SInfty n := by\n sorry",
"new_string": "/-- [PROVED session 011] Archimedean lower bound (draft \u00a73.1 Step 1,\nD-037 \u00a73): S_\u221e(n) \u2265 \u00bd n log n + (C\u2081 \u2212 \u03b3/2) n \u2212 4 for n \u2265 20.\nProof: Bernoulli truncation at K \u2248 n/2 + the two \u03b3-shifted harmonic\nbounds; the \u03b3/log 2/log \u03c0 pieces cancel EXACTLY (parity algebra), and\nthe residual logarithmic defect is \u2264 n/(n\u22121) (even) resp. \u2264 1/2 (odd),\nabsorbed by the \u22124 constant. Machine-validated against exact values for\n20 \u2264 n \u2264 5000 (E-021/E-023 V1, min slack 9.52). -/\ntheorem sInfty_lower_bound (n : \u2115) (hn : 20 \u2264 n) :\n (1 / 2) * n * Real.log n +\n (lagariasC1 - Real.eulerMascheroniConstant / 2) * n - 4 \u2264\n SInfty n := by\n -- reduction to a K-specialized real inequality\n have hmain : \u2200 K : \u2115,\n (1 / 2) * (n : \u211d) * Real.log n +\n (lagariasC1 - Real.eulerMascheroniConstant / 2) * n - 4 \u2264\n (1 - lagariasA1) * (n : \u211d) - 1 +\n ((n : \u211d) * (Real.log (2 * (K : \u211d) + 1) - Real.log ((K : \u211d) + 1) / 2 +\n Real.eulerMascheroniConstant / 2 - 1) - (K : \u211d)) \u2192\n (1 / 2) * (n : \u211d) * Real.log n +\n (lagariasC1 - Real.eulerMascheroniConstant / 2) * n - 4 \u2264\n SInfty n := by\n intro K hK\n have h1 := sInf_partial_lower n K\n have h2 := oddHarm_lower K\n have h3 : (n : \u211d) * (Real.log (2 * (K : \u211d) + 1) - Real.log ((K : \u211d) + 1) / 2 +\n Real.eulerMascheroniConstant / 2 - 1) \u2264 (n : \u211d) * oddHarm K :=\n mul_le_mul_of_nonneg_left h2 (by positivity)\n have h4 : SInfty n = (1 - lagariasA1) * (n : \u211d) - 1 +\n \u2211' m : {m : \u2115 // Odd m \u2227 3 \u2264 m},\n ((1 - 1 / (m : \u211d)) ^ n - 1 + (n : \u211d) / (m : \u211d)) := rfl\n rw [h4]\n linarith [h1, h3]\n -- logarithm identities for the \u03c0-factors\n have h4pi : Real.log (4 * Real.pi) = 2 * Real.log 2 + Real.log Real.pi := by\n rw [Real.log_mul (by norm_num : (4 : \u211d) \u2260 0) Real.pi_ne_zero]\n have e : Real.log (4 : \u211d) = 2 * Real.log 2 := by\n rw [show (4 : \u211d) = 2 ^ 2 by norm_num, Real.log_pow]\n norm_num\n rw [e]\n have h2pi : Real.log (2 * Real.pi) = Real.log 2 + Real.log Real.pi := by\n rw [Real.log_mul (by norm_num : (2 : \u211d) \u2260 0) Real.pi_ne_zero]\n rcases Nat.even_or_odd n with \u27e8q, rfl\u27e9 | \u27e8q, rfl\u27e9\n \u00b7 -- n = q + q, K = q \u2212 1: defect \u2264 n/(n\u22121) \u2264 2 < 4\n have hq10 : 10 \u2264 q := by omega\n have hQ : (10 : \u211d) \u2264 (q : \u211d) := by exact_mod_cast hq10\n refine hmain (q - 1) ?_\n have hN : ((q + q : \u2115) : \u211d) = 2 * (q : \u211d) := by push_cast; ring\n have hK1 : 2 * ((q - 1 : \u2115) : \u211d) + 1 = 2 * (q : \u211d) - 1 := by\n rw [Nat.cast_sub (by omega : 1 \u2264 q), Nat.cast_one]; ring\n have hK2 : ((q - 1 : \u2115) : \u211d) + 1 = (q : \u211d) := by\n rw [Nat.cast_sub (by omega : 1 \u2264 q), Nat.cast_one]; ring\n have hK3 : ((q - 1 : \u2115) : \u211d) = (q : \u211d) - 1 := by\n rw [Nat.cast_sub (by omega : 1 \u2264 q), Nat.cast_one]\n have hlogq : Real.log (q : \u211d) = Real.log (2 * (q : \u211d)) - Real.log 2 := by\n have h := Real.log_mul (by norm_num : (2 : \u211d) \u2260 0)\n (ne_of_gt (by linarith : (0 : \u211d) < (q : \u211d)))\n linarith [h]\n rw [hN, hK1, hK2, hK3, hlogq]\n unfold lagariasA1 lagariasC1\n rw [h4pi, h2pi]\n have hpos : (0 : \u211d) < 2 * (q : \u211d) - 1 := by linarith\n have hlogb1 : Real.log (2 * (q : \u211d)) - Real.log (2 * (q : \u211d) - 1) \u2264\n 1 / (2 * (q : \u211d) - 1) := by\n have h1 := Real.log_le_sub_one_of_pos\n (x := (2 * (q : \u211d)) / (2 * (q : \u211d) - 1)) (div_pos (by linarith) hpos)\n rw [Real.log_div (by linarith : (2 : \u211d) * (q : \u211d) \u2260 0) hpos.ne'] at h1\n have e : (2 * (q : \u211d)) / (2 * (q : \u211d) - 1) - 1 = 1 / (2 * (q : \u211d) - 1) := by\n field_simp [hpos.ne']\n ring\n linarith [h1, e]\n have hlogb2 : (2 * (q : \u211d)) * (Real.log (2 * (q : \u211d)) - Real.log (2 * (q : \u211d) - 1)) \u2264\n 2 := by\n have h2 := mul_le_mul_of_nonneg_left hlogb1 (by linarith : (0 : \u211d) \u2264 2 * (q : \u211d))\n have e : (2 * (q : \u211d)) * (1 / (2 * (q : \u211d) - 1)) \u2264 2 := by\n rw [mul_one_div, div_le_iff\u2080 hpos]\n linarith\n linarith [h2, e]\n linarith [hlogb2]\n \u00b7 -- n = 2q + 1, K = q: defect \u2264 1/2 < 7/2\n have hq10 : 10 \u2264 q := by omega\n have hQ : (10 : \u211d) \u2264 (q : \u211d) := by exact_mod_cast hq10\n refine hmain q ?_\n have hN : ((2 * q + 1 : \u2115) : \u211d) = 2 * (q : \u211d) + 1 := by push_cast; ring\n have hlogq1 : Real.log ((q : \u211d) + 1) = Real.log (2 * (q : \u211d) + 2) - Real.log 2 := by\n have h1 : (2 * (q : \u211d) + 2) = 2 * ((q : \u211d) + 1) := by ring\n have h2 := Real.log_mul (by norm_num : (2 : \u211d) \u2260 0)\n (by positivity : ((q : \u211d) + 1) \u2260 0)\n rw [\u2190 h1] at h2\n linarith [h2]\n rw [hN, hlogq1]\n unfold lagariasA1 lagariasC1\n rw [h4pi, h2pi]\n have hpos : (0 : \u211d) < 2 * (q : \u211d) + 1 := by linarith\n have hlogb1 : Real.log (2 * (q : \u211d) + 2) - Real.log (2 * (q : \u211d) + 1) \u2264\n 1 / (2 * (q : \u211d) + 1) := by\n have h1 := Real.log_le_sub_one_of_pos\n (x := (2 * (q : \u211d) + 2) / (2 * (q : \u211d) + 1)) (div_pos (by linarith) hpos)\n rw [Real.log_div (by linarith : (2 : \u211d) * (q : \u211d) + 2 \u2260 0) hpos.ne'] at h1\n have e : (2 * (q : \u211d) + 2) / (2 * (q : \u211d) + 1) - 1 = 1 / (2 * (q : \u211d) + 1) := by\n field_simp [hpos.ne']\n ring\n linarith [h1, e]\n have hlogb2 : ((2 * (q : \u211d) + 1) / 2) *\n (Real.log (2 * (q : \u211d) + 2) - Real.log (2 * (q : \u211d) + 1)) \u2264 1 / 2 := by\n have h2 := mul_le_mul_of_nonneg_left hlogb1\n (by positivity : (0 : \u211d) \u2264 (2 * (q : \u211d) + 1) / 2)\n have e : ((2 * (q : \u211d) + 1) / 2) * (1 / (2 * (q : \u211d) + 1)) = 1 / 2 := by\n field_simp [hpos.ne']\n ring\n linarith [h2, e]\n linarith [hlogb2]"
}
raw content_json (database row)
[{"type":"thinking","thinking":"`oddHarm_lower` compiles. Piece 5: the main assembly. I'll replace the `sorry` in `sInfty_lower_bound` with the hmain reduction + log identities + both parity branches.","signature":""},{"type":"text","text":"Piece 5: the main assembly — replacing the `sorry` in `sInfty_lower_bound`."},{"type":"tool_use","id":"Edit_73","name":"Edit","input":{"file_path":"D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiSkeleton.lean","old_string":"/-- [SKELETON] Archimedean lower bound (draft §3.1 Step 1):\nS_∞(n) ≥ ½ n log n + (C₁ − γ/2) n − 4 for n ≥ 20.\nElementary (Bernoulli + explicit harmonic bounds); machine-validated\nagainst exact values for 20 ≤ n ≤ 5000 (E-021/E-023 V1, min slack 9.52). -/\ntheorem sInfty_lower_bound (n : ℕ) (hn : 20 ≤ n) :\n (1 / 2) * n * Real.log n +\n (lagariasC1 - Real.eulerMascheroniConstant / 2) * n - 4 ≤\n SInfty n := by\n sorry","new_string":"/-- [PROVED session 011] Archimedean lower bound (draft §3.1 Step 1,\nD-037 §3): S_∞(n) ≥ ½ n log n + (C₁ − γ/2) n − 4 for n ≥ 20.\nProof: Bernoulli truncation at K ≈ n/2 + the two γ-shifted harmonic\nbounds; the γ/log 2/log π pieces cancel EXACTLY (parity algebra), and\nthe residual logarithmic defect is ≤ n/(n−1) (even) resp. ≤ 1/2 (odd),\nabsorbed by the −4 constant. Machine-validated against exact values for\n20 ≤ n ≤ 5000 (E-021/E-023 V1, min slack 9.52). -/\ntheorem sInfty_lower_bound (n : ℕ) (hn : 20 ≤ n) :\n (1 / 2) * n * Real.log n +\n (lagariasC1 - Real.eulerMascheroniConstant / 2) * n - 4 ≤\n SInfty n := by\n -- reduction to a K-specialized real inequality\n have hmain : ∀ K : ℕ,\n (1 / 2) * (n : ℝ) * Real.log n +\n (lagariasC1 - Real.eulerMascheroniConstant / 2) * n - 4 ≤\n (1 - lagariasA1) * (n : ℝ) - 1 +\n ((n : ℝ) * (Real.log (2 * (K : ℝ) + 1) - Real.log ((K : ℝ) + 1) / 2 +\n Real.eulerMascheroniConstant / 2 - 1) - (K : ℝ)) →\n (1 / 2) * (n : ℝ) * Real.log n +\n (lagariasC1 - Real.eulerMascheroniConstant / 2) * n - 4 ≤\n SInfty n := by\n intro K hK\n have h1 := sInf_partial_lower n K\n have h2 := oddHarm_lower K\n have h3 : (n : ℝ) * (Real.log (2 * (K : ℝ) + 1) - Real.log ((K : ℝ) + 1) / 2 +\n Real.eulerMascheroniConstant / 2 - 1) ≤ (n : ℝ) * oddHarm K :=\n mul_le_mul_of_nonneg_left h2 (by positivity)\n have h4 : SInfty n = (1 - lagariasA1) * (n : ℝ) - 1 +\n ∑' m : {m : ℕ // Odd m ∧ 3 ≤ m},\n ((1 - 1 / (m : ℝ)) ^ n - 1 + (n : ℝ) / (m : ℝ)) := rfl\n rw [h4]\n linarith [h1, h3]\n -- logarithm identities for the π-factors\n have h4pi : Real.log (4 * Real.pi) = 2 * Real.log 2 + Real.log Real.pi := by\n rw [Real.log_mul (by norm_num : (4 : ℝ) ≠ 0) Real.pi_ne_zero]\n have e : Real.log (4 : ℝ) = 2 * Real.log 2 := by\n rw [show (4 : ℝ) = 2 ^ 2 by norm_num, Real.log_pow]\n norm_num\n rw [e]\n have h2pi : Real.log (2 * Real.pi) = Real.log 2 + Real.log Real.pi := by\n rw [Real.log_mul (by norm_num : (2 : ℝ) ≠ 0) Real.pi_ne_zero]\n rcases Nat.even_or_odd n with ⟨q, rfl⟩ | ⟨q, rfl⟩\n · -- n = q + q, K = q − 1: defect ≤ n/(n−1) ≤ 2 < 4\n have hq10 : 10 ≤ q := by omega\n have hQ : (10 : ℝ) ≤ (q : ℝ) := by exact_mod_cast hq10\n refine hmain (q - 1) ?_\n have hN : ((q + q : ℕ) : ℝ) = 2 * (q : ℝ) := by push_cast; ring\n have hK1 : 2 * ((q - 1 : ℕ) : ℝ) + 1 = 2 * (q : ℝ) - 1 := by\n rw [Nat.cast_sub (by omega : 1 ≤ q), Nat.cast_one]; ring\n have hK2 : ((q - 1 : ℕ) : ℝ) + 1 = (q : ℝ) := by\n rw [Nat.cast_sub (by omega : 1 ≤ q), Nat.cast_one]; ring\n have hK3 : ((q - 1 : ℕ) : ℝ) = (q : ℝ) - 1 := by\n rw [Nat.cast_sub (by omega : 1 ≤ q), Nat.cast_one]\n have hlogq : Real.log (q : ℝ) = Real.log (2 * (q : ℝ)) - Real.log 2 := by\n have h := Real.log_mul (by norm_num : (2 : ℝ) ≠ 0)\n (ne_of_gt (by linarith : (0 : ℝ) < (q : ℝ)))\n linarith [h]\n rw [hN, hK1, hK2, hK3, hlogq]\n unfold lagariasA1 lagariasC1\n rw [h4pi, h2pi]\n have hpos : (0 : ℝ) < 2 * (q : ℝ) - 1 := by linarith\n have hlogb1 : Real.log (2 * (q : ℝ)) - Real.log (2 * (q : ℝ) - 1) ≤\n 1 / (2 * (q : ℝ) - 1) := by\n have h1 := Real.log_le_sub_one_of_pos\n (x := (2 * (q : ℝ)) / (2 * (q : ℝ) - 1)) (div_pos (by linarith) hpos)\n rw [Real.log_div (by linarith : (2 : ℝ) * (q : ℝ) ≠ 0) hpos.ne'] at h1\n have e : (2 * (q : ℝ)) / (2 * (q : ℝ) - 1) - 1 = 1 / (2 * (q : ℝ) - 1) := by\n field_simp [hpos.ne']\n ring\n linarith [h1, e]\n have hlogb2 : (2 * (q : ℝ)) * (Real.log (2 * (q : ℝ)) - Real.log (2 * (q : ℝ) - 1)) ≤\n 2 := by\n have h2 := mul_le_mul_of_nonneg_left hlogb1 (by linarith : (0 : ℝ) ≤ 2 * (q : ℝ))\n have e : (2 * (q : ℝ)) * (1 / (2 * (q : ℝ) - 1)) ≤ 2 := by\n rw [mul_one_div, div_le_iff₀ hpos]\n linarith\n linarith [h2, e]\n linarith [hlogb2]\n · -- n = 2q + 1, K = q: defect ≤ 1/2 < 7/2\n have hq10 : 10 ≤ q := by omega\n have hQ : (10 : ℝ) ≤ (q : ℝ) := by exact_mod_cast hq10\n refine hmain q ?_\n have hN : ((2 * q + 1 : ℕ) : ℝ) = 2 * (q : ℝ) + 1 := by push_cast; ring\n have hlogq1 : Real.log ((q : ℝ) + 1) = Real.log (2 * (q : ℝ) + 2) - Real.log 2 := by\n have h1 : (2 * (q : ℝ) + 2) = 2 * ((q : ℝ) + 1) := by ring\n have h2 := Real.log_mul (by norm_num : (2 : ℝ) ≠ 0)\n (by positivity : ((q : ℝ) + 1) ≠ 0)\n rw [← h1] at h2\n linarith [h2]\n rw [hN, hlogq1]\n unfold lagariasA1 lagariasC1\n rw [h4pi, h2pi]\n have hpos : (0 : ℝ) < 2 * (q : ℝ) + 1 := by linarith\n have hlogb1 : Real.log (2 * (q : ℝ) + 2) - Real.log (2 * (q : ℝ) + 1) ≤\n 1 / (2 * (q : ℝ) + 1) := by\n have h1 := Real.log_le_sub_one_of_pos\n (x := (2 * (q : ℝ) + 2) / (2 * (q : ℝ) + 1)) (div_pos (by linarith) hpos)\n rw [Real.log_div (by linarith : (2 : ℝ) * (q : ℝ) + 2 ≠ 0) hpos.ne'] at h1\n have e : (2 * (q : ℝ) + 2) / (2 * (q : ℝ) + 1) - 1 = 1 / (2 * (q : ℝ) + 1) := by\n field_simp [hpos.ne']\n ring\n linarith [h1, e]\n have hlogb2 : ((2 * (q : ℝ) + 1) / 2) *\n (Real.log (2 * (q : ℝ) + 2) - Real.log (2 * (q : ℝ) + 1)) ≤ 1 / 2 := by\n have h2 := mul_le_mul_of_nonneg_left hlogb1\n (by positivity : (0 : ℝ) ≤ (2 * (q : ℝ) + 1) / 2)\n have e : ((2 * (q : ℝ) + 1) / 2) * (1 / (2 * (q : ℝ) + 1)) = 1 / 2 := by\n field_simp [hpos.ne']\n ring\n linarith [h2, e]\n linarith [hlogb2]"},"extra_content":null}]