D-007 — zeta-23-lean inspection & audit confirmation (task 0.5)

Date: 2026-08-17 | Session: 001 | Task: 0.5 | Status: complete (static audit); full rebuild deferred

1. Clone facts

Repo: https://github.com/anthropics/zeta-23-lean — cloned to D:\Python\Quantum\zeta-23-lean, HEAD at tag v1.0 = commit 3635e74 ("Merge PR #3 xiprime-pairceiling"). Toolchain leanprover/lean4:v4.33.0-rc2; Mathlib pinned at 51e6992efd06 (lake-manifest.json). NOTE: nested git repo — excluded from our git via .gitignore; it is an external artifact with its own VCS.

2. Structure map (for Track D reuse)

• Zeta23/Statement.lean — counting functions vs Mathlib riemannZeta.
• Zeta23/Unconditional.lean, Final.lean, FinalMult.lean — headline Thms A/B/C (2/3 on-line, 2/3 simple, 5/6 distinct; dyadic + cumulative).
• Zeta23/ThmD/ — Montgomery–Taylor constants (c₁ = √2 tan ϑ/(1+ϑ tan ϑ), ϑ = 1/√2, c₁ = 0.75329…; 2 − 1/c₁* = 0.67250 ✔ consistent with E-001).
• Zeta23/ThmE/, ThmDE/ — Dirichlet L-function versions (paper's Thm B).
• Zeta23/XiPrime/ — ξ′ results (Remark 7.1 constants).
• Zeta23/PairCeiling/ — the 0.682 bandwidth-one ceiling (LawN256.lean). ← MUST READ before attacking the ceiling (open thread T3).
• Zeta23/LinAlg/, MV/, Poisson/, WeilEF/, ExplicitFormula/, RvM/, GammaFacts/, PrimeSideA/B/, ZeroSide/, Tail/, Taper/, Chebyshev.lean — the machine-checkable skeleton of every lemma we reproduced in D-002..D-005. Our Phase-1 lemmas should target these module boundaries.
• Zeta23/FromPNTPlus/ — ports from PrimeNumberTheoremAnd (attribution kept).
• comparator/ — trusted Challenge statements (Mathlib-only deps, deliberate sorry placeholders) + Solution (delegating to Zeta23).
• AUDIT.md — reproduction instructions + recorded results.

3. Audit cross-check (static, independent)

AUDIT.md records: 0 axiom declarations; 27 sorries, ALL in trusted challenge statement files; #print axioms on all 27 comparator statements + 28 library theorems → only [propext, Classical.choice, Quot.sound]; no sorryAx. My static spot-check (grep, sources as-is):

• ^\s*axiom matches: 3 — ALL benign: two are inside a tactic doc-comment example (FromPNTPlus/Tactic/AdditiveCombination.lean:183–184, inside /- … -/ block, verified by reading the file), one is prose in Hypotheses.lean:15. ⟹ 0 real axiom declarations. ✔ consistent.
• sorry under Zeta23/ + Solution*: 3 matches — all comments ("sorry'd", "no sorry enters", "sorry-free prefix"). ⟹ 0 real sorries outside trusted challenge files. ✔ consistent.
• Challenge.lean / Challenge/Multiplicity.lean: 17/13 raw sorry tokens (audit counts 15/12 after comment-stripping) — the deliberate placeholders. ✔ consistent. CONCLUSION: audit claims hold up under static inspection. [VERIFIED-static]

4. NOT done (deferred, recorded)

Full kernel-level rebuild (lake build + lake env lean comparator/PrintAxioms*.lean) requires installing elan + Lean v4.33.0-rc2 and building pinned Mathlib — heavy (8890 jobs per AUDIT.md). DEFERRED to Phase 5 (Track D) or an earlier dedicated sub-stage if we start contributing Lean lemmas. Decision recorded; no silent assumption. Also deferred: reading PairCeiling/LawN256.lean in detail (scheduled with thread T3 / Phase 1.1).

5. Notable detail for our chain notes

README: in the repo, Theorem C (5/6 distinct) is obtained from the rank–trace inequality with parameter c = 3 (Zeta23.ZeroSide.ZeroBlockData .mult_three), whereas the paper text derives it via c = 2 regrouping — two formulations of the same constant. Worth knowing when we formalize. Also: c₁* notation (0.75329…) = reciprocal of our c⁻¹_MT = 1.32749930. ✔