← Session 18 — Lean tier (ii): finite-height proof + certified base points
Now the main theorem: swap the derivative hypothesis for the second evaluation point.
tool: Edit
input
{
"file_path": "D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiSkeleton.lean",
"old_string": "/-- [PROVED session 012 \u2014 TIER (ii) STEP 1, assembly modulo `SfBoundProp`]\nR-004, the finite-height Li theorem (draft Thm 3.1): assuming the named\nanalytic hypothesis `SfBoundProp`, the computational perimeter\n(Platt\u2013Trudgian RH-to-T\u2080, finite Li verification to 5\u00d710\u2075), and the two\nelementary base-point evaluations (E-028/E-029 values; interval-bound\ndischarge = tier (ii) step 2), \u03bb_n > 0 for all n \u2264 (T\u2080\u22121)\u00b2.\n\nProof: for n < 8\u00d710\u2074 use the perimeter finite verification; for\nn \u2265 8\u00d710\u2074, \u03bb_n = S_\u221e(n) \u2212 S_f(n) + 1 \u2265 sInftyLower(n) \u2212 B(n) + 1\n= margin\u0303(n) > 0 by convexity (`marginTilde_convex` + `FAlt_psi_neg`)\nand the base point (`pos_of_convex_of_base`).\n`_hRH` documents the bridge input: it is consumed by `SfBoundProp`'s\neventual proof (D-037 \u00a76), not by the assembly itself. -/\ntheorem lambda_pos_finite_height\n (_hRH : RHUpTo (3 * 10 ^ 12)) (hfinite : LiVerifiedUpTo (5 * 10 ^ 5))\n (hbase : 0 < marginTilde FAlt 80000)\n (hbase' : 0 < deriv (marginTilde FAlt) 80000)\n (hSf : SfBoundProp) :\n \u2200 n : \u2115, 1 \u2264 n \u2192 (n : \u211d) \u2264 (3 * 10 ^ 12 - 1 : \u211d) ^ 2 \u2192\n 0 < (liCoeff n).re := by\n intro n hn1 hnN\n rcases lt_or_ge n 80000 with hlt | hge\n \u00b7 exact hfinite n hn1 (by omega)\n \u00b7 have hn20 : 20 \u2264 n := by omega\n have h1 := sInfty_lower_bound n hn20\n have h2 := hSf n hge hnN\n have h3 : (liCoeff n).re = SInfty n - Sf n + 1 := by\n unfold Sf\n ring\n have h4 : marginTilde FAlt (n : \u211d) = sInftyLower (n : \u211d) - Bn FAlt (n : \u211d) + 1 :=\n marginTilde_eq_sub FAlt n\n have hdiffM : \u2200 y : \u211d, y \u2208 Set.Ioi 20 \u2192\n DifferentiableAt \u211d (marginTilde FAlt) y := by\n intro y hy\n rw [marginTilde_eq_expanded FAlt]\n exact ((contDiffOn_marginExpanded FAlt contDiffOn_FAlt).differentiableOn\n (by norm_num)).differentiableAt (Ioi_mem_nhds hy)\n have h5 : 0 < marginTilde FAlt (n : \u211d) :=\n pos_of_convex_of_base\n (marginTilde_convex FAlt contDiffOn_FAlt FAlt_psi_neg)\n hdiffM (by norm_num) (by exact_mod_cast hge) hbase hbase'\n have habs : Sf n \u2264 |Sf n| := le_abs_self _\n rw [h3]\n linarith [h1, h2, h4, h5, habs]\nend NguyenRH1",
"new_string": "/-- [PROVED session 012 \u2014 TIER (ii) STEP 1, assembly modulo `SfBoundProp`]\nR-004, the finite-height Li theorem (draft Thm 3.1): assuming the named\nanalytic hypothesis `SfBoundProp`, the computational perimeter\n(Platt\u2013Trudgian RH-to-T\u2080, finite Li verification to 5\u00d710\u2075), and two\nelementary evaluations of the explicit margin function (E-028/E-029\nvalues: margin\u0303(8\u00d710\u2074) \u2248 1.58\u00d710\u2074 > 0 and margin\u0303(10\u2075) \u2248 9.3\u00d710\u2074\n> margin\u0303(8\u00d710\u2074); interval-bound discharge = tier (ii) step 2),\n\u03bb_n > 0 for all n \u2264 (T\u2080\u22121)\u00b2.\n\nProof: for n < 10\u2075 use the perimeter finite verification; for\nn \u2265 10\u2075, \u03bb_n = S_\u221e(n) \u2212 S_f(n) + 1 \u2265 sInftyLower(n) \u2212 B(n) + 1\n= margin\u0303(n) > 0 by convexity (`marginTilde_convex` + `FAlt_psi_neg`)\nand the two base points (`pos_of_convex_of_two_points`).\n`_hRH` documents the bridge input: it is consumed by `SfBoundProp`'s\neventual proof (D-037 \u00a76), not by the assembly itself. -/\ntheorem lambda_pos_finite_height\n (_hRH : RHUpTo (3 * 10 ^ 12)) (hfinite : LiVerifiedUpTo (5 * 10 ^ 5))\n (hbase : 0 < marginTilde FAlt 80000)\n (hbase2 : marginTilde FAlt 80000 < marginTilde FAlt 100000)\n (hSf : SfBoundProp) :\n \u2200 n : \u2115, 1 \u2264 n \u2192 (n : \u211d) \u2264 (3 * 10 ^ 12 - 1 : \u211d) ^ 2 \u2192\n 0 < (liCoeff n).re := by\n intro n hn1 hnN\n rcases lt_or_ge n 100000 with hlt | hge\n \u00b7 exact hfinite n hn1 (by omega)\n \u00b7 have hn20 : 20 \u2264 n := by omega\n have h1 := sInfty_lower_bound n hn20\n have h2 := hSf n hge hnN\n have h3 : (liCoeff n).re = SInfty n - Sf n + 1 := by\n unfold Sf\n ring\n have h4 : marginTilde FAlt (n : \u211d) = sInftyLower (n : \u211d) - Bn FAlt (n : \u211d) + 1 :=\n marginTilde_eq_sub FAlt n\n have h5 : 0 < marginTilde FAlt (n : \u211d) :=\n pos_of_convex_of_two_points\n (marginTilde_convex FAlt contDiffOn_FAlt FAlt_psi_neg)\n (by norm_num) (by norm_num) (by exact_mod_cast hge) hbase hbase2\n have habs : Sf n \u2264 |Sf n| := le_abs_self _\n rw [h3]\n linarith [h1, h2, h4, h5, habs]\nend NguyenRH1"
}
raw content_json (database row)
[{"type":"text","text":"Now the main theorem: swap the derivative hypothesis for the second evaluation point."},{"type":"tool_use","id":"Edit_84","name":"Edit","input":{"file_path":"D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiSkeleton.lean","old_string":"/-- [PROVED session 012 — TIER (ii) STEP 1, assembly modulo `SfBoundProp`]\nR-004, the finite-height Li theorem (draft Thm 3.1): assuming the named\nanalytic hypothesis `SfBoundProp`, the computational perimeter\n(Platt–Trudgian RH-to-T₀, finite Li verification to 5×10⁵), and the two\nelementary base-point evaluations (E-028/E-029 values; interval-bound\ndischarge = tier (ii) step 2), λ_n > 0 for all n ≤ (T₀−1)².\n\nProof: for n < 8×10⁴ use the perimeter finite verification; for\nn ≥ 8×10⁴, λ_n = S_∞(n) − S_f(n) + 1 ≥ sInftyLower(n) − B(n) + 1\n= margiñ(n) > 0 by convexity (`marginTilde_convex` + `FAlt_psi_neg`)\nand the base point (`pos_of_convex_of_base`).\n`_hRH` documents the bridge input: it is consumed by `SfBoundProp`'s\neventual proof (D-037 §6), not by the assembly itself. -/\ntheorem lambda_pos_finite_height\n (_hRH : RHUpTo (3 * 10 ^ 12)) (hfinite : LiVerifiedUpTo (5 * 10 ^ 5))\n (hbase : 0 < marginTilde FAlt 80000)\n (hbase' : 0 < deriv (marginTilde FAlt) 80000)\n (hSf : SfBoundProp) :\n ∀ n : ℕ, 1 ≤ n → (n : ℝ) ≤ (3 * 10 ^ 12 - 1 : ℝ) ^ 2 →\n 0 < (liCoeff n).re := by\n intro n hn1 hnN\n rcases lt_or_ge n 80000 with hlt | hge\n · exact hfinite n hn1 (by omega)\n · have hn20 : 20 ≤ n := by omega\n have h1 := sInfty_lower_bound n hn20\n have h2 := hSf n hge hnN\n have h3 : (liCoeff n).re = SInfty n - Sf n + 1 := by\n unfold Sf\n ring\n have h4 : marginTilde FAlt (n : ℝ) = sInftyLower (n : ℝ) - Bn FAlt (n : ℝ) + 1 :=\n marginTilde_eq_sub FAlt n\n have hdiffM : ∀ y : ℝ, y ∈ Set.Ioi 20 →\n DifferentiableAt ℝ (marginTilde FAlt) y := by\n intro y hy\n rw [marginTilde_eq_expanded FAlt]\n exact ((contDiffOn_marginExpanded FAlt contDiffOn_FAlt).differentiableOn\n (by norm_num)).differentiableAt (Ioi_mem_nhds hy)\n have h5 : 0 < marginTilde FAlt (n : ℝ) :=\n pos_of_convex_of_base\n (marginTilde_convex FAlt contDiffOn_FAlt FAlt_psi_neg)\n hdiffM (by norm_num) (by exact_mod_cast hge) hbase hbase'\n have habs : Sf n ≤ |Sf n| := le_abs_self _\n rw [h3]\n linarith [h1, h2, h4, h5, habs]\nend NguyenRH1","new_string":"/-- [PROVED session 012 — TIER (ii) STEP 1, assembly modulo `SfBoundProp`]\nR-004, the finite-height Li theorem (draft Thm 3.1): assuming the named\nanalytic hypothesis `SfBoundProp`, the computational perimeter\n(Platt–Trudgian RH-to-T₀, finite Li verification to 5×10⁵), and two\nelementary evaluations of the explicit margin function (E-028/E-029\nvalues: margiñ(8×10⁴) ≈ 1.58×10⁴ > 0 and margiñ(10⁵) ≈ 9.3×10⁴\n> margiñ(8×10⁴); interval-bound discharge = tier (ii) step 2),\nλ_n > 0 for all n ≤ (T₀−1)².\n\nProof: for n < 10⁵ use the perimeter finite verification; for\nn ≥ 10⁵, λ_n = S_∞(n) − S_f(n) + 1 ≥ sInftyLower(n) − B(n) + 1\n= margiñ(n) > 0 by convexity (`marginTilde_convex` + `FAlt_psi_neg`)\nand the two base points (`pos_of_convex_of_two_points`).\n`_hRH` documents the bridge input: it is consumed by `SfBoundProp`'s\neventual proof (D-037 §6), not by the assembly itself. -/\ntheorem lambda_pos_finite_height\n (_hRH : RHUpTo (3 * 10 ^ 12)) (hfinite : LiVerifiedUpTo (5 * 10 ^ 5))\n (hbase : 0 < marginTilde FAlt 80000)\n (hbase2 : marginTilde FAlt 80000 < marginTilde FAlt 100000)\n (hSf : SfBoundProp) :\n ∀ n : ℕ, 1 ≤ n → (n : ℝ) ≤ (3 * 10 ^ 12 - 1 : ℝ) ^ 2 →\n 0 < (liCoeff n).re := by\n intro n hn1 hnN\n rcases lt_or_ge n 100000 with hlt | hge\n · exact hfinite n hn1 (by omega)\n · have hn20 : 20 ≤ n := by omega\n have h1 := sInfty_lower_bound n hn20\n have h2 := hSf n hge hnN\n have h3 : (liCoeff n).re = SInfty n - Sf n + 1 := by\n unfold Sf\n ring\n have h4 : marginTilde FAlt (n : ℝ) = sInftyLower (n : ℝ) - Bn FAlt (n : ℝ) + 1 :=\n marginTilde_eq_sub FAlt n\n have h5 : 0 < marginTilde FAlt (n : ℝ) :=\n pos_of_convex_of_two_points\n (marginTilde_convex FAlt contDiffOn_FAlt FAlt_psi_neg)\n (by norm_num) (by norm_num) (by exact_mod_cast hge) hbase hbase2\n have habs : Sf n ≤ |Sf n| := le_abs_self _\n rw [h3]\n linarith [h1, h2, h4, h5, habs]\nend NguyenRH1"},"extra_content":null}]