← Session 18 — Lean tier (ii): finite-height proof + certified base points
thinking (1822 chars)
PERFECT result:
- 139 declarations audited.
- 134 of them: exactly `[propext, Classical.choice, Quot.sound]` — the 3 standard axioms only.
- 5 (exactly the intended skeletons): the 3 standard + sorryAx.
- NOTHING else. No hidden axioms anywhere.
Step C complete. Now step D: statement-to-paper correspondence. Let me display the exact final theorem statements and the key definitions (SfBoundProp, RHUpTo, LiVerifiedUpTo, liCoeff, Sf, Bn, FAlt) and map them to the paper claims. I've read these already this session — let me re-verify the exact current statements by grepping them out of the built source (they're unchanged since my writes, but the audit should re-display them for the record).
Key checks:
1. lambda_pos_finite_height_verified: 3 hypotheses (RHUpTo 3e12, LiVerifiedUpTo 5e5, SfBoundProp) → ∀ n, 1 ≤ n → n ≤ (3e12−1)² → 0 < (liCoeff n).re. ✓ matches paperA Theorem R-004 + Appendix B claim.
2. SfBoundProp: ∀ n : ℕ, 100000 ≤ n → (n:ℝ) ≤ (3*10^12−1)^2 → |Sf n| ≤ Bn FAlt (n:ℝ). ✓ matches "|S_f(n)| ≤ B(n) on 10⁵ ≤ n ≤ (T₀−1)²".
3. RHUpTo T₀: ∀ ρ, IsNontrivialZero ρ → |ρ.im| ≤ T₀ → ρ.re = 1/2 ✓ "RH verified to height T₀".
4. LiVerifiedUpTo N: ∀ n, 1 ≤ n → n ≤ N → 0 < (liCoeff n).re ✓.
5. liCoeff: zero-side tsum with multiplicity ✓ (matches λ_n = Σ′_ρ[1−(1−1/ρ)ⁿ]; the summability honesty note is documented in the def comment — content inside SfBoundProp).
6. Sf := SInfty + 1 − liCoeff.re — BL Thm 2 by construction (documented).
7. marginTilde_FAlt_80000_pos / _lt_100000: the two evaluations ✓.
Also verify lambda_pos_finite_height (the 5-hypothesis modular version) — both exist.
Then step E: re-run the zeta-23-lean comparator audits. From D-061 §3: the vendored repo has PrintAxioms scripts. Let me check what's there: zeta-23-lean has AUDIT.md and some audit scripts. Let me find and run them.
**Exhaustive audit: PERFECT.** All 139 declarations — 134 with exactly the 3 standard axioms; exactly the 5 intended skeletons carry `sorryAx`; nothing else anywhere. Now the statement-to-paper correspondence check.
tool: Bash
input
{
"command": "cd D:/Python/Quantum/research/lean/NguyenRH1/NguyenRH1 && echo \"=== final theorem ===\" && grep -A 8 \"theorem lambda_pos_finite_height_verified\" LiBasePoints.lean && echo \"=== SfBoundProp ===\" && grep -A 4 \"def SfBoundProp\" LiSkeleton.lean && echo \"=== RHUpTo / LiVerifiedUpTo ===\" && grep -A 3 \"def RHUpTo\" LiSkeleton.lean && grep -A 3 \"def LiVerifiedUpTo\" LiSkeleton.lean && echo \"=== liCoeff / Sf ===\" && grep -A 3 \"def liCoeff\" LiSkeleton.lean && grep -A 1 \"def Sf \" LiSkeleton.lean",
"description": "Display final statements for paper correspondence check"
}
raw content_json (database row)
[{"type":"thinking","thinking":"PERFECT result:\n- 139 declarations audited.\n- 134 of them: exactly `[propext, Classical.choice, Quot.sound]` — the 3 standard axioms only.\n- 5 (exactly the intended skeletons): the 3 standard + sorryAx.\n- NOTHING else. No hidden axioms anywhere.\n\nStep C complete. Now step D: statement-to-paper correspondence. Let me display the exact final theorem statements and the key definitions (SfBoundProp, RHUpTo, LiVerifiedUpTo, liCoeff, Sf, Bn, FAlt) and map them to the paper claims. I've read these already this session — let me re-verify the exact current statements by grepping them out of the built source (they're unchanged since my writes, but the audit should re-display them for the record).\n\nKey checks:\n1. lambda_pos_finite_height_verified: 3 hypotheses (RHUpTo 3e12, LiVerifiedUpTo 5e5, SfBoundProp) → ∀ n, 1 ≤ n → n ≤ (3e12−1)² → 0 < (liCoeff n).re. ✓ matches paperA Theorem R-004 + Appendix B claim.\n2. SfBoundProp: ∀ n : ℕ, 100000 ≤ n → (n:ℝ) ≤ (3*10^12−1)^2 → |Sf n| ≤ Bn FAlt (n:ℝ). ✓ matches \"|S_f(n)| ≤ B(n) on 10⁵ ≤ n ≤ (T₀−1)²\".\n3. RHUpTo T₀: ∀ ρ, IsNontrivialZero ρ → |ρ.im| ≤ T₀ → ρ.re = 1/2 ✓ \"RH verified to height T₀\".\n4. LiVerifiedUpTo N: ∀ n, 1 ≤ n → n ≤ N → 0 < (liCoeff n).re ✓.\n5. liCoeff: zero-side tsum with multiplicity ✓ (matches λ_n = Σ′_ρ[1−(1−1/ρ)ⁿ]; the summability honesty note is documented in the def comment — content inside SfBoundProp).\n6. Sf := SInfty + 1 − liCoeff.re — BL Thm 2 by construction (documented).\n7. marginTilde_FAlt_80000_pos / _lt_100000: the two evaluations ✓.\n\nAlso verify lambda_pos_finite_height (the 5-hypothesis modular version) — both exist.\n\nThen step E: re-run the zeta-23-lean comparator audits. From D-061 §3: the vendored repo has PrintAxioms scripts. Let me check what's there: zeta-23-lean has AUDIT.md and some audit scripts. Let me find and run them.","signature":""},{"type":"text","text":"**Exhaustive audit: PERFECT.** All 139 declarations — 134 with exactly the 3 standard axioms; exactly the 5 intended skeletons carry `sorryAx`; nothing else anywhere. Now the statement-to-paper correspondence check."},{"type":"tool_use","id":"Bash_264","name":"Bash","input":{"command":"cd D:/Python/Quantum/research/lean/NguyenRH1/NguyenRH1 && echo \"=== final theorem ===\" && grep -A 8 \"theorem lambda_pos_finite_height_verified\" LiBasePoints.lean && echo \"=== SfBoundProp ===\" && grep -A 4 \"def SfBoundProp\" LiSkeleton.lean && echo \"=== RHUpTo / LiVerifiedUpTo ===\" && grep -A 3 \"def RHUpTo\" LiSkeleton.lean && grep -A 3 \"def LiVerifiedUpTo\" LiSkeleton.lean && echo \"=== liCoeff / Sf ===\" && grep -A 3 \"def liCoeff\" LiSkeleton.lean && grep -A 1 \"def Sf \" LiSkeleton.lean","description":"Display final statements for paper correspondence check"},"extra_content":null}]