← Session 14 — Phase 5 kickoff: paper draft + honesty audit
thinking (143 chars)
`completedRiemannZeta` is root-level ✓, `RiemannHypothesis` root-level ✓, `Real.eulerMascheroniConstant` ✓. Now write the three skeleton files.
All names verified. Writing the three skeleton files.
tool: Write
input
{
"file_path": "D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiSkeleton.lean",
"content": "/-\nNguyenRH1/LiSkeleton.lean \u2014 [SKELETON] statement-level formalization of\npaper draft.tex \u00a73.1 (R-004 finite-height Li theorem + archimedean lower\nbound + margin convexity mechanism).\n\nConventions follow zeta-23-lean's hypothesis-driven style (cf. Zeta23.Final):\nthe computational inputs (Platt\u2013Trudgian RH-to-height; finite Li\nverification) are named Prop hypotheses, exactly as Zeta23 treats hEF/hRvM.\n\nAll proofs are `sorry` at this stage BY DESIGN (task 5.1 first pass:\nmachine-checked statements). `#print axioms` shows `sorryAx` until the\nproofs are filled in; no new axioms are introduced anywhere.\n\nArchive references: R-004, D-037, D-056, D-057, E-023, E-028, E-029.\n-/\nimport Mathlib\nimport Zeta23.Statement\n\nopen Zeta23 Complex\n\nnoncomputable section\n\nnamespace NguyenRH1\n\n/-! ## 1. The Keiper\u2013Li coefficients -/\n\n/-- The Keiper\u2013Li coefficient \u03bb_n as the zero-side sum with multiplicity\n(draft \u00a73.1; Zeta23's IsNontrivialZero/zeroMult conventions).\nNOTE (honesty): `tsum` of a non-summable family is 0 in Lean, so the\nSUMMABILITY of this family is part of the mathematical content to be\nformalized (it follows from \u03a3 |\u03c1|\u207b\u00b2 < \u221e and |1\u2212(1\u22121/\u03c1)\u207f| = O(n/|\u03c1|)). -/\ndef liCoeff (n : \u2115) : \u2102 :=\n tsum fun \u03c1 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1} =>\n (zeroMult \u03c1 : \u2102) * (1 - (1 - 1 / (\u03c1 : \u2102)) ^ n)\n\n/-- \"RH verified to height T\u2080\": every nontrivial zero with |Im \u03c1| \u2264 T\u2080 is\non the critical line. Platt\u2013Trudgian 2021 (interval arithmetic) is the\nT\u2080 = 3\u00d710\u00b9\u00b2 instance; treated here as a hypothesis, mirroring Zeta23's\nliterature-hypothesis style. -/\ndef RHUpTo (T\u2080 : \u211d) : Prop :=\n \u2200 \u03c1 : \u2102, IsNontrivialZero \u03c1 \u2192 |\u03c1.im| \u2264 T\u2080 \u2192 \u03c1.re = 1 / 2\n\n/-- \"Li coefficients verified positive up to N\" (computational input:\nthis project to N = 3000 (E-011/E-015, two independent methods);\nMisguich\u2013Voros to N = 5\u00d710\u2075). \u03bb_n is real (conjugate symmetry of the\nzero set); the skeleton states positivity of the real part. -/\ndef LiVerifiedUpTo (N : \u2115) : Prop :=\n \u2200 n : \u2115, 1 \u2264 n \u2192 n \u2264 N \u2192 0 < (liCoeff n).re\n\n/-- [SKELETON] R-004, the finite-height Li theorem (draft Thm 3.1):\nassuming RH verified to T\u2080 = 3\u00d710\u00b9\u00b2 and finite Li verification to\n5\u00d710\u2075, \u03bb_n > 0 for all n \u2264 (T\u2080\u22121)\u00b2 \u2248 9.0\u00d710\u00b2\u2074.\nProof content to formalize: D-037 assembly (archimedean lower bound +\ntraced contour bound + bridge + margin argument). -/\ntheorem lambda_pos_finite_height\n (hRH : RHUpTo (3 * 10 ^ 12)) (hfinite : LiVerifiedUpTo (5 * 10 ^ 5)) :\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 sorry\n\n/-! ## 2. The archimedean lower bound (D-037 Step 1) -/\n\n/-- a\u2081 = (log 4\u03c0 + \u03b3)/2, the j = 1 Lagarias coefficient. -/\ndef lagariasA1 : \u211d := (Real.log (4 * Real.pi) + Real.eulerMascheroniConstant) / 2\n\n/-- S_\u221e(n) in the exact odd-m identity form (D-037):\nS_\u221e(n) = (1\u2212a\u2081)n \u2212 1 + \u03a3_{m \u2265 3, odd} [(1\u22121/m)\u207f \u2212 1 + n/m].\n(Same tsum-summability honesty note as liCoeff.) -/\ndef SInfty (n : \u2115) : \u211d :=\n (1 - lagariasA1) * n - 1 +\n tsum fun m : {m : \u2115 // Odd m \u2227 3 \u2264 m} =>\n ((1 - 1 / (m : \u211d)) ^ n - 1 + (n : \u211d) / (m : \u211d))\n\n/-- C\u2081 = (\u03b3 \u2212 1 \u2212 log 2\u03c0)/2 (D-037). -/\ndef lagariasC1 : \u211d :=\n (Real.eulerMascheroniConstant - 1 - Real.log (2 * Real.pi)) / 2\n\n/-- [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\n\n/-! ## 3. The margin and its convexity (D-057) -/\n\n/-- The honest closed-form unit-interval zero-count majorant (D-056 \u00a72):\n\u0108\u2080(t) = 0.433 log(t+2) + 0.886 log log(t+2) + 2.9. -/\ndef C0hat (t : \u211d) : \u211d :=\n 0.433 * Real.log (t + 2) + 0.886 * Real.log (Real.log (t + 2)) + 2.9\n\n/-- H majorant with A = 10.5, B\u2080 = 48 (D-056). -/\ndef Hhat (T : \u211d) : \u211d :=\n 3 * C0hat T ^ 2 + 10.5 * Real.log (T + 2) + 48\n\n/-- The I_I boundary-integral majorant (D-057 \u00a73):\nB\u0303\u2084(n) = 2(\u221an+1)\u00b7(e^{\u221an/2}+1)\u00b70.57\u00b72^{\u2212(2\u221an\u22122)}. -/\ndef IIMaj (n : \u211d) : \u211d :=\n 2 * (Real.sqrt n + 1) * (Real.exp (Real.sqrt n / 2) + 1) * 0.57 *\n 2 ^ (-(2 * Real.sqrt n - 2))\n\n/-- The margin majorant chain (D-057): margin\u0303(n) = S(n) \u2212 B\u0303(n) + 1 with\nthe counting function majorized by a smooth function F (the explicit\nTrudgian N(T) majorant is part of the formalization content and enters\nhere as a parameter with its majorant property as a hypothesis).\nM\u2080 = 1.3352 (E-023, grid-verified \u2014 see D-060 \u00a74 for its status). -/\ndef marginTilde (F : \u211d \u2192 \u211d) (n : \u211d) : \u211d :=\n let T := Real.sqrt n + 1\n ((1 / 2) * n * Real.log n +\n (lagariasC1 - Real.eulerMascheroniConstant / 2) * n - 4) -\n (2 * F T + 4 * T * ((2 / 3) * C0hat T + 10.5 * Real.log (T + 2) + 48) +\n 40 * 1.3352 + 2 * (Real.exp 4 + 1) * (7 * Hhat T + 3.3) +\n IIMaj n + 1) + 1\n\n/-- [SKELETON] Margin convexity (D-057, draft \u00a73.1 Step 4): for any\ntwice-differentiable majorant F of the zero count N(0,T] whose\n\u03c8-block \u03c8[F](T) = F\u2033(T) \u2212 F\u2032(T)/(T\u22121) is negative for T \u2265 \u221a20 + 1\n(the D-057 11-block table discharges this for the explicit Trudgian\nmajorant), the margin majorant margin\u0303 is convex on [20, \u221e).\nTogether with margin\u0303(8\u00d710\u2074) = 16 020 > 0 and margin\u0303\u2032(8\u00d710\u2074) > 0\n(E-028/E-029) this gives margin > 0 on [8\u00d710\u2074, N\u2081]. -/\ntheorem marginTilde_convex (F : \u211d \u2192 \u211d) (hF : ContDiff \u211d 2 F)\n (hmaj : \u2200 T : \u211d, (Ncount 0 T : \u211d) \u2264 F T)\n (h\u03c8 : \u2200 T : \u211d, Real.sqrt 20 + 1 \u2264 T \u2192\n deriv (deriv F) T - deriv F T / (T - 1) < 0) :\n ConvexOn \u211d (Set.Ici 20) (marginTilde F) := by\n sorry\n\n/-- [SKELETON] The D-057 chain-rule identity behind the 11-block\nreduction: with T(n) = \u221an + 1,\nd\u00b2/dn\u00b2 \u03c6(T(n)) = [\u03c6\u2033(T) \u2212 \u03c6\u2032(T)/(T\u22121)] / (4n). -/\ntheorem chain_rule_sqrt_shift (\u03c6 : \u211d \u2192 \u211d) (h\u03c6 : ContDiff \u211d 2 \u03c6)\n (n : \u211d) (hn : 0 < n) :\n deriv (deriv fun n => \u03c6 (Real.sqrt n + 1)) n =\n (deriv (deriv \u03c6) (Real.sqrt n + 1) -\n deriv \u03c6 (Real.sqrt n + 1) / Real.sqrt n) / (4 * n) := by\n sorry\n\nend\n\nend NguyenRH1\n"
}
raw content_json (database row)
[{"type":"thinking","thinking":"`completedRiemannZeta` is root-level ✓, `RiemannHypothesis` root-level ✓, `Real.eulerMascheroniConstant` ✓. Now write the three skeleton files.","signature":""},{"type":"text","text":"All names verified. Writing the three skeleton files."},{"type":"tool_use","id":"Write_91","name":"Write","input":{"file_path":"D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiSkeleton.lean","content":"/-\nNguyenRH1/LiSkeleton.lean — [SKELETON] statement-level formalization of\npaper draft.tex §3.1 (R-004 finite-height Li theorem + archimedean lower\nbound + margin convexity mechanism).\n\nConventions follow zeta-23-lean's hypothesis-driven style (cf. Zeta23.Final):\nthe computational inputs (Platt–Trudgian RH-to-height; finite Li\nverification) are named Prop hypotheses, exactly as Zeta23 treats hEF/hRvM.\n\nAll proofs are `sorry` at this stage BY DESIGN (task 5.1 first pass:\nmachine-checked statements). `#print axioms` shows `sorryAx` until the\nproofs are filled in; no new axioms are introduced anywhere.\n\nArchive references: R-004, D-037, D-056, D-057, E-023, E-028, E-029.\n-/\nimport Mathlib\nimport Zeta23.Statement\n\nopen Zeta23 Complex\n\nnoncomputable section\n\nnamespace NguyenRH1\n\n/-! ## 1. The Keiper–Li coefficients -/\n\n/-- The Keiper–Li coefficient λ_n as the zero-side sum with multiplicity\n(draft §3.1; Zeta23's IsNontrivialZero/zeroMult conventions).\nNOTE (honesty): `tsum` of a non-summable family is 0 in Lean, so the\nSUMMABILITY of this family is part of the mathematical content to be\nformalized (it follows from Σ |ρ|⁻² < ∞ and |1−(1−1/ρ)ⁿ| = O(n/|ρ|)). -/\ndef liCoeff (n : ℕ) : ℂ :=\n tsum fun ρ : {ρ : ℂ // IsNontrivialZero ρ} =>\n (zeroMult ρ : ℂ) * (1 - (1 - 1 / (ρ : ℂ)) ^ n)\n\n/-- \"RH verified to height T₀\": every nontrivial zero with |Im ρ| ≤ T₀ is\non the critical line. Platt–Trudgian 2021 (interval arithmetic) is the\nT₀ = 3×10¹² instance; treated here as a hypothesis, mirroring Zeta23's\nliterature-hypothesis style. -/\ndef RHUpTo (T₀ : ℝ) : Prop :=\n ∀ ρ : ℂ, IsNontrivialZero ρ → |ρ.im| ≤ T₀ → ρ.re = 1 / 2\n\n/-- \"Li coefficients verified positive up to N\" (computational input:\nthis project to N = 3000 (E-011/E-015, two independent methods);\nMisguich–Voros to N = 5×10⁵). λ_n is real (conjugate symmetry of the\nzero set); the skeleton states positivity of the real part. -/\ndef LiVerifiedUpTo (N : ℕ) : Prop :=\n ∀ n : ℕ, 1 ≤ n → n ≤ N → 0 < (liCoeff n).re\n\n/-- [SKELETON] R-004, the finite-height Li theorem (draft Thm 3.1):\nassuming RH verified to T₀ = 3×10¹² and finite Li verification to\n5×10⁵, λ_n > 0 for all n ≤ (T₀−1)² ≈ 9.0×10²⁴.\nProof content to formalize: D-037 assembly (archimedean lower bound +\ntraced contour bound + bridge + margin argument). -/\ntheorem lambda_pos_finite_height\n (hRH : RHUpTo (3 * 10 ^ 12)) (hfinite : LiVerifiedUpTo (5 * 10 ^ 5)) :\n ∀ n : ℕ, 1 ≤ n → (n : ℝ) ≤ (3 * 10 ^ 12 - 1 : ℝ) ^ 2 →\n 0 < (liCoeff n).re := by\n sorry\n\n/-! ## 2. The archimedean lower bound (D-037 Step 1) -/\n\n/-- a₁ = (log 4π + γ)/2, the j = 1 Lagarias coefficient. -/\ndef lagariasA1 : ℝ := (Real.log (4 * Real.pi) + Real.eulerMascheroniConstant) / 2\n\n/-- S_∞(n) in the exact odd-m identity form (D-037):\nS_∞(n) = (1−a₁)n − 1 + Σ_{m ≥ 3, odd} [(1−1/m)ⁿ − 1 + n/m].\n(Same tsum-summability honesty note as liCoeff.) -/\ndef SInfty (n : ℕ) : ℝ :=\n (1 - lagariasA1) * n - 1 +\n tsum fun m : {m : ℕ // Odd m ∧ 3 ≤ m} =>\n ((1 - 1 / (m : ℝ)) ^ n - 1 + (n : ℝ) / (m : ℝ))\n\n/-- C₁ = (γ − 1 − log 2π)/2 (D-037). -/\ndef lagariasC1 : ℝ :=\n (Real.eulerMascheroniConstant - 1 - Real.log (2 * Real.pi)) / 2\n\n/-- [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\n\n/-! ## 3. The margin and its convexity (D-057) -/\n\n/-- The honest closed-form unit-interval zero-count majorant (D-056 §2):\nĈ₀(t) = 0.433 log(t+2) + 0.886 log log(t+2) + 2.9. -/\ndef C0hat (t : ℝ) : ℝ :=\n 0.433 * Real.log (t + 2) + 0.886 * Real.log (Real.log (t + 2)) + 2.9\n\n/-- H majorant with A = 10.5, B₀ = 48 (D-056). -/\ndef Hhat (T : ℝ) : ℝ :=\n 3 * C0hat T ^ 2 + 10.5 * Real.log (T + 2) + 48\n\n/-- The I_I boundary-integral majorant (D-057 §3):\nB̃₄(n) = 2(√n+1)·(e^{√n/2}+1)·0.57·2^{−(2√n−2)}. -/\ndef IIMaj (n : ℝ) : ℝ :=\n 2 * (Real.sqrt n + 1) * (Real.exp (Real.sqrt n / 2) + 1) * 0.57 *\n 2 ^ (-(2 * Real.sqrt n - 2))\n\n/-- The margin majorant chain (D-057): margiñ(n) = S(n) − B̃(n) + 1 with\nthe counting function majorized by a smooth function F (the explicit\nTrudgian N(T) majorant is part of the formalization content and enters\nhere as a parameter with its majorant property as a hypothesis).\nM₀ = 1.3352 (E-023, grid-verified — see D-060 §4 for its status). -/\ndef marginTilde (F : ℝ → ℝ) (n : ℝ) : ℝ :=\n let T := Real.sqrt n + 1\n ((1 / 2) * n * Real.log n +\n (lagariasC1 - Real.eulerMascheroniConstant / 2) * n - 4) -\n (2 * F T + 4 * T * ((2 / 3) * C0hat T + 10.5 * Real.log (T + 2) + 48) +\n 40 * 1.3352 + 2 * (Real.exp 4 + 1) * (7 * Hhat T + 3.3) +\n IIMaj n + 1) + 1\n\n/-- [SKELETON] Margin convexity (D-057, draft §3.1 Step 4): for any\ntwice-differentiable majorant F of the zero count N(0,T] whose\nψ-block ψ[F](T) = F″(T) − F′(T)/(T−1) is negative for T ≥ √20 + 1\n(the D-057 11-block table discharges this for the explicit Trudgian\nmajorant), the margin majorant margiñ is convex on [20, ∞).\nTogether with margiñ(8×10⁴) = 16 020 > 0 and margiñ′(8×10⁴) > 0\n(E-028/E-029) this gives margin > 0 on [8×10⁴, N₁]. -/\ntheorem marginTilde_convex (F : ℝ → ℝ) (hF : ContDiff ℝ 2 F)\n (hmaj : ∀ T : ℝ, (Ncount 0 T : ℝ) ≤ F T)\n (hψ : ∀ T : ℝ, Real.sqrt 20 + 1 ≤ T →\n deriv (deriv F) T - deriv F T / (T - 1) < 0) :\n ConvexOn ℝ (Set.Ici 20) (marginTilde F) := by\n sorry\n\n/-- [SKELETON] The D-057 chain-rule identity behind the 11-block\nreduction: with T(n) = √n + 1,\nd²/dn² φ(T(n)) = [φ″(T) − φ′(T)/(T−1)] / (4n). -/\ntheorem chain_rule_sqrt_shift (φ : ℝ → ℝ) (hφ : ContDiff ℝ 2 φ)\n (n : ℝ) (hn : 0 < n) :\n deriv (deriv fun n => φ (Real.sqrt n + 1)) n =\n (deriv (deriv φ) (Real.sqrt n + 1) -\n deriv φ (Real.sqrt n + 1) / Real.sqrt n) / (4 * n) := by\n sorry\n\nend\n\nend NguyenRH1\n"},"extra_content":null}]